harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem restrict_prod_eq_prod_univ (s : Set α) :
    (μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ univ)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
this : ν = ν.restrict univ
⊢ (μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ univ)

Tactic:
rw [this, Measure.prod_restrict, ← this]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
⊢ (μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ univ)

Tactic:
have : ν = ν.restrict Set.univ := Measure.restrict_univ.symm

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set α
this : ν = ν.restrict univ
⊢ (μ.restrict s).prod ν = (μ.prod ν).restrict (s ×ˢ univ)
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
/-- The difference `log (1+z) - z` is bounded by `‖z‖^2/(2*(1-‖z‖))` when `‖z‖ < 1`. -/
lemma norm_log_one_add_sub_self_le {z : ℂ} (hz : ‖z‖ < 1) :
    ‖log (1 + z) - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2

Proof state:
case h.e'_4.h.e'_6
z : ℂ
hz : ‖z‖ < 1
⊢ 2 = ↑1 + 1

Tactic:
norm_num

Result:
no goals

Proof state:
case h.e'_3.h.e'_3
z : ℂ
hz : ‖z‖ < 1
⊢ log (1 + z) - z = log (1 + z) - logTaylor (1 + 1) z

Tactic:
simp [logTaylor_succ, logTaylor_zero, sub_eq_add_neg]

Result:
no goals

Proof state:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2

Tactic:
convert norm_log_sub_logTaylor_le 1 hz using 2

Result:
case h.e'_3.h.e'_3
z : ℂ
hz : ‖z‖ < 1
⊢ log (1 + z) - z = log (1 + z) - logTaylor (1 + 1) z

case h.e'_4.h.e'_6
z : ℂ
hz : ‖z‖ < 1
⊢ 2 = ↑1 + 1
-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem map_one_ne_zero (f_ne_zero : f ≠ 0) (f_nonneg : 0 ≤ f)
    (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) : f 1 ≠ 0

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h1 : f 1 = 0
⊢ False

Tactic:
specialize f_mul 1

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
h1 : f 1 = 0
f_mul : ∀ (y : R), f (1 * y) ≤ c * f 1 * f y
⊢ False

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
h1 : f 1 = 0
f_mul : ∀ (y : R), f (1 * y) ≤ c * f 1 * f y
⊢ False

Tactic:
simp_rw [h1, one_mul, mul_zero, zero_mul] at f_mul

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
h1 : f 1 = 0
f_mul : ∀ (y : R), f y ≤ 0
⊢ False

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
h1 : f 1 = 0
f_mul : ∀ (y : R), f y ≤ 0
z : R
hz : f z ≠ 0 z
⊢ False

Tactic:
exact hz <| (f_mul z).antisymm (f_nonneg z)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ f 1 ≠ 0

Tactic:
intro h1

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h1 : f 1 = 0
⊢ False

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
h1 : f 1 = 0
f_mul : ∀ (y : R), f y ≤ 0
⊢ False

Tactic:
obtain ⟨z, hz⟩ := Function.ne_iff.mp f_ne_zero

Result:
case intro
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
h1 : f 1 = 0
f_mul : ∀ (y : R), f y ≤ 0
z : R
hz : f z ≠ 0 z
⊢ False
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem smul_zero_aux (x : T) : x • (0 : LocalizedModule S M) = 0

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
⊢ x • 0 = 0

Tactic:
conv => lhs; rw [← zero_mk 1, smul_def, smul_zero, zero_mk]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem rightInvSeq_singleton (i : B) : ris [i] = [s i]

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.rightInvSeq [i] = [cs.simple i]

Tactic:
simp [rightInvSeq]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem one_le_card {o} : 1 ≤ card o ↔ 1 ≤ o

Proof state:
o : Ordinal.{u_1}
⊢ 1 ≤ o.card ↔ 1 ≤ o

Tactic:
simpa using nat_le_card (n := 1)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_eq_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_eq ctx (m₁, m₂)) : denote_eq ctx (cancel m₁ m₂)

Proof state:
case h
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (m₁, m₂)
⊢ denote_eq ctx ([].reverse ++ m₁, [].reverse ++ m₂)

Tactic:
simp [h]

Result:
no goals

