harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean
lemma exp_mul (x : EReal) (y : ℝ) : exp (x * y) = (exp x) ^ y

Proof state:
x : EReal
y : ℝ
⊢ (x * ↑y).exp = x.exp ^ y

Tactic:
rw [← log_eq_iff, log_rpow, log_exp, log_exp, mul_comm]

Result:
no goals
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem projIic_eq_self : projIic b x = ⟨b, le_rfl⟩ ↔ b ≤ x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
b x : α
⊢ projIic b x = ⟨b, ⋯⟩ ↔ b ≤ x

Tactic:
simp [projIic, Subtype.ext_iff]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_eq_bot_iff : a \ b = ⊥ ↔ a ≤ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a \ b = ⊥ ↔ a ≤ b

Tactic:
rw [← le_bot_iff, sdiff_le_iff, sup_bot_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_of_le (h : a ≤ b) : ∫ x in a..b, f x ∂μ = ∫ x in Ioc a b, f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in Ioc a b, f x ∂μ

Tactic:
simp [intervalIntegral, h]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem of_map_inf_le_left [SemilatticeInf α] [Preorder β] {f : α → β}
    (h : ∀ x y, f (x ⊓ y) ≤ f x) : Monotone f

Proof state:
α : Type u
β : Type v
inst✝¹ : SemilatticeInf α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f (x ⊓ y) ≤ f x
⊢ Monotone f

Tactic:
intro x y hxy

Result:
α : Type u
β : Type v
inst✝¹ : SemilatticeInf α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f (x ⊓ y) ≤ f x
x y : α
hxy : x ≤ y
⊢ f x ≤ f y

Proof state:
α : Type u
β : Type v
inst✝¹ : SemilatticeInf α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f (x ⊓ y) ≤ f x
x y : α
hxy : x ≤ y
⊢ f x ≤ f y

Tactic:
rw [← inf_eq_right.2 hxy]

Result:
α : Type u
β : Type v
inst✝¹ : SemilatticeInf α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f (x ⊓ y) ≤ f x
x y : α
hxy : x ≤ y
⊢ f (y ⊓ x) ≤ f y

Proof state:
α : Type u
β : Type v
inst✝¹ : SemilatticeInf α
inst✝ : Preorder β
f : α → β
h : ∀ (x y : α), f (x ⊓ y) ≤ f x
x y : α
hxy : x ≤ y
⊢ f (y ⊓ x) ≤ f y

Tactic:
apply h

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
@[simp] lemma erase_eq : s.erase a = s ↔ a ∉ s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
⊢ s.erase a = s ↔ a ∉ s

Tactic:
rw [← sdiff_singleton]

Result:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
⊢ s.sdiff {a} = s ↔ a ∉ s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
⊢ s.sdiff {a} = s ↔ a ∉ s

Tactic:
simp [-sdiff_singleton]

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Basic.lean
theorem ideal_eq_bot_of_localization' (I : Ideal R)
    (h : ∀ (J : Ideal R) (_ : J.IsMaximal),
      Ideal.map (algebraMap R (Localization.AtPrime J)) I = ⊥) :
    I = ⊥ :=
  Ideal.eq_of_localization_maximal fun P hP => by simpa using h P hP

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : ∀ (J : Ideal R) (x : J.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime J)) I = ⊥
P : Ideal R
hP : P.IsMaximal
⊢ Ideal.map (algebraMap R (Localization.AtPrime P)) I = Ideal.map (algebraMap R (Localization.AtPrime P)) ⊥

Tactic:
simpa using h P hP

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_const_mul_atBot_of_pos (hr : 0 < r) :
    Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atBot

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : 0 < r
⊢ Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atBot

