harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matroid/Dual.lean
theorem setOf_dual_isBase_eq : {B | M✶.IsBase B} = (fun X ↦ M.E \ X) '' {B | M.IsBase B}

Proof state:
case h
α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBase (M.E \ B) ∧ B ⊆ M.E ↔ ∃ x, M.IsBase x ∧ M.E \ x = B

Tactic:
refine ⟨fun h ↦ ⟨_, h.1, diff_diff_cancel_left h.2⟩,
  fun ⟨B', hB', h⟩ ↦ ⟨?_,h.symm.trans_subset diff_subset⟩⟩

Result:
case h
α : Type u_1
M : Matroid α
B : Set α
x✝ : ∃ x, M.IsBase x ∧ M.E \ x = B
B' : Set α
hB' : M.IsBase B'
h : M.E \ B' = B
⊢ M.IsBase (M.E \ B)

Proof state:
case h
α : Type u_1
M : Matroid α
B : Set α
x✝ : ∃ x, M.IsBase x ∧ M.E \ x = B
B' : Set α
hB' : M.IsBase B'
h : M.E \ B' = B
⊢ M.IsBase (M.E \ B)

Tactic:
rwa [← h, diff_diff_cancel_left hB'.subset_ground]

Result:
no goals

Proof state:
case h
α : Type u_1
M : Matroid α
B : Set α
⊢ B ∈ {B | M✶.IsBase B} ↔ B ∈ (fun X => M.E \ X) '' {B | M.IsBase B}

Tactic:
simp only [mem_setOf_eq, mem_image, dual_isBase_iff']

Result:
case h
α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBase (M.E \ B) ∧ B ⊆ M.E ↔ ∃ x, M.IsBase x ∧ M.E \ x = B

Proof state:
α : Type u_1
M : Matroid α
⊢ {B | M✶.IsBase B} = (fun X => M.E \ X) '' {B | M.IsBase B}

Tactic:
ext B

Result:
case h
α : Type u_1
M : Matroid α
B : Set α
⊢ B ∈ {B | M✶.IsBase B} ↔ B ∈ (fun X => M.E \ X) '' {B | M.IsBase B}
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem forall_mem_range {f : α →ₛ β} {p : β → Prop} : (∀ y ∈ f.range, p y) ↔ ∀ x, p (f x)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f : α →ₛ β
p : β → Prop
⊢ (∀ y ∈ f.range, p y) ↔ ∀ (x : α), p (f x)

Tactic:
simp only [mem_range, Set.forall_mem_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
    (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b

Proof state:
α : Type u_1
n : Nat
a b : α
p : α → Bool
⊢ find? p (replicate n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma IsMarkovKernel.map (κ : Kernel α β) [IsMarkovKernel κ] (hf : Measurable f) :
    IsMarkovKernel (map κ f) :=
  ⟨fun a => ⟨by rw [map_apply' κ hf a MeasurableSet.univ, Set.preimage_univ, measure_univ]⟩⟩

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
κ : Kernel α β
inst✝ : IsMarkovKernel κ
hf : Measurable f
a : α
⊢ ((κ.map f) a) Set.univ = 1

Tactic:
rw [map_apply' κ hf a MeasurableSet.univ, Set.preimage_univ, measure_univ]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean
@[to_additive]
lemma prod_Iio_mul_right (a : α) : (∏ x ∈ Iio a, f x) * f a = ∏ x ∈ Iic a, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ (∏ x ∈ Iio a, f x) * f a = ∏ x ∈ Iic a, f x

Tactic:
rw [mul_comm, right_mul_prod_Iio]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Bimon_.lean
theorem comul_assoc_flip_hom (M : Bimon_ C) :
    M.comul.hom ≫ (M.comul.hom ▷ M.X.X) =
      M.comul.hom ≫ (M.X.X ◁ M.comul.hom) ≫ (α_ M.X.X M.X.X M.X.X).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon_ C
⊢ M.comul.hom ≫ M.comul.hom ▷ M.X.X = M.comul.hom ≫ M.X.X ◁ M.comul.hom ≫ (α_ M.X.X M.X.X M.X.X).inv

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_monomial_ne {m n : σ →₀ ℕ} (h : m ≠ n) (a : R) : coeff R m (monomial R n a) = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ (coeff R m) ((monomial R n) a) = 0

Tactic:
rw [monomial_def]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ (coeff R m) ((LinearMap.single R (fun x => R) n) a) = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ (coeff R m) ((monomial R n) a) = 0

Tactic:
classical
rw [monomial_def]
exact Pi.single_eq_of_ne h _

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
h : m ≠ n
a : R
⊢ (coeff R m) ((LinearMap.single R (fun x => R) n) a) = 0

Tactic:
exact Pi.single_eq_of_ne h _

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem isPartition_iff_iUnion_eq {π : Prepartition I} : π.IsPartition ↔ π.iUnion = I

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ π.IsPartition ↔ π.iUnion = ↑I

Tactic:
simp_rw [IsPartition, Set.Subset.antisymm_iff, π.iUnion_subset, true_and, Set.subset_def,
  mem_iUnion, Box.mem_coe]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/ExistsOfLE.lean
theorem le_of_forall_one_lt_le_mul (h : ∀ ε : α, 1 < ε → a ≤ b * ε) : a ≤ b :=
  le_of_forall_gt_imp_ge_of_dense fun x hxb => by
    obtain ⟨ε, rfl⟩ := exists_mul_of_le hxb.le
    exact h _ (one_lt_of_lt_mul_right hxb)

Proof state:
case intro
α : Type u
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : Monoid α
inst✝¹ : ExistsMulOfLE α
inst✝ : MulLeftReflectLT α
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
ε : α
hxb : b < b * ε
⊢ a ≤ b * ε

Tactic:
exact h _ (one_lt_of_lt_mul_right hxb)

Result:
no goals

Proof state:
α : Type u
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : Monoid α
inst✝¹ : ExistsMulOfLE α
inst✝ : MulLeftReflectLT α
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
x : α
hxb : b < x
⊢ a ≤ x

Tactic:
obtain ⟨ε, rfl⟩ := exists_mul_of_le hxb.le

Result:
case intro
α : Type u
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : Monoid α
inst✝¹ : ExistsMulOfLE α
inst✝ : MulLeftReflectLT α
a b : α
h : ∀ (ε : α), 1 < ε → a ≤ b * ε
ε : α
hxb : b < b * ε
⊢ a ≤ b * ε
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem pullbackIsoUnopPushout_hom_inl {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g]
    [HasPushout f.op g.op] :
    pushout.inl _ _ ≫ (pullbackIsoUnopPushout f g).hom.op = (pullback.fst f g).op

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ pushout.inl f.op g.op ≫ (pullbackIsoUnopPushout f g).hom.op = (pullback.fst f g).op

Tactic:
apply Quiver.Hom.unop_inj

Result:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pushout.inl f.op g.op ≫ (pullbackIsoUnopPushout f g).hom.op).unop = (pullback.fst f g).op.unop

Proof state:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pushout.inl f.op g.op ≫ (pullbackIsoUnopPushout f g).hom.op).unop = (pullback.fst f g).op.unop

Tactic:
dsimp

Result:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pullbackIsoUnopPushout f g).hom ≫ (pushout.inl f.op g.op).unop = pullback.fst f g

Proof state:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pullbackIsoUnopPushout f g).hom ≫ (pushout.inl f.op g.op).unop = pullback.fst f g

Tactic:
rw [← pullbackIsoUnopPushout_inv_fst, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma IsMeasurableRatCDF.measure_stieltjesFunction_Iic (a : α) (x : ℝ) :
    (hf.stieltjesFunction a).measure (Iic x) = ENNReal.ofReal (hf.stieltjesFunction a x)

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ (hf.stieltjesFunction a).measure (Iic x) = ENNReal.ofReal (↑(hf.stieltjesFunction a) x - 0)

Tactic:
exact (hf.stieltjesFunction a).measure_Iic (tendsto_stieltjesFunction_atBot hf a) _

Result:
no goals

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ (hf.stieltjesFunction a).measure (Iic x) = ENNReal.ofReal (↑(hf.stieltjesFunction a) x)

Tactic:
rw [← sub_zero (hf.stieltjesFunction a x)]

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ (hf.stieltjesFunction a).measure (Iic x) = ENNReal.ofReal (↑(hf.stieltjesFunction a) x - 0)
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mul_smul_aux (x y : T) (p : LocalizedModule S M) :
    (x * y) • p = x • y • p

Proof state:
case h
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 y : T
m : M
s : ↥S
⊢ (x * y) • mk m s = x • y • mk m s

Tactic:
rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y]

Result:
case h
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 y : T
m : M
s : ↥S
⊢ (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 *
        IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) •
      mk m s =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2 • mk m s

Proof state:
case h
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 y : T
m : M
s : ↥S
⊢ (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 *
        IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) •
      mk m s =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2 • mk m s

Tactic:
simp_rw [← IsLocalization.mk'_mul, mk'_smul_mk, ← mul_smul, mul_assoc]

Result:
no goals

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 y : T
p : LocalizedModule S M
⊢ (x * y) • p = x • y • p

Tactic:
induction' p with m s

Result:
case h
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 y : T
m : M
s : ↥S
⊢ (x * y) • mk m s = x • y • mk m s
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem units_smul_resolvent_self {r : Rˣ} {a : A} :
    r • resolvent a (r : R) = resolvent (r⁻¹ • a) (1 : R)

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : A
⊢ r • resolvent a ↑r = resolvent (r⁻¹ • a) 1

Tactic:
simpa only [Units.smul_def, Algebra.id.smul_eq_mul, Units.inv_mul] using
  @units_smul_resolvent _ _ _ _ _ r r a

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem abs_sin_eq_sqrt_one_sub_cos_sq (x : ℝ) : |sin x| = √(1 - cos x ^ 2)

Proof state:
x : ℝ
⊢ |sin x| = √(1 - cos x ^ 2)

Tactic:
rw [← sin_sq, sqrt_sq_eq_abs]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_nonneg {f : R → R} {a : A} (h : ∀ x ∈ spectrum R a, 0 ≤ f x) :
    0 ≤ cfc f a

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.683489) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, 0 ≤ f x
hf : ContinuousOn f (spectrum R a)
⊢ 0 ≤ cfc f a

Tactic:
simpa using cfc_mono h

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.683489) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, 0 ≤ f x
⊢ 0 ≤ cfc f a

Tactic:
by_cases hf : ContinuousOn f (spectrum R a)

Result:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.683489) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, 0 ≤ f x
hf : ContinuousOn f (spectrum R a)
⊢ 0 ≤ cfc f a