Proof state:
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (m₁, m₂)
⊢ denote_eq ctx (m₁.cancel m₂)

Tactic:
apply denote_eq_cancelAux

Result:
case h
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (m₁, m₂)
⊢ denote_eq ctx ([].reverse ++ m₁, [].reverse ++ m₂)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insertManyIfNewUnit_list
    {l : List α} {k : α} :
    get! (insertManyIfNewUnit m l).1 k = ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => Unit
l : List α
k : α
⊢ get! (insertManyIfNewUnit m l).val k = ()

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/Normal/Basic.lean
theorem AlgHom.fieldRange_of_normal {E : IntermediateField F K} [Normal F E]
    (f : E →ₐ[F] K) : f.fieldRange = E

Proof state:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
E : IntermediateField F K
inst✝ : Normal F ↥E
f : ↥E →ₐ[F] K
g : ↥E ≃ₐ[F] ↥E := f.restrictNormal' ↥E
⊢ f.fieldRange = E

Tactic:
rw [← show E.val.comp ↑g = f from DFunLike.ext_iff.mpr (f.restrictNormal_commutes E),
  ← AlgHom.map_fieldRange, AlgEquiv.fieldRange_eq_top g, ← AlgHom.fieldRange_eq_map,
  IntermediateField.fieldRange_val]

Result:
no goals

Proof state:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
E : IntermediateField F K
inst✝ : Normal F ↥E
f : ↥E →ₐ[F] K
⊢ f.fieldRange = E

Tactic:
let g := f.restrictNormal' E

Result:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
E : IntermediateField F K
inst✝ : Normal F ↥E
f : ↥E →ₐ[F] K
g : ↥E ≃ₐ[F] ↥E := f.restrictNormal' ↥E
⊢ f.fieldRange = E
-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJ_ne_0_ne_1728 (h0 : j ≠ 0) (h1728 : j ≠ 1728) : ofJ j = ofJNe0Or1728 j

Proof state:
F : Type u_2
inst✝¹ : Field F
j : F
inst✝ : DecidableEq F
h0 : j ≠ 0
h1728 : j ≠ 1728
⊢ ofJ j = ofJNe0Or1728 j

Tactic:
rw [ofJ, if_neg h0, if_neg h1728]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatMap_singleton (f : α → Vector β m) (x : α) : #v[x].flatMap f = (f x).cast (by simp)

Proof state:
α : Type u_1
β : Type u_2
m : Nat
f : α → Vector β m
x : α
⊢ { toArray := #[x], size_toArray := ⋯ }.flatMap f = Vector.cast ⋯ (f x)

Tactic:
simp [flatMap_def]

Result:
no goals

Proof state:
α : Type ?u.327418
β : Type ?u.327398
m : Nat
f : α → Vector β m
x : α
⊢ m = 1 * m

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem max_val {a : Fin n} : max (a : ℕ) n = n

Proof state:
n : ℕ
a : Fin n
⊢ ↑a ⊔ n = n

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem isUnit_of_mul_isUnit_right [CommMonoid M] {x y : M} (hu : IsUnit (x * y)) : IsUnit y :=
  @isUnit_of_mul_isUnit_left _ _ y x <| by rwa [mul_comm]

Proof state:
M : Type u_1
inst✝ : CommMonoid M
x y : M
hu : IsUnit (x * y)
⊢ IsUnit (y * x)

Tactic:
rwa [mul_comm]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem gcd_mul_lcm (i j : ℤ) : gcd i j * lcm i j = natAbs (i * j)

Proof state:
i j : ℤ
⊢ i.gcd j * i.lcm j = (i * j).natAbs

Tactic:
rw [Int.gcd, Int.lcm, Nat.gcd_mul_lcm, natAbs_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem push_mk {data : Array α} {size : data.size = n} {x : α} :
    (Vector.mk data size).push x =
      Vector.mk (data.push x) (by simp [size, Nat.succ_eq_add_one]) := rfl

Proof state:
α : Type ?u.2918
n : Nat
data : Array α
size : data.size = n
x : α
⊢ (data.push x).size = n + 1

Tactic:
simp [size, Nat.succ_eq_add_one]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem mapₗ_apply_of_measurable {f : α → β} (hf : Measurable f) (μ : Measure α) :
    mapₗ f μ = map f μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure α
⊢ (mapₗ f) μ = map f μ

Tactic:
simp only [← mapₗ_mk_apply_of_aemeasurable hf.aemeasurable]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure α
⊢ (mapₗ f) μ = (mapₗ (AEMeasurable.mk f ⋯)) μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure α
⊢ (mapₗ f) μ = (mapₗ (AEMeasurable.mk f ⋯)) μ

Tactic:
exact mapₗ_congr hf hf.aemeasurable.measurable_mk hf.aemeasurable.ae_eq_mk

Result:
no goals
-- Mathlib/Topology/Instances/ZMultiples.lean
theorem tendsto_coe_cofinite : Tendsto ((↑) : ℤ → ℝ) cofinite (cocompact ℝ)

Proof state:
⊢ Tendsto Int.cast Filter.cofinite (cocompact ℝ)

Tactic:
apply (castAddHom ℝ).tendsto_coe_cofinite_of_discrete cast_injective

Result:
⊢ DiscreteTopology ↥(castAddHom ℝ).range

Proof state:
⊢ DiscreteTopology ↥(castAddHom ℝ).range

Tactic:
rw [range_castAddHom]

Result:
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 1)

Proof state:
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 1)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.isOpen_iff {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) :
    IsOpen s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Proof state:
α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ IsOpen s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Tactic:
simp [isOpen_iff_mem_nhds, hb.mem_nhds_iff]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem multipliable_mabs_iff [LinearOrderedCommGroup α] [UniformSpace α] [UniformGroup α]
    [CompleteSpace α] {f : ι → α} : (Multipliable fun x ↦ mabs (f x)) ↔ Multipliable f :=
  let s := { x | 1 ≤ f x }
  have h1 : ∀ x : s, mabs (f x) = f x := fun x ↦ mabs_of_one_le x.2
  have h2 : ∀ x : ↑sᶜ, mabs (f x) = (f x)⁻¹ := fun x ↦ mabs_of_lt_one (not_le.1 x.2)
  calc (Multipliable fun x ↦ mabs (f x)) ↔
      (Multipliable fun x : s ↦ mabs (f x)) ∧ Multipliable fun x : ↑sᶜ ↦ mabs (f x) :=
        multipliable_subtype_and_compl.symm
  _ ↔ (Multipliable fun x : s ↦ f x) ∧ Multipliable fun x : ↑sᶜ ↦ (f x)⁻¹

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : LinearOrderedCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformGroup α
inst✝ : CompleteSpace α
f : ι → α
s : Set ι := {x | 1 ≤ f x}
h1 : ∀ (x : ↑s), mabs (f ↑x) = f ↑x
h2 : ∀ (x : ↑sᶜ), mabs (f ↑x) = (f ↑x)⁻¹
⊢ ((Multipliable fun x => mabs (f ↑x)) ∧ Multipliable fun x => mabs (f ↑x)) ↔
    (Multipliable fun x => f ↑x) ∧ Multipliable fun x => (f ↑x)⁻¹

Tactic:
simp only [h1, h2]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : LinearOrderedCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformGroup α
inst✝ : CompleteSpace α
f : ι → α
s : Set ι := {x | 1 ≤ f x}
h1 : ∀ (x : ↑s), mabs (f ↑x) = f ↑x
h2 : ∀ (x : ↑sᶜ), mabs (f ↑x) = (f ↑x)⁻¹
⊢ ((Multipliable fun x => f ↑x) ∧ Multipliable fun x => (f ↑x)⁻¹) ↔ Multipliable f

Tactic:
simp only [multipliable_inv_iff, multipliable_subtype_and_compl]

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem lowerBounds_insert (a : α) (s : Set α) :
    lowerBounds (insert a s) = Iic a ∩ lowerBounds s

Proof state:
α : Type u
inst✝ : Preorder α
a : α
s : Set α
⊢ lowerBounds (insert a s) = Iic a ∩ lowerBounds s

Tactic:
rw [insert_eq, lowerBounds_union, lowerBounds_singleton]

Result:
no goals
-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_concat_of_some (l : List (Option α)) (x : α) :
    (l.concat (some x)).reduceOption = l.reduceOption.concat x