Tactic:
simpa only [← mul_neg, ← tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos hr

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem biprod.lift_desc {T U : C} {f : T ⟶ X} {g : T ⟶ Y} {h : X ⟶ U} {i : Y ⟶ U} :
    biprod.lift f g ≫ biprod.desc h i = f ≫ h + g ≫ i

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
T U : C
f : T ⟶ X
g : T ⟶ Y
h : X ⟶ U
i : Y ⟶ U
⊢ lift f g ≫ desc h i = f ≫ h + g ≫ i

Tactic:
simp [biprod.lift_eq, biprod.desc_eq]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iInf_univ {f : β → α} : ⨅ x ∈ (univ : Set β), f x = ⨅ x, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
⊢ ⨅ x ∈ univ, f x = ⨅ x, f x

Tactic:
simp

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

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

Tactic:
split <;> rfl

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
theorem smul_eq_C_mul (r : K) (x : RatFunc K) : r • x = C r * x

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
r : K
x : RatFunc K
⊢ r • x = C r * x

Tactic:
rw [Algebra.smul_def, algebraMap_eq_C]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem mem_toList {t : RBNode α} : x ∈ t.toList ↔ x ∈ t

Proof state:
α : Type u_1
x : α
t : RBNode α
⊢ x ∈ t.toList ↔ x ∈ t

Tactic:
induction t <;> simp [*, or_left_comm]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Units.lean
theorem closure_ne_top (I : Ideal R) (hI : I ≠ ⊤) : I.closure ≠ ⊤

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
I : Ideal R
hI : I ≠ ⊤
⊢ I.closure ≠ ⊤

Tactic:
have h := closure_minimal (coe_subset_nonunits hI) nonunits.isClosed

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
I : Ideal R
hI : I ≠ ⊤
h : closure ↑I ⊆ nonunits R
⊢ I.closure ≠ ⊤

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
I : Ideal R
hI : I ≠ ⊤
h : closure ↑I ⊆ nonunits R
⊢ I.closure ≠ ⊤

Tactic:
simpa only [I.closure.eq_top_iff_one, Ne] using mt (@h 1) one_not_mem_nonunits

Result:
no goals
-- Mathlib/ModelTheory/LanguageMap.lean
theorem id_comp (F : L →ᴸ L') : LHom.id L' ∘ᴸ F = F

Proof state:
L : Language
L' : Language
F : L →ᴸ L'
⊢ LHom.id L' ∘ᴸ F = F

Tactic:
cases F

Result:
case mk
L : Language
L' : Language
onFunction✝ : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
onRelation✝ : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
⊢ LHom.id L' ∘ᴸ { onFunction := onFunction✝, onRelation := onRelation✝ } =
    { onFunction := onFunction✝, onRelation := onRelation✝ }

Proof state:
case mk
L : Language
L' : Language
onFunction✝ : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
onRelation✝ : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
⊢ LHom.id L' ∘ᴸ { onFunction := onFunction✝, onRelation := onRelation✝ } =
    { onFunction := onFunction✝, onRelation := onRelation✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addY_of_X_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) : W.addY P Q = addU P Q

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W.addY P Q = addU P Q

Tactic:
rw [addU, ← mul_div_mul_right _ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz,
  ← addY_of_X_eq' hP hQ hPz hQz hx, ← pow_succ',
  mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]

Result:
no goals
-- Mathlib/GroupTheory/DoubleCoset.lean
theorem mem_doset {s t : Set α} {a b : α} : b ∈ doset a s t ↔ ∃ x ∈ s, ∃ y ∈ t, b = x * a * y

Proof state:
α : Type u_2
inst✝ : Mul α
s t : Set α
a b : α
⊢ b ∈ doset a s t ↔ ∃ x ∈ s, ∃ y ∈ t, b = x * a * y

Tactic:
simp only [doset_eq_image2, Set.mem_image2, eq_comm]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem sub {M : Type*} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M]
    {v₁ v₂ : VectorMeasure α M} {w : VectorMeasure α N} (hv₁ : v₁ ≪ᵥ w) (hv₂ : v₂ ≪ᵥ w) :
    v₁ - v₂ ≪ᵥ w

Proof state:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(v₁ - v₂) s = 0

Tactic:
rw [sub_apply, hv₁ hs, hv₂ hs, zero_sub, neg_zero]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
⊢ v₁ - v₂ ≪ᵥ w

Tactic:
intro s hs

Result:
α : Type u_1
m : MeasurableSpace α
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : TopologicalSpace N
M : Type u_6
inst✝² : AddCommGroup M
inst✝¹ : TopologicalSpace M
inst✝ : IsTopologicalAddGroup M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(v₁ - v₂) s = 0
-- Mathlib/Topology/DiscreteQuotient.lean
lemma toSetoid_injective : Function.Injective (@toSetoid X _)
  | ⟨_, _⟩, ⟨_, _⟩, _ => by congr

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
toSetoid✝¹ : Setoid X
isOpen_setOf_rel✝¹ : ∀ (x : X), IsOpen (setOf (toSetoid✝¹ x))
toSetoid✝ : Setoid X
isOpen_setOf_rel✝ : ∀ (x : X), IsOpen (setOf (toSetoid✝ x))
x✝ :
  { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ }.toSetoid =
    { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }.toSetoid
⊢ { toSetoid := toSetoid✝¹, isOpen_setOf_rel := isOpen_setOf_rel✝¹ } =
    { toSetoid := toSetoid✝, isOpen_setOf_rel := isOpen_setOf_rel✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_compl' (s : Set α) (f : α → G) :
    mulIndicator sᶜ f = f / mulIndicator s f

Proof state:
α : Type u_1
G : Type u_5
inst✝ : Group G
s : Set α
f : α → G
⊢ sᶜ.mulIndicator f = f / s.mulIndicator f

Tactic:
rw [div_eq_mul_inv, mulIndicator_compl]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
@[reassoc (attr := simp)]
lemma inv_right_hom_right {f g : Under X} (e : f ≅ g) :
    e.inv.right ≫ e.hom.right = 𝟙 g.right

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f g : Under X
e : f ≅ g
⊢ e.inv.right ≫ e.hom.right = 𝟙 g.right

Tactic:
simp [← Under.comp_right]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
theorem inv_left [IsIso sq] : (inv sq).left = inv sq.left :=
  IsIso.eq_inv_of_hom_inv_id <| by rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]

Proof state:
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ sq.left ≫ (inv sq).left = 𝟙 f.left

Tactic:
rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem integralClosure_eq_top_iff : integralClosure R A = ⊤ ↔ Algebra.IsIntegral R A

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ integralClosure R A = ⊤ ↔ Algebra.IsIntegral R A

Tactic:
rw [← top_le_iff, le_integralClosure_iff_isIntegral,
    (Subalgebra.topEquiv (R := R) (A := A)).isIntegral_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem measure_add_measure_compl₀ {s : Set α} (hs : NullMeasurableSet s μ) :
    μ s + μ sᶜ = μ univ

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
⊢ μ s + μ sᶜ = μ univ

Tactic:
rw [← measure_union₀' hs aedisjoint_compl_right, union_compl_self]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem real_smul_posPart_nonneg (r : ℝ) (hr : 0 ≤ r) :
    (r • j).posPart = r.toNNReal • j.posPart

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : 0 ≤ r
⊢ (r • j).posPart = r.toNNReal • j.posPart

Tactic:
rw [real_smul_def, ← smul_posPart, if_pos hr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Sigma.fst)
    {h'} :
    (m.insertMany l).1.getKey k' h' = k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Sigma.fst l
h' : (m.insertMany l).val.contains k' = true
⊢ (m.insertMany l).val.getKey k' h' = k

Tactic:
simp_to_model [insertMany] using List.getKey_insertList_of_mem

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
@[simp] lemma sqrt_eq_zero : sqrt x = 0 ↔ x = 0

Proof state:
x : ℝ≥0
⊢ sqrt x = 0 ↔ x = 0

Tactic:
simp [sqrt_eq_iff_eq_sq]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_at_intCast {S : Type*} [Ring S] (f : R →+* S) (n : ℤ) :
    p.eval₂ f n = f (p.eval n)

Proof state:
case h.e'_2.h.e'_6
R : Type u
inst✝¹ : Ring R
p : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
n : ℤ
⊢ ↑n = f ↑n

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
p : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
n : ℤ
⊢ eval₂ f (↑n) p = f (eval (↑n) p)

Tactic:
convert eval₂_at_apply (p := p) f n

Result:
case h.e'_2.h.e'_6
R : Type u
inst✝¹ : Ring R
p : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
n : ℤ
⊢ ↑n = f ↑n
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_lt_log (hx : 0 < x) (h : x < y) : log x < log y

Proof state:
x y : ℝ
hx : 0 < x
h : x < y
⊢ log x < log y

Tactic:
rwa [← exp_lt_exp, exp_log hx, exp_log (lt_trans hx h)]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem lineMap_eq_right_iff [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c : k} :
    lineMap p₀ p₁ c = p₁ ↔ p₀ = p₁ ∨ c = 1

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AffineSpace V1 P1
inst✝ : NoZeroSMulDivisors k V1
p₀ p₁ : P1
c : k
⊢ (lineMap p₀ p₁) c = p₁ ↔ p₀ = p₁ ∨ c = 1

Tactic:
rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_one]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem isClosed_preimage (h : X ≃ₜ Y) {s : Set Y} : IsClosed (h ⁻¹' s) ↔ IsClosed s

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set Y
⊢ IsClosed (⇑h ⁻¹' s) ↔ IsClosed s

Tactic:
simp only [← isOpen_compl_iff, ← preimage_compl, isOpen_preimage]

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.top : ωScottContinuous (⊤ : α → β) :=
  ωScottContinuous.of_monotone_map_ωSup
    ⟨monotone_const, fun c ↦ eq_of_forall_ge_iff fun a ↦ by simp⟩

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
c : Chain α
a : β
⊢ ⊤ (ωSup c) ≤ a ↔ ωSup (c.map { toFun := ⊤, monotone' := ⋯ }) ≤ a

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Cardinality.lean
theorem cardinalMk_le_max : #L ≤ max #R ℵ₀

Proof state:
R : Type u
inst✝⁵ : CommRing R
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : NoZeroSMulDivisors R L
inst✝ : Algebra.IsAlgebraic R L
⊢ #L ≤ #R ⊔ ℵ₀

Tactic:
simpa only [lift_id] using lift_cardinalMk_le_max R L

Result:
no goals
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem aeconst_comp [MeasurableSingletonClass γ] {f : α → β} (hf : MeasurePreserving f μa μb)
    {g : β → γ} (hg : NullMeasurable g μb) :
    Filter.EventuallyConst (g ∘ f) (ae μa) ↔ Filter.EventuallyConst g (ae μb) :=
  exists_congr fun s ↦ and_congr_left fun hs ↦ by
    simp only [Filter.mem_map, mem_ae_iff, ← hf.measure_preimage (hg hs.measurableSet).compl,
      preimage_comp, preimage_compl]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μa : Measure α
μb : Measure β
inst✝ : MeasurableSingletonClass γ
f : α → β
hf : MeasurePreserving f μa μb
g : β → γ
hg : NullMeasurable g μb
s : Set γ
hs : s.Subsingleton
⊢ s ∈ Filter.map (g ∘ f) (ae μa) ↔ s ∈ Filter.map g (ae μb)

Tactic:
simp only [Filter.mem_map, mem_ae_iff, ← hf.measure_preimage (hg hs.measurableSet).compl,
  preimage_comp, preimage_compl]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem cgf_zero [IsZeroOrProbabilityMeasure μ] : cgf X μ 0 = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsZeroOrProbabilityMeasure μ
⊢ cgf X μ 0 = 0

Tactic:
rcases eq_zero_or_isProbabilityMeasure μ with rfl | h <;> simp [cgf_zero']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem get?_zero (l : List α) : l.get? 0 = l.head?

Proof state:
α : Type u_1
l : List α
⊢ l.get? 0 = l.head?

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/RingTheory/IsTensorProduct.lean
theorem Algebra.pushoutDesc_right [Algebra.IsPushout R S R' S'] {A : Type*} [Semiring A]
    [Algebra R A] (f : S →ₐ[R] A) (g : R' →ₐ[R] A) (H) (x : R') :
    Algebra.pushoutDesc S' f g H (algebraMap R' S' x) = g x

Proof state:
R : Type u_1
S : Type v₃
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring S
inst✝¹¹ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝¹⁰ : CommSemiring R'
inst✝⁹ : CommSemiring S'
inst✝⁸ : Algebra R R'
inst✝⁷ : Algebra S S'
inst✝⁶ : Algebra R' S'
inst✝⁵ : Algebra R S'
inst✝⁴ : IsScalarTower R R' S'
inst✝³ : IsScalarTower R S S'
inst✝² : IsPushout R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : S →ₐ[R] A
g : R' →ₐ[R] A
H : ∀ (x : S) (y : R'), f x * g y = g y * f x
x : R'
⊢ (pushoutDesc S' f g H) ((algebraMap R' S') x) = g x

Tactic:
simp [Algebra.pushoutDesc_apply, Algebra.IsPushout.equiv_symm_algebraMap_right]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem self_lt_rpow_of_one_lt (h₁ : 1 < x) (h₂ : 1 < y) : x < x ^ y

Proof state:
x y : ℝ
h₁ : 1 < x
h₂ : 1 < y
⊢ x < x ^ y

Tactic:
simpa only [rpow_one] using rpow_lt_rpow_of_exponent_lt h₁ h₂

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_eq_false_iff_exists_containsKey [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} :
    l.isEmpty = false ↔ ∃ a, containsKey a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : ReflBEq α
l : List ((a : α) × β a)
⊢ l.isEmpty = false ↔ ∃ a, containsKey a l = true

Tactic:
simp [isEmpty_eq_false_iff_exists_isSome_getEntry?, containsKey_eq_isSome_getEntry?]

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem inter_eq_of_inter_eq_of_eqOn {e' : PartialEquiv α β} (h : e.IsImage s t)
    (h' : e'.IsImage s t) (hs : e.source ∩ s = e'.source ∩ s) (heq : EqOn e e' (e.source ∩ s)) :
    e.target ∩ t = e'.target ∩ t

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
h' : e'.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e) (↑e') (e.source ∩ s)
⊢ e.target ∩ t = e'.target ∩ t

Tactic:
rw [← h.image_eq, ← h'.image_eq, ← hs, heq.image_eq]

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem stereographic'_target {n : ℕ} [Fact (finrank ℝ E = n + 1)] (v : sphere (0 : E) 1) :
    (stereographic' n v).target = Set.univ

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ (stereographic' n v).target = Set.univ

Tactic:
simp [stereographic']

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
lemma leadingCoeff_mul_C_of_isUnit (ha : IsUnit a) (p : R[X]) :
    (p * C a).leadingCoeff = p.leadingCoeff * a

Proof state:
R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (p * C a).leadingCoeff = p.leadingCoeff * a

Tactic:
rwa [leadingCoeff, coeff_mul_C, natDegree_mul_C_of_isUnit, leadingCoeff]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem singleton_mul_mem_nhds (a : α) {b : α} (h : s ∈ 𝓝 b) : {a} * s ∈ 𝓝 (a * b)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul α α
s : Set α
a b : α
h : s ∈ 𝓝 b
⊢ {a} * s ∈ 𝓝 (a * b)

Tactic:
rwa [← smul_eq_mul, ← smul_eq_mul, singleton_smul, smul_mem_nhds_smul_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_mul_Ioc (a b : α) {c : α} (h : 0 < c) :
    (c * ·) ⁻¹' Ioc a b = Ioc (a / c) (b / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : 0 < c
⊢ (fun x => c * x) ⁻¹' Ioc a b = Ioc (a / c) (b / c)

Tactic:
simp [← Ioi_inter_Iic, h]

Result:
no goals
-- Mathlib/Data/Nat/Find.lean
lemma findGreatest_eq_zero_iff : Nat.findGreatest P k = 0 ↔ ∀ ⦃n⦄, 0 < n → n ≤ k → ¬P n

Proof state:
k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n

Tactic:
simp [findGreatest_eq_iff]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_eq (hf : IsFundamentalSequence a o f) : a.cof.ord = o :=
  hf.1.antisymm' <| by
    rw [← hf.2.2]
    exact (ord_le_ord.2 (cof_blsub_le f)).trans (ord_card_le o)

Proof state:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
⊢ a.cof.ord ≤ o

Tactic:
rw [← hf.2.2]

Result:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
⊢ (o.blsub f).cof.ord ≤ o

Proof state:
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
⊢ (o.blsub f).cof.ord ≤ o

Tactic:
exact (ord_le_ord.2 (cof_blsub_le f)).trans (ord_card_le o)

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsRatCondKernelCDF.tendsto_atBot_zero (hf : IsRatCondKernelCDF f κ ν) (a : α) :
    ∀ᵐ b ∂(ν a), Tendsto (f (a, b)) atBot (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
⊢ ∀ᵐ (b : β) ∂ν a, Tendsto (f (a, b)) atBot (𝓝 0)

Tactic:
filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.tendsto_atBot_zero

Result:
no goals
-- Mathlib/Data/Nat/PrimeFin.lean
lemma primeFactors_mul (ha : a ≠ 0) (hb : b ≠ 0) :
    (a * b).primeFactors = a.primeFactors ∪ b.primeFactors

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).primeFactors = a.primeFactors ∪ b.primeFactors

Tactic:
ext

Result:
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ a✝ ∈ (a * b).primeFactors ↔ a✝ ∈ a.primeFactors ∪ b.primeFactors

Proof state:
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
a✝ : ℕ
⊢ a✝ ∈ (a * b).primeFactors ↔ a✝ ∈ a.primeFactors ∪ b.primeFactors

Tactic:
simp only [Finset.mem_union, mem_primeFactors_iff_mem_primeFactorsList,
mem_primeFactorsList_mul ha hb]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem posDef_toMatrix' [DecidableEq n] {Q : QuadraticForm ℝ (n → ℝ)} (hQ : Q.PosDef) :
    Q.toMatrix'.PosDef

Proof state:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ :
  (LinearMap.BilinMap.toQuadraticMap
      ((LinearMap.toMatrix₂' ℝ).invFun ((↑(LinearMap.toMatrix₂' ℝ)).toFun ((associatedHom ℝ) Q)))).PosDef
⊢ (toMatrix' Q).PosDef

Tactic:
exact .of_toQuadraticForm' (isSymm_toMatrix' Q) hQ

Result:
no goals

Proof state:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : PosDef Q
⊢ (toMatrix' Q).PosDef

Tactic:
rw [← toQuadraticMap_associated ℝ Q, ←
  (LinearMap.toMatrix₂' ℝ).left_inv ((associatedHom (R := ℝ) ℝ) Q)] at hQ

Result:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ :
  (LinearMap.BilinMap.toQuadraticMap
      ((LinearMap.toMatrix₂' ℝ).invFun ((↑(LinearMap.toMatrix₂' ℝ)).toFun ((associatedHom ℝ) Q)))).PosDef
⊢ (toMatrix' Q).PosDef