case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type ?u.683489) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, 0 ≤ f x
hf : ¬ContinuousOn f (spectrum R a)
⊢ 0 ≤ cfc f a

Proof state:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : OrderedCommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : ∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁵ : TopologicalSpace A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
h : ∀ x ∈ spectrum R a, 0 ≤ f x
hf : ¬ContinuousOn f (spectrum R a)
⊢ 0 ≤ cfc f a

Tactic:
simp only [cfc_apply_of_not_continuousOn _ hf, le_rfl]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem vanishingIdeal_eq_top_iff {s : Set (PrimeSpectrum R)} : vanishingIdeal s = ⊤ ↔ s = ∅

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s = ⊤ ↔ s = ∅

Tactic:
rw [← top_le_iff, ← subset_zeroLocus_iff_le_vanishingIdeal, Submodule.top_coe, zeroLocus_univ,
  Set.subset_empty_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem trailingCoeff_mul {R : Type*} [Ring R] [NoZeroDivisors R] (p q : R[X]) :
    (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff

Proof state:
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff

Tactic:
rw [← reverse_leadingCoeff, reverse_mul_of_domain, leadingCoeff_mul, reverse_leadingCoeff,
  reverse_leadingCoeff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Ordered.map (f : α → β) [IsMonotone cmpα cmpβ f] :
    ∀ {t : RBNode α}, t.Ordered cmpα → (t.map f).Ordered cmpβ
  | nil, _ => ⟨⟩
  | node _ a x b, ⟨ax, xb, ha, hb⟩ => by
    refine ⟨ax.map ?_, xb.map ?_, ha.map f, hb.map f⟩ <;> exact IsMonotone.lt_mono

Proof state:
α : Type u_1
β : Type u_2
cmpα : α → α → Ordering
cmpβ : β → β → Ordering
f : α → β
inst✝ : IsMonotone cmpα cmpβ f
c✝ : RBColor
a : RBNode α
x : α
b : RBNode α
ax : All (fun x_1 => cmpLT cmpα x_1 x) a
xb : All (fun x_1 => cmpLT cmpα x x_1) b
ha : Ordered cmpα a
hb : Ordered cmpα b
⊢ Ordered cmpβ (map f (node c✝ a x b))

Tactic:
refine ⟨ax.map ?_, xb.map ?_, ha.map f, hb.map f⟩ <;> exact IsMonotone.lt_mono

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma setLIntegral_condKernel_univ_right (hf : Measurable f) {s : Set β}
    (hs : MeasurableSet s) :
    ∫⁻ b in s, ∫⁻ ω, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst
      = ∫⁻ x in s ×ˢ Set.univ, f x ∂ρ

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ

Tactic:
rw [← setLIntegral_condKernel hf hs MeasurableSet.univ]

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in Set.univ, f (b, ω) ∂ρ.condKernel b ∂ρ.fst

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in Set.univ, f (b, ω) ∂ρ.condKernel b ∂ρ.fst

Tactic:
simp_rw [Measure.restrict_univ]

Result:
no goals
-- Mathlib/Probability/Kernel/MeasurableLIntegral.lean
theorem Kernel.measurable_lintegral_indicator_const {t : Set (α × β)} (ht : MeasurableSet t)
    (c : ℝ≥0∞) : Measurable fun a => ∫⁻ b, t.indicator (Function.const (α × β) c) (a, b) ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable fun x => c * (κ x) (Prod.mk x ⁻¹' t)

Tactic:
exact Measurable.const_mul (measurable_kernel_prod_mk_left ht) c

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable fun a => ∫⁻ (b : β), t.indicator (Function.const (α × β) c) (a, b) ∂κ a

Tactic:
conv =>
  congr
  ext
  erw [lintegral_indicator_const_comp measurable_prod_mk_left ht _]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
c : ℝ≥0∞
⊢ Measurable fun x => c * (κ x) (Prod.mk x ⁻¹' t)
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem NF.of_dvd_omega0 {e n a} (h : NF (ONote.oadd e n a)) :
    ω ∣ repr (ONote.oadd e n a) → repr e ≠ 0 ∧ ω ∣ repr a

Proof state:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ ω ∣ (e.oadd n a).repr → e.repr ≠ 0 ∧ ω ∣ a.repr

Tactic:
rw [← opow_one ω, ← one_le_iff_ne_zero]

Result:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ ω ^ 1 ∣ (e.oadd n a).repr → 1 ≤ e.repr ∧ ω ^ 1 ∣ a.repr

Proof state:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ ω ∣ (e.oadd n a).repr → e.repr ≠ 0 ∧ ω ∣ a.repr

Tactic:
(rw [← opow_one ω, ← one_le_iff_ne_zero]; exact h.of_dvd_omega0_opow)

Result:
no goals

Proof state:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ ω ^ 1 ∣ (e.oadd n a).repr → 1 ≤ e.repr ∧ ω ^ 1 ∣ a.repr

Tactic:
exact h.of_dvd_omega0_opow

Result:
no goals
-- Mathlib/Algebra/Group/Operations.lean
@[to_additive]
lemma ite_mul_ite (a b c d : α) :
    ((if P then a else b) * if P then c else d) = if P then a * c else b * d

Proof state:
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a b c d : α
⊢ ((if P then a else b) * if P then c else d) = if P then a * c else b * d

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/Data/FunLike/Equiv.lean
lemma inv_apply_eq_iff_eq_apply {e : E} {b : β} {a : α} : (EquivLike.inv e b) = a ↔ b = e a

Proof state:
E : Sort u_1
α : Sort u_3
β : Sort u_4
inst✝ : EquivLike E α β
e : E
b : β
a : α
⊢ inv e b = a ↔ b = e a

Tactic:
constructor <;> rintro ⟨_, rfl⟩ <;> simp

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

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁵ : GroupWithZero α
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : MulAction α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : 0 < a
⊢ a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂

Tactic:
rw [← smul_le_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
@[simp]
lemma comp_neg [∀ (a : M), (shiftFunctor C a).Additive]
    {a b c : M} (α : ShiftedHom X Y a) (β : ShiftedHom Y Z b) (h : b + a = c) :
    α.comp (-β) h = -α.comp β h

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
X Y Z : C
inst✝¹ : Preadditive C
inst✝ : ∀ (a : M), (shiftFunctor C a).Additive
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ α.comp (-β) h = -α.comp β h

Tactic:
rw [comp, comp, Functor.map_neg, Preadditive.neg_comp, Preadditive.comp_neg]

Result:
no goals
-- Mathlib/Order/PiLex.lean
theorem lex_desc {α} [Preorder ι] [DecidableEq ι] [Preorder α] {f : ι → α} {i j : ι} (h₁ : i ≤ j)
    (h₂ : f j < f i) : toLex (f ∘ Equiv.swap i j) < toLex f :=
  ⟨i, fun _ hik => congr_arg f (Equiv.swap_apply_of_ne_of_ne hik.ne (hik.trans_le h₁).ne), by
    simpa only [Pi.toLex_apply, Function.comp_apply, Equiv.swap_apply_left] using h₂⟩

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : Preorder ι
inst✝¹ : DecidableEq ι
inst✝ : Preorder α
f : ι → α
i j : ι
h₁ : i ≤ j
h₂ : f j < f i
⊢ (fun x x1 x2 => x1 < x2) i (toLex (f ∘ ⇑(Equiv.swap i j)) i) (toLex f i)

Tactic:
simpa only [Pi.toLex_apply, Function.comp_apply, Equiv.swap_apply_left] using h₂

Result:
no goals
-- Mathlib/Topology/Algebra/GroupWithZero.lean
theorem ContinuousOn.div_const (hf : ContinuousOn f s) (y : G₀) :
    ContinuousOn (fun x => f x / y) s

Proof state:
α : Type u_1
G₀ : Type u_3
inst✝³ : DivInvMonoid G₀
inst✝² : TopologicalSpace G₀
inst✝¹ : ContinuousMul G₀
f : α → G₀
s : Set α
inst✝ : TopologicalSpace α
hf : ContinuousOn f s
y : G₀
⊢ ContinuousOn (fun x => f x / y) s

Tactic:
simpa only [div_eq_mul_inv] using hf.mul continuousOn_const

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
protected lemma Connected.mono' {H H' : G.Subgraph}
    (hle : ∀ v w, H.Adj v w → H'.Adj v w) (hv : H.verts = H'.verts)
    (h : H.Connected) : H'.Connected

Proof state:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hle : ∀ (v w : V), H.Adj v w → H'.Adj v w
hv : H.verts = H'.verts
h : H.Connected
⊢ H'.Connected

Tactic:
exact h.mono ⟨hv.le, hle⟩ hv

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem div_sub' {a b c : K} (hc : c ≠ 0) : a / c - b = (a - c * b) / c

Proof state:
K : Type u_1
inst✝ : Field K
a b c : K
hc : c ≠ 0
⊢ a / c - b = (a - c * b) / c

Tactic:
simpa using div_sub_div a b hc one_ne_zero

Result:
no goals
-- Mathlib/Topology/Order/ScottTopology.lean
lemma lowerClosure_subset_closure [IsScott α univ] : ↑(lowerClosure s) ⊆ closure s

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α univ
⊢ Topology.IsUpperSet α

Tactic:
infer_instance

Result:
no goals

Proof state:
case h.e'_3
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α univ
⊢ ↑(lowerClosure s) = closure s

Tactic:
rw [@IsUpperSet.closure_eq_lowerClosure α _ (upperSet α) ?_ s]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α univ
⊢ Topology.IsUpperSet α

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α univ
⊢ ↑(lowerClosure s) ⊆ closure s

Tactic:
convert closure.mono (@upperSet_le_scott α _)

Result:
case h.e'_3
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α univ
⊢ ↑(lowerClosure s) = closure s

case h.e'_4.h.e'_2
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α univ
⊢ inst✝¹ = scott α univ

Proof state:
case h.e'_4.h.e'_2
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α univ
⊢ inst✝¹ = scott α univ

Tactic:
exact topology_eq α univ

Result:
no goals