Proof state:
α : Type u_1
l : List (Option α)
x : α
⊢ (l.concat (some x)).reduceOption = l.reduceOption.concat x

Tactic:
simp only [reduceOption_nil, concat_eq_append, reduceOption_append, reduceOption_cons_of_some]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem monomial_neg (n : ℕ) (a : R) : monomial n (-a) = -monomial n a

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
a : R
⊢ (monomial n) (-a) = -(monomial n) a

Tactic:
rw [eq_neg_iff_add_eq_zero, ← monomial_add, neg_add_cancel, monomial_zero_right]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
/-- Value of a geometric sum over the naturals. Note: see `geom_sum_mul_add` for a formulation
that avoids division and subtraction. -/
lemma Nat.geomSum_eq (hm : 2 ≤ m) (n : ℕ) :
    ∑ k ∈ range n, m ^ k = (m ^ n - 1) / (m - 1)

Proof state:
m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ ∑ k ∈ range n, m ^ k = (m ^ n - 1) / (m - 1)

Tactic:
refine (Nat.div_eq_of_eq_mul_left (tsub_pos_iff_lt.2 hm) <| tsub_eq_of_eq_add ?_).symm

Result:
m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ m ^ n = (∑ k ∈ range n, m ^ k) * (m - 1) + 1

Proof state:
m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ m ^ n = (∑ k ∈ range n, m ^ k) * (m - 1) + 1

Tactic:
simpa only [tsub_add_cancel_of_le (one_le_two.trans hm), eq_comm] using geom_sum_mul_add (m - 1) n

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
/-- If `M = R^ι`, `ofTensorProduct` is bijective. -/
lemma ofTensorProduct_bijective_of_pi_of_fintype [Finite ι] :
    Function.Bijective (ofTensorProduct I (ι → R))

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
ι : Type u_4
inst✝ : Finite ι
⊢ Function.Bijective ⇑(ofTensorProduct I (ι → R))

Tactic:
classical
cases nonempty_fintype ι
exact EquivLike.bijective (ofTensorProductEquivOfPiFintype I ι)

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
ι : Type u_4
inst✝ : Finite ι
val✝ : Fintype ι
⊢ Function.Bijective ⇑(ofTensorProduct I (ι → R))

Tactic:
exact EquivLike.bijective (ofTensorProductEquivOfPiFintype I ι)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
ι : Type u_4
inst✝ : Finite ι
⊢ Function.Bijective ⇑(ofTensorProduct I (ι → R))

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
ι : Type u_4
inst✝ : Finite ι
val✝ : Fintype ι
⊢ Function.Bijective ⇑(ofTensorProduct I (ι → R))
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
@[simp]
lemma compProd_apply_univ {κ : Kernel α β} {η : Kernel (α × β) γ}
    [IsSFiniteKernel κ] [IsMarkovKernel η] {a : α} :
    (κ ⊗ₖ η) a Set.univ = κ a Set.univ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
a : α
⊢ ((κ ⊗ₖ η) a) Set.univ = (κ a) Set.univ

Tactic:
rw [compProd_apply MeasurableSet.univ]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
a : α
⊢ ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ Set.univ} ∂κ a = (κ a) Set.univ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsMarkovKernel η
a : α
⊢ ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ Set.univ} ∂κ a = (κ a) Set.univ

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
lemma essInf_eq_ciInf (hμ : ∀ a, μ {a} ≠ 0) (hf : BddBelow (Set.range f)) :
    essInf f μ = ⨅ a, f a

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : ConditionallyCompleteLattice β
f : α → β
inst✝ : Nonempty α
hμ : ∀ (a : α), μ {a} ≠ 0
hf : BddBelow (range f)
⊢ essInf f μ = ⨅ a, f a

Tactic:
rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_ciInf hf]

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
theorem ofFn_mul' {m n} (f : Fin (m * n) → α) :
    List.ofFn f = List.flatten (List.ofFn fun i : Fin n => List.ofFn fun j : Fin m => f ⟨m * i + j,
    calc
      m * i + j < m * (i + 1) :=
        (Nat.add_lt_add_left j.prop _).trans_eq (by rw [Nat.mul_add, Nat.mul_one])
      _ ≤ _ := Nat.mul_le_mul_left _ i.prop⟩)

