harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_add_const_Icc : (fun x => x + a) ⁻¹' Icc b c = Icc (b - a) (c - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x + a) ⁻¹' Icc b c = Icc (b - a) (c - a)

Tactic:
simp [← Ici_inter_Iic]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean
lemma opEquiv'_symm_comp (f : Y ⟶ X) {n a : ℤ} (x : Opposite.op (Z⟦a⟧) ⟶ (Opposite.op X⟦n⟧))
    (a' : ℤ) (h : n + a = a') :
    (opEquiv' n a a' h).symm (x ≫ f.op⟦n⟧') = f ≫ (opEquiv' n a a' h).symm x :=
  Quiver.Hom.op_inj (by simp [opEquiv'_symm_apply, opEquiv_symm_apply])

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
f : Y ⟶ X
n a : ℤ
x : Opposite.op ((shiftFunctor C a).obj Z) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ Quiver.Hom.op ((opEquiv' n a a' h).symm (x ≫ (shiftFunctor Cᵒᵖ n).map f.op)) = (f ≫ (opEquiv' n a a' h).symm x).op

Tactic:
simp [opEquiv'_symm_apply, opEquiv_symm_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
theorem CostructuredArrow.overEquivPresheafCostructuredArrow_functor_map_toOverCompCoyoneda
    {A : Cᵒᵖ ⥤ Type v} {T : Over A} {X : CostructuredArrow yoneda A}
    (f : yoneda.obj X ⟶ (overEquivPresheafCostructuredArrow A).functor.obj T) :
    (overEquivPresheafCostructuredArrow A).functor.map
      (((CostructuredArrow.toOverCompCoyoneda A).inv.app (op X)).app T f) =
      (CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).hom.app X ≫ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
T : Over A
X : CostructuredArrow yoneda A
f : yoneda.obj X ⟶ (overEquivPresheafCostructuredArrow A).functor.obj T
⊢ (overEquivPresheafCostructuredArrow A).functor.map (((toOverCompCoyoneda A).inv.app (op X)).app T f) =
    (toOverCompOverEquivPresheafCostructuredArrow A).hom.app X ≫ f

Tactic:
simp [CostructuredArrow.toOverCompCoyoneda]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean
theorem eventually_iff_seq_eventually {ι : Type*} {l : Filter ι} {p : ι → Prop}
    [l.IsCountablyGenerated] :
    (∀ᶠ n in l, p n) ↔ ∀ x : ℕ → ι, Tendsto x atTop l → ∀ᶠ n : ℕ in atTop, p (x n)

Proof state:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)

Tactic:
simpa using tendsto_iff_seq_tendsto (f := id) (l := 𝓟 {x | p x})

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_compl_sum_single (hp : 0 < p.toReal) (f : lp E p) (s : Finset α) :
    ‖f - ∑ i ∈ s, lp.single p i (f i)‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖f i‖ ^ p.toReal

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ ‖f - ∑ i ∈ s, lp.single p i (↑f i)‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal

Tactic:
linarith [lp.norm_sub_norm_compl_sub_single hp f s]

Result:
no goals
-- Mathlib/Data/List/Lemmas.lean
theorem mapAccumr_eq_foldr {σ : Type*} (f : α → σ → σ × β) : ∀ (as : List α) (s : σ),
    mapAccumr f as s = List.foldr (fun a s =>
                                    let r := f a s.1
                                    (r.1, r.2 :: s.2)
                                  ) (s, []) as
  | [], _ => rfl
  | a :: as, s => by
    simp only [mapAccumr, foldr, mapAccumr_eq_foldr f as]

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
f : α → σ → σ × β
a : α
as : List α
s : σ
⊢ mapAccumr f (a :: as) s =
    foldr
      (fun a s =>
        let r := f a s.1;
        (r.1, r.2 :: s.2))
      (s, []) (a :: as)

Tactic:
simp only [mapAccumr, foldr, mapAccumr_eq_foldr f as]

Result:
no goals
-- Mathlib/RepresentationTheory/Character.lean
theorem char_linHom (V W : FDRep k G) (g : G) :
    (of (linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character g

Proof state:
k : Type u
inst✝¹ : Field k
G : Type u
inst✝ : Group G
V W : FDRep k G
g : G
⊢ (of (linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character g

Tactic:
rw [← char_iso (dualTensorIsoLinHom _ _), char_tensor, Pi.mul_apply, char_dual]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma predAbove_pred_of_lt (p i : Fin (n + 1)) (h : i < p) (hp := Fin.ne_zero_of_lt h)
    (hi := Fin.ne_last_of_lt h) : (pred p hp).predAbove i = castPred i hi

Proof state:
n : ℕ
p i : Fin (n + 1)
h : i < p
hp : optParam (p ≠ 0) ⋯
hi : optParam (i ≠ last n) ⋯
⊢ (p.pred hp).predAbove i = i.castPred hi

Tactic:
rw [predAbove_of_lt_succ _ _ (succ_pred _ _ ▸ h)]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem HasColimit.isoOfEquivalence_inv_π {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasColimit G]
    (e : J ≌ K) (w : e.functor ⋙ G ≅ F) (k : K) :
    colimit.ι G k ≫ (HasColimit.isoOfEquivalence e w).inv =
      G.map (e.counitInv.app k) ≫ w.hom.app (e.inverse.obj k) ≫ colimit.ι F (e.inverse.obj k)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
G : K ⥤ C
inst✝ : HasColimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ colimit.ι G k ≫ (isoOfEquivalence e w).inv =
    G.map (e.counitInv.app k) ≫ w.hom.app (e.inverse.obj k) ≫ colimit.ι F (e.inverse.obj k)

Tactic:
simp [HasColimit.isoOfEquivalence, IsColimit.coconePointsIsoOfEquivalence_inv]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem monomial_single_add : monomial (Finsupp.single n e + s) a = X n ^ e * monomial s a

Proof state:
R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
⊢ (monomial (Finsupp.single n e + s)) a = X n ^ e * (monomial s) a

Tactic:
rw [X_pow_eq_monomial, monomial_mul, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
    (h : m.WF) {l : List (α × β)} {k : α}
    (contains_eq_false : (l.map Prod.fst).contains k = false) :
    (insertMany m l).getKey! k = m.getKey! k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
l : List (α × β)
k : α
contains_eq_false : (List.map Prod.fst l).contains k = false
⊢ (insertMany m l).getKey! k = m.getKey! k

Tactic:
simp_to_raw using Raw₀.Const.getKey!_insertMany_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem geom_mean_eq_arith_mean_weighted_of_constant (w z : ι → ℝ) (x : ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
    (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) (hx : ∀ i ∈ s, w i ≠ 0 → z i = x) :
    ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
⊢ ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i

Tactic:
rw [geom_mean_weighted_of_constant, arith_mean_weighted_of_constant] <;> assumption

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem inv_top : (⊤ : Rel α β).inv = (⊤ : Rel β α)

Proof state:
α : Type u_1
β : Type u_2
⊢ ⊤.inv = ⊤

Tactic:
simp [Top.top, inv, Function.flip_def]

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem coassoc_symm_apply (a : A) :
    (TensorProduct.assoc R A A A).symm (comul.lTensor A (comul a)) = comul.rTensor A (comul a)

Proof state:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
⊢ (TensorProduct.assoc R A A A).symm ((LinearMap.lTensor A comul) (comul a)) = (LinearMap.rTensor A comul) (comul a)

Tactic:
rw [(TensorProduct.assoc R A A A).symm_apply_eq, coassoc_apply a]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_add_oangle_rev_neg_left (x y : V) : o.oangle (-x) y + o.oangle (-y) x = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle (-x) y + o.oangle (-y) x = 0

Tactic:
rw [oangle_neg_left_eq_neg_right, oangle_rev, neg_add_cancel]

Result:
no goals
-- Mathlib/Algebra/Divisibility/Units.lean
theorem isRelPrime_mul_unit_right : IsRelPrime (y * x) (z * x) ↔ IsRelPrime y z

Proof state:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (y * x) (z * x) ↔ IsRelPrime y z

Tactic:
rw [isRelPrime_mul_unit_right_left hu, isRelPrime_mul_unit_right_right hu]

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem integralCLM_dirac_eq_delta (x : E) : integralCLM 𝕜 (dirac x) = delta 𝕜 F x

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : SMulCommClass ℝ 𝕜 F
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace F
x : E
⊢ integralCLM 𝕜 (dirac x) = delta 𝕜 F x

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem sOppSide_vadd_right_iff {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) :
    s.SOppSide x (v +ᵥ y) ↔ s.SOppSide x y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.SOppSide x (v +ᵥ y) ↔ s.SOppSide x y

Tactic:
rw [sOppSide_comm, sOppSide_vadd_left_iff hv, sOppSide_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_mul_const_Ioo_of_neg (a b : α) {c : α} (h : c < 0) :
    (fun x => x * c) ⁻¹' Ioo a b = Ioo (b / c) (a / c)

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

Tactic:
simp [← Ioi_inter_Iio, h, inter_comm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
lemma IsHamiltonian.map {H : SimpleGraph β} (f : G →g H) (hf : Bijective f) (hp : p.IsHamiltonian) :
    (p.map f).IsHamiltonian

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
G : SimpleGraph α
a b : α
p : G.Walk a b
H : SimpleGraph β
f : G →g H
hf : Bijective ⇑f
hp : p.IsHamiltonian
⊢ (Walk.map f p).IsHamiltonian

Tactic:
simp [IsHamiltonian, hf.surjective.forall, hf.injective, hp _]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem pmap_eq_map (p : α → Prop) (f : α → β) (o : Option α) (H) :
    @pmap _ _ p (fun a _ => f a) o H = Option.map f o

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : α → β
o : Option α
H : ∀ (a : α), a ∈ o → p a
⊢ pmap (fun a x => f a) o H = Option.map f o

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean
theorem toTensorAlgebra_gOne :
    TensorPower.toTensorAlgebra (@GradedMonoid.GOne.one _ (fun n => ⨂[R]^n M) _ _) = 1

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ toTensorAlgebra GradedMonoid.GOne.one = 1

Tactic:
simp [GradedMonoid.GOne.one, TensorPower.toTensorAlgebra_tprod]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
/-- val_v(0) = 0. -/
lemma count_zero : count K v (0 : FractionalIdeal R⁰ K) = 0

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ count K v 0 = 0

Tactic:
simp only [count, dif_pos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_eq_empty_iff {xs : Array α} {p : α → Bool} : xs.eraseP p = #[] ↔ xs = #[] ∨ ∃ x, p x ∧ xs = #[x]

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ xs.eraseP p = #[] ↔ xs = #[] ∨ ∃ x, p x = true ∧ xs = #[x]

Tactic:
cases xs

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ { toList := toList✝ }.eraseP p = #[] ↔ { toList := toList✝ } = #[] ∨ ∃ x, p x = true ∧ { toList := toList✝ } = #[x]

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ { toList := toList✝ }.eraseP p = #[] ↔ { toList := toList✝ } = #[] ∨ ∃ x, p x = true ∧ { toList := toList✝ } = #[x]

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
/-- A function from a locally finite partial order is monotone if and only if it is monotone when
restricted to pairs satisfying `a ⋖ b`. -/
lemma monotone_iff_forall_covBy [PartialOrder α] [LocallyFiniteOrder α] [Preorder β]
    (f : α → β) : Monotone f ↔ ∀ a b : α, a ⋖ b → f a ≤ f b

Proof state:
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
⊢ Monotone f ↔ ∀ (a b : α), a ⋖ b → f a ≤ f b

Tactic:
refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩

Result:
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
h : ∀ (a b : α), a ⋖ b → f a ≤ f b
a b : α
hab : a ≤ b
⊢ f a ≤ f b
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Assoc.lean
theorem inr_pushoutAssoc_hom [HasPushout (g₃ ≫ (pushout.inr _ _ : X₂ ⟶ Y₁)) g₄]
    [HasPushout g₁ (g₂ ≫ (pushout.inl _ _ : X₂ ⟶ Y₂))] :
    pushout.inr _ _ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom = pushout.inr _ _ ≫ pushout.inr _ _

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom =
    pushout.inr g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)

Tactic:
rw [← Iso.eq_comp_inv, Category.assoc, inr_inr_pushoutAssoc_inv]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem graph_id : graph id = @Eq α

Proof state:
α : Type u_1
⊢ graph id = Eq

Tactic:
simp (config := { unfoldPartialApp := true }) [graph]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma uIoo_comm (a b : α) : uIoo a b = uIoo b a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ uIoo a b = uIoo b a

Tactic:
simp_rw [uIoo, inf_comm, sup_comm]

Result:
no goals
-- Mathlib/Analysis/Convex/Continuous.lean
protected lemma ConcaveOn.locallyLipschitzOn (hC : IsOpen C) (hf : ConcaveOn ℝ C f) :
    LocallyLipschitzOn C f

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
C : Set E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hC : IsOpen C
hf : ConcaveOn ℝ C f
⊢ LocallyLipschitzOn C f

Tactic:
simpa using hf.neg.locallyLipschitzOn hC

Result:
no goals
-- Mathlib/Data/Fintype/Basic.lean
theorem Fin.univ_image_get [DecidableEq α] (l : List α) :
    Finset.univ.image l.get = l.toFinset

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ image l.get univ = l.toFinset

Tactic:
simp [univ_image_def]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_lf_iff {x y : PGame} : -y ⧏ x ↔ -x ⧏ y

Proof state:
x y : PGame
⊢ -y ⧏ x ↔ -x ⧏ y

Tactic:
rw [← neg_neg x, neg_lf_neg_iff, neg_neg]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem finrank_self : finrank R R = 1 :=
  finrank_eq_of_rank_eq (by simp)

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
⊢ Module.rank R R = ↑1

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem not_minimal_iff_exists_lt (hx : P x) : ¬ Minimal P x ↔ ∃ y, y < x ∧ P y

Proof state:
α : Type u_1
P : α → Prop
x : α
inst✝ : Preorder α
hx : P x
⊢ ¬Minimal P x ↔ ∃ y < x, P y

Tactic:
simp_rw [not_minimal_iff hx, lt_iff_le_not_le, and_comm]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
lemma iIndep_iff (m : ι → MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : Measure Ω) :
    iIndep m μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i, i ∈ s → MeasurableSet[m i] (f i)),
      μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Proof state:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ (∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ {s | MeasurableSet s}) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)) ↔
    ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f i)) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Tactic:
rfl

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ iIndep m μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f i)) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Tactic:
simp only [iIndep_iff_iIndepSets, iIndepSets_iff]

Result:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ (∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ {s | MeasurableSet s}) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)) ↔
    ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, MeasurableSet (f i)) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem take_append {l₁ l₂ : List α} (i : Nat) :
    take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ take i l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
i : Nat
⊢ take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ take i l₂

Tactic:
rw [take_append_eq_append_take, take_of_length_le (Nat.le_add_right _ _), Nat.add_sub_cancel_left]

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem ofReal_zero : ENNReal.ofReal (0 : ℝ) = 0

Proof state:
⊢ ENNReal.ofReal 0 = 0

Tactic:
simp [ENNReal.ofReal]

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma CorepresentableBy.homEquiv_symm_comp {F : C ⥤ Type v} {X : C}
    (e : F.CorepresentableBy X) {Y Y' : C} (y : F.obj Y) (g : Y ⟶ Y') :
    e.homEquiv.symm y ≫ g = e.homEquiv.symm (F.map g y) :=
  e.homEquiv.injective (by simp [homEquiv_comp])

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : F.CorepresentableBy X
Y Y' : C
y : F.obj Y
g : Y ⟶ Y'
⊢ e.homEquiv (e.homEquiv.symm y ≫ g) = e.homEquiv (e.homEquiv.symm (F.map g y))

Tactic:
simp [homEquiv_comp]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_zero [RingHomSurjective τ₁₂] : range (0 : M →ₛₗ[τ₁₂] M₂) = ⊥

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
⊢ range 0 = ⊥

Tactic:
simpa only [range_eq_map] using Submodule.map_zero _

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean
theorem convexOn_rpow {p : ℝ} (hp : 1 ≤ p) : ConvexOn ℝ (Ici 0) fun x : ℝ ↦ x ^ p

Proof state:
p : ℝ
hp : 1 ≤ p
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ p

Tactic:
rcases eq_or_lt_of_le hp with (rfl | hp)

Result:
case inl
hp : 1 ≤ 1
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ 1

case inr
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ p

Proof state:
case inr
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ p

Tactic:
exact (strictConvexOn_rpow hp).convexOn

Result:
no goals

Proof state:
case inl
hp : 1 ≤ 1
⊢ ConvexOn ℝ (Ici 0) fun x => x ^ 1

Tactic:
simpa using convexOn_id (convex_Ici _)

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem antitoneOn_iff_antitone : AntitoneOn f s ↔
    Antitone fun a : s => f a

Proof state:
α : Type u
β : Type v
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ AntitoneOn f s ↔ Antitone fun a => f ↑a

Tactic:
simp [Antitone, AntitoneOn]

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
lemma le_egauge_ball_one (x : E) : ‖x‖ₑ ≤ egauge 𝕜 (ball 0 1) x

Proof state:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ‖x‖ₑ ≤ egauge 𝕜 (ball 0 1) x

Tactic:
simpa using div_le_egauge_ball 𝕜 1 x

Result:
no goals
-- Mathlib/Data/Fintype/Perm.lean
theorem card_perms_of_finset : ∀ s : Finset α, #(permsOfFinset s) = (#s)!

Proof state:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
val✝ : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk (⇑(isSetoid α)) l)
⊢ #(permsOfFinset { val := Quot.mk (⇑(isSetoid α)) l, nodup := hs }) =
    (#{ val := Quot.mk (⇑(isSetoid α)) l, nodup := hs })!

Tactic:
exact length_permsOfList l

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (s : Finset α), #(permsOfFinset s) = (#s)!

Tactic:
rintro ⟨⟨l⟩, hs⟩

Result:
case mk.mk
α : Type u_1
inst✝ : DecidableEq α
val✝ : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk (⇑(isSetoid α)) l)
⊢ #(permsOfFinset { val := Quot.mk (⇑(isSetoid α)) l, nodup := hs }) =
    (#{ val := Quot.mk (⇑(isSetoid α)) l, nodup := hs })!
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem smul_inv (r : k) (φ : MvPowerSeries σ k) : (r • φ)⁻¹ = r⁻¹ • φ⁻¹

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
r : k
φ : MvPowerSeries σ k
⊢ (r • φ)⁻¹ = r⁻¹ • φ⁻¹

Tactic:
simp [smul_eq_C_mul, mul_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem existsUnique_zpow_near_of_one_lt' {a : α} (ha : 1 < a) (g : α) :
    ∃! k : ℤ, 1 ≤ g / a ^ k ∧ g / a ^ k < a

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedCommGroup α
inst✝ : MulArchimedean α
a : α
ha : 1 < a
g : α
⊢ ∃! k, 1 ≤ g / a ^ k ∧ g / a ^ k < a

Tactic:
simpa only [one_le_div', zpow_add_one, div_lt_iff_lt_mul'] using
  existsUnique_zpow_near_of_one_lt ha g

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Noetherian.lean
theorem IsHausdorff.of_noZeroSMulDivisors [NoZeroSMulDivisors R M] (h : I ≠ ⊤) : IsHausdorff I M :=
  ⟨fun x hx ↦ (I.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors h).le (by simpa [SModEq.zero] using hx)⟩

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : NoZeroSMulDivisors R M
h : I ≠ ⊤
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
⊢ x ∈ ⨅ i, I ^ i • ⊤

Tactic:
simpa [SModEq.zero] using hx

Result:
no goals
-- Mathlib/CategoryTheory/Idempotents/Basic.lean
theorem idem_of_id_sub_idem [Preadditive C] {X : C} (p : X ⟶ X) (hp : p ≫ p = p) :
    (𝟙 _ - p) ≫ (𝟙 _ - p) = 𝟙 _ - p

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ (𝟙 X - p) ≫ (𝟙 X - p) = 𝟙 X - p

Tactic:
simp only [comp_sub, sub_comp, id_comp, comp_id, hp, sub_self, sub_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_neg_Ioc : Neg.neg '' Ioc a b = Ico (-b) (-a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ Neg.neg '' Ioc a b = Ico (-b) (-a)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Sober.lean
theorem genericPoint_specializes [QuasiSober α] [IrreducibleSpace α] (x : α) : genericPoint α ⤳ x :=
  (IsIrreducible.isGenericPoint_genericPoint_closure _).specializes (by simp)

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSober α
inst✝ : IrreducibleSpace α
x : α
⊢ x ∈ closure univ

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem mem_iff_generator_dvd (S : Ideal R) [S.IsPrincipal] {x : R} : x ∈ S ↔ generator S ∣ x :=
  (mem_iff_eq_smul_generator S).trans (exists_congr fun a => by simp only [mul_comm, smul_eq_mul])

Proof state:
R : Type u
inst✝¹ : CommRing R
S : Ideal R
inst✝ : IsPrincipal S
x a : R
⊢ x = a • generator S ↔ x = generator S * a

Tactic:
simp only [mul_comm, smul_eq_mul]

Result:
no goals
-- Mathlib/Tactic/NormNum/Result.lean
theorem IsNat.to_isInt {α} [Ring α] : ∀ {a : α} {n}, IsNat a n → IsInt a (.ofNat n)
  | _, _, ⟨rfl⟩ => ⟨by simp⟩

Proof state:
α : Type u_1
inst✝ : Ring α
n✝ : ℕ
⊢ ↑n✝ = ↑(Int.ofNat n✝)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Semisimple.lean
@[simp] lemma isSemisimple_neg : (-f).IsSemisimple ↔ f.IsSemisimple

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ (-f).IsSemisimple ↔ f.IsSemisimple

Tactic:
simp [isSemisimple_iff, mem_invtSubmodule]

Result:
no goals