Proof state:
α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = (ofFn fun i => ofFn fun j => f ⟨m * ↑i + ↑j, ⋯⟩).flatten

Tactic:
simp_rw [m.mul_comm, ofFn_mul, Fin.cast_mk]

Result:
no goals

Proof state:
α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin n
j : Fin m
⊢ m * ↑i + m = m * (↑i + 1)

Tactic:
rw [Nat.mul_add, Nat.mul_one]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem piecewise_mem_pi {δ : α → Type*} {t : Set α} {t' : ∀ i, Set (δ i)} {f g} (hf : f ∈ pi t t')
    (hg : g ∈ pi t t') : s.piecewise f g ∈ pi t t'

Proof state:
α : Type u_1
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
i : α
ht : i ∈ t
⊢ s.piecewise f g i ∈ t' i

Tactic:
by_cases hs : i ∈ s <;> simp [hf i ht, hg i ht, hs]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
⊢ s.piecewise f g ∈ t.pi t'

Tactic:
intro i ht

Result:
α : Type u_1
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_8
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
i : α
ht : i ∈ t
⊢ s.piecewise f g i ∈ t' i
-- Mathlib/Tactic/CancelDenoms/Core.lean
theorem mul_subst {α} [CommRing α] {n1 n2 k e1 e2 t1 t2 : α}
    (h1 : n1 * e1 = t1) (h2 : n2 * e2 = t2) (h3 : n1 * n2 = k) : k * (e1 * e2) = t1 * t2

Proof state:
α : Type u_1
inst✝ : CommRing α
n1 n2 k e1 e2 t1 t2 : α
h1 : n1 * e1 = t1
h2 : n2 * e2 = t2
h3 : n1 * n2 = k
⊢ k * (e1 * e2) = t1 * t2

Tactic:
rw [← h3, mul_comm n1, mul_assoc n2, ← mul_assoc n1, h1,
    ← mul_assoc n2, mul_comm n2, mul_assoc, h2]

Result:
no goals
-- Mathlib/Data/PNat/Basic.lean
theorem exists_eq_succ_of_ne_one : ∀ {n : ℕ+} (_ : n ≠ 1), ∃ k : ℕ+, n = k + 1
  | ⟨1, _⟩, h₁ => False.elim <| h₁ rfl
  | ⟨n + 2, _⟩, _ => ⟨⟨n + 1, by simp⟩, rfl⟩

Proof state:
n : ℕ
property✝ : 0 < n + 2
x✝ : ⟨n + 2, property✝⟩ ≠ 1
⊢ 0 < n + 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma sub_bot {x : EReal} (h : x ≠ ⊥) : x - ⊥ = ⊤

Proof state:
x : EReal
h : x ≠ ⊥
⊢ x - ⊥ = ⊤

Tactic:
cases x <;> tauto

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem isClosedEmbedding_of_spaced_out {α} [TopologicalSpace α] [DiscreteTopology α]
    [T0Space β] {f : α → β} {s : Set (β × β)} (hs : s ∈ 𝓤 β)
    (hf : Pairwise fun x y => (f x, f y) ∉ s) : IsClosedEmbedding f

Proof state:
β : Type v
inst✝² : UniformSpace β
α : Type u_1
inst✝¹ : T0Space β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
inst✝ : DiscreteTopology α
⊢ IsClosedEmbedding f

Tactic:
let _ : UniformSpace α := ⊥

Result:
β : Type v
inst✝² : UniformSpace β
α : Type u_1
inst✝¹ : T0Space β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
inst✝ : DiscreteTopology α
x✝ : UniformSpace α := ⊥
⊢ IsClosedEmbedding f

Proof state:
β : Type v
inst✝² : UniformSpace β
α : Type u_1
inst✝¹ : T0Space β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
inst✝ : DiscreteTopology α
x✝ : UniformSpace α := ⊥
⊢ IsClosedEmbedding f

Tactic:
exact
  { (isUniformEmbedding_of_spaced_out hs hf).isEmbedding with
    isClosed_range := isClosed_range_of_spaced_out hs hf }

Result:
no goals

Proof state:
β : Type v
inst✝³ : UniformSpace β
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : DiscreteTopology α
inst✝ : T0Space β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
⊢ IsClosedEmbedding f

Tactic:
rcases @DiscreteTopology.eq_bot α _ _ with rfl

Result:
β : Type v
inst✝² : UniformSpace β
α : Type u_1
inst✝¹ : T0Space β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => (f x, f y) ∉ s
inst✝ : DiscreteTopology α
⊢ IsClosedEmbedding f
-- Mathlib/Order/UpperLower/Basic.lean
theorem map_Ioi (f : α ≃o β) (a : α) : map f (Ioi a) = Ioi (f a)

Proof state:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑((map f) (Ioi a)) ↔ x✝ ∈ ↑(Ioi (f a))

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
⊢ (map f) (Ioi a) = Ioi (f a)

Tactic:
ext

Result:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑((map f) (Ioi a)) ↔ x✝ ∈ ↑(Ioi (f a))
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem exists_zpow_eq_one (x : G) : ∃ (i : ℤ) (_ : i ≠ 0), x ^ (i : ℤ) = 1

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun x_1 => x * x_1) w 1
⊢ x ^ w = 1

Tactic:
exact (isPeriodicPt_mul_iff_pow_eq_one _).mp hw2

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun x_1 => x * x_1) w 1
⊢ ∃ i, ∃ (_ : i ≠ 0), x ^ i = 1

Tactic:
refine ⟨w, Int.natCast_ne_zero.mpr (_root_.ne_of_gt hw1), ?_⟩

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun x_1 => x * x_1) w 1
⊢ x ^ ↑w = 1

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun x_1 => x * x_1) w 1
⊢ x ^ ↑w = 1

Tactic:
rw [zpow_natCast]

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun x_1 => x * x_1) w 1
⊢ x ^ w = 1

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
⊢ ∃ i, ∃ (_ : i ≠ 0), x ^ i = 1

Tactic:
obtain ⟨w, hw1, hw2⟩ := isOfFinOrder_of_finite x

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt (fun x_1 => x * x_1) w 1
⊢ ∃ i, ∃ (_ : i ≠ 0), x ^ i = 1
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem measure_union_eq_top_iff : μ (s ∪ t) = ∞ ↔ μ s = ∞ ∨ μ t = ∞ :=
  not_iff_not.1 <| by simp only [← lt_top_iff_ne_top, ← Ne.eq_def, not_or, measure_union_lt_top_iff]

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ ¬μ (s ∪ t) = ⊤ ↔ ¬(μ s = ⊤ ∨ μ t = ⊤)

Tactic:
simp only [← lt_top_iff_ne_top, ← Ne.eq_def, not_or, measure_union_lt_top_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem twoPow_eq (w : Nat) (i : Nat) : twoPow w i = 1#w <<< i

Proof state:
w i : Nat
⊢ twoPow w i = 1#w <<< i

Tactic:
dsimp [twoPow]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem cosh_dist' (z w : ℍ) :
    Real.cosh (dist z w) = ((z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2) / (2 * z.im * w.im)

Proof state:
z w : ℍ
⊢ 2 * z.im * w.im + ((z.re - w.re) * (z.re - w.re) + (z.im - w.im) * (z.im - w.im)) =
    (z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2

Tactic:
ring

Result:
no goals

Proof state:
z w : ℍ
⊢ Real.cosh (dist z w) = ((z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2) / (2 * z.im * w.im)

Tactic:
field_simp [cosh_dist, Complex.dist_eq, Complex.sq_norm, normSq_apply]

Result:
z w : ℍ
⊢ 2 * z.im * w.im + ((z.re - w.re) * (z.re - w.re) + (z.im - w.im) * (z.im - w.im)) =
    (z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2
-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem corecF_eq {α : TypeVec n} {β : Type u} (g : β → F (α.append1 β)) (x : β) :
    M.dest q.P (corecF g x) = appendFun id (corecF g) <$$> repr (g x)

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: β)
x : β
⊢ M.dest (P F) (corecF g x) = (TypeVec.id ::: corecF g) <$$> repr (g x)

Tactic:
rw [corecF, M.dest_corec]

Result:
no goals