harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/PiSystem.lean
theorem isPiSystem_Icc_mem (s t : Set α) :
    IsPiSystem { S | ∃ᵉ (l ∈ s) (u ∈ t), l ≤ u ∧ Icc l u = S } :=
  isPiSystem_Ixx_mem (Ixx := Icc) nonempty_Icc.1 (by exact Icc_inter_Icc) s t

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
⊢ ∀ {a₁ b₁ a₂ b₂ : α}, Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Tactic:
exact Icc_inter_Icc

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean
@[reassoc, to_app]
lemma whiskerLeft_mapId_hom (f : a ⟶ b) : F.map f ◁ (F.mapId b).hom =
    (F.mapComp f (𝟙 b)).inv ≫ F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : Pseudofunctor B C
a b : B
f : a ⟶ b
⊢ F.map f ◁ (F.mapId b).hom = (F.mapComp f (𝟙 b)).inv ≫ F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv

Tactic:
simp [whiskerLeftIso_mapId]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedHahn.lean
theorem restrictNonposSeq_measurableSet (n : ℕ) :
    MeasurableSet (restrictNonposSeq s i n)

Proof state:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ MeasurableSet
    (MeasureTheory.SignedMeasure.someExistsOneDivLT s
      (i \
        ⋃ k,
          ⋃ (H : k ≤ n✝),
            let_fun this := ⋯;
            MeasureTheory.SignedMeasure.restrictNonposSeq s i k))

Tactic:
exact someExistsOneDivLT_measurableSet

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ MeasurableSet (MeasureTheory.SignedMeasure.restrictNonposSeq s i (n✝ + 1))

Tactic:
rw [restrictNonposSeq]

Result:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α
n✝ : ℕ
⊢ MeasurableSet
    (MeasureTheory.SignedMeasure.someExistsOneDivLT s
      (i \
        ⋃ k,
          ⋃ (H : k ≤ n✝),
            let_fun this := ⋯;
            MeasureTheory.SignedMeasure.restrictNonposSeq s i k))
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem log_inv (x : ℂ) (hx : x.arg ≠ π) : log x⁻¹ = -log x

Proof state:
x : ℂ
hx : x.arg ≠ π
⊢ log x⁻¹ = -log x

Tactic:
rw [log_inv_eq_ite, if_neg hx]

Result:
no goals
-- Mathlib/Data/Rat/Floor.lean
theorem ceil_intCast_div_natCast (n : ℤ) (d : ℕ) : ⌈(↑n / ↑d : ℚ)⌉ = -((-n) / (↑d : ℤ))

Proof state:
n : ℤ
d : ℕ
⊢ ⌈↑n / ↑d⌉ = -(-n / ↑d)

Tactic:
conv_lhs => rw [← neg_neg ⌈_⌉, ← floor_neg]

Result:
n : ℤ
d : ℕ
⊢ -⌊-(↑n / ↑d)⌋ = -(-n / ↑d)

Proof state:
n : ℤ
d : ℕ
⊢ -⌊-(↑n / ↑d)⌋ = -(-n / ↑d)

Tactic:
rw [← neg_div, ← Int.cast_neg, floor_intCast_div_natCast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range'_concat (s n : Nat) : range' s (n + 1) step = range' s n step ++ [s + step * n]

Proof state:
step s n : Nat
⊢ range' s (n + 1) step = range' s n step ++ [s + step * n]

Tactic:
exact (range'_append s n 1 step).symm

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem transvection_mul_transvection_same (h : i ≠ j) (c d : R) :
    transvection i j c * transvection i j d = transvection i j (c + d)

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
h : i ≠ j
c d : R
⊢ transvection i j c * transvection i j d = transvection i j (c + d)

Tactic:
simp [transvection, Matrix.add_mul, Matrix.mul_add, h, h.symm, add_smul, add_assoc,
  stdBasisMatrix_add]

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
lemma units_coeff_zero_smul (c : R[X]ˣ) (p : R[X]) : (c : R[X]).coeff 0 • p = c * p

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
c : R[X]ˣ
p : R[X]
⊢ (↑c).coeff 0 • p = ↑c * p

Tactic:
rw [← Polynomial.C_mul', ← Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive (attr := simp)]
lemma one_mem_inv_mul_iff : (1 : α) ∈ t⁻¹ * s ↔ ¬Disjoint s t

Proof state:
α : Type u_2
inst✝ : Group α
s t : Set α
⊢ 1 ∈ t⁻¹ * s ↔ ¬Disjoint s t

Tactic:
aesop (add simp [not_disjoint_iff_nonempty_inter, mem_mul, mul_eq_one_iff_eq_inv, Set.Nonempty])

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem d_pos : 0 < d a1 :=
  tsub_pos_of_lt (mul_lt_mul a1 (le_of_lt a1) (by decide) (Nat.zero_le _) : 1 * 1 < a * a)

Proof state:
a : ℕ
a1 : 1 < a
⊢ 0 < 1

Tactic:
decide

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem completeSpace_iff (e : α ≃ᵢ β) : CompleteSpace α ↔ CompleteSpace β

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
e : α ≃ᵢ β
⊢ CompleteSpace α ↔ CompleteSpace β

Tactic:
simp only [completeSpace_iff_isComplete_univ, ← e.range_eq_univ, ← image_univ,
  isComplete_image_iff e.isometry.isUniformInducing]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_inv_le_iff {x y : ℝ≥0} {z : ℝ} (hz : 0 < z) : x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

Proof state:
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

Tactic:
rw [← rpow_le_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz.ne']

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Base.lean
@[simp]
lemma span_root_support :
    span R (P.root '' b.support) = P.rootSpan

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
b : P.Base
⊢ span R (⇑P.root '' b.support) = P.rootSpan

Tactic:
rw [← span_span_of_tower (R := ℤ), span_int_root_support, span_span_of_tower]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem Basis.toMatrix_map (b : Basis ι R M) (f : M ≃ₗ[R] N) (v : ι → N) :
    (b.map f).toMatrix v = b.toMatrix (f.symm ∘ v)

Proof state:
ι : Type u_1
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b : Basis ι R M
f : M ≃ₗ[R] N
v : ι → N
⊢ (b.map f).toMatrix v = b.toMatrix (⇑f.symm ∘ v)

Tactic:
ext

Result:
case a
ι : Type u_1
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b : Basis ι R M
f : M ≃ₗ[R] N
v : ι → N
i✝ j✝ : ι
⊢ (b.map f).toMatrix v i✝ j✝ = b.toMatrix (⇑f.symm ∘ v) i✝ j✝
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem rnDeriv_smul_left_of_ne_top (ν μ : Measure α) [IsFiniteMeasure ν]
    [ν.HaveLebesgueDecomposition μ] {r : ℝ≥0∞} (hr : r ≠ ∞) :
    (r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ ⊤
h : (r.toNNReal • ν).rnDeriv μ =ᶠ[ae μ] r.toNNReal • ν.rnDeriv μ
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ

Tactic:
simpa [ENNReal.smul_def, ENNReal.coe_toNNReal hr] using h

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ ⊤
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ

Tactic:
have h : (r.toNNReal • ν).rnDeriv μ =ᵐ[μ] r.toNNReal • ν.rnDeriv μ :=
  rnDeriv_smul_left ν μ r.toNNReal

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0∞
hr : r ≠ ⊤
h : (r.toNNReal • ν).rnDeriv μ =ᶠ[ae μ] r.toNNReal • ν.rnDeriv μ
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem rat_add_continuous_lemma {ε : α} (ε0 : 0 < ε) :
    ∃ δ > 0, ∀ {a₁ a₂ b₁ b₂ : β}, abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ →
      abv (a₁ + a₂ - (b₁ + b₂)) < ε :=
  ⟨ε / 2, half_pos ε0, fun {a₁ a₂ b₁ b₂} h₁ h₂ => by
    simpa [add_halves, sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using
      lt_of_le_of_lt (abv_add abv _ _) (add_lt_add h₁ h₂)⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
ε : α
ε0 : 0 < ε
a₁ a₂ b₁ b₂ : β
h₁ : abv (a₁ - b₁) < ε / 2
h₂ : abv (a₂ - b₂) < ε / 2
⊢ abv (a₁ + a₂ - (b₁ + b₂)) < ε

Tactic:
simpa [add_halves, sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using
  lt_of_le_of_lt (abv_add abv _ _) (add_lt_add h₁ h₂)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_modify_self (h : m.1.WF) {k : α} {fallback : β} {f : β → β} :
    Const.getD (Const.modify m k f) k fallback = ((Const.get? m k).map f).getD fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k : α
fallback : β
f : β → β
⊢ getD (modify m k f) k fallback = (Option.map f (get? m k)).getD fallback

Tactic:
simp_to_model [Const.modify] using List.Const.getValueD_modifyKey_self

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
theorem one_lt_mul_iff : 1 < a * b ↔ 1 < a ∨ 1 < b

Proof state:
α : Type u
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedMul α
a b : α
⊢ 1 < a * b ↔ 1 < a ∨ 1 < b

Tactic:
simp only [one_lt_iff_ne_one, Ne, mul_eq_one, not_and_or]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma exactAt_of_isGE (n i : ℤ) (hi : i < n) [K.IsGE n] :
    K.ExactAt i :=
  exactAt_of_isSupported K (embeddingUpIntGE n) i
    (by simpa only [not_mem_range_embeddingUpIntGE_iff] using hi)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
n i : ℤ
hi : i < n
inst✝ : K.IsGE n
⊢ ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i

Tactic:
simpa only [not_mem_range_embeddingUpIntGE_iff] using hi

Result:
no goals
-- Mathlib/CategoryTheory/Localization/DerivabilityStructure/Basic.lean
lemma guitartExact_of_isRightDerivabilityStructure' [h : Φ.IsRightDerivabilityStructure]
    (e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F) : TwoSquare.GuitartExact e.hom

Proof state:
C₁ : Type u₁
C₂ : Type u₂
inst✝⁵ : Category.{v₁, u₁} C₁
inst✝⁴ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝³ : Category.{u_4, u_1} D₁
inst✝² : Category.{u_3, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₁.IsLocalization W₁
inst✝ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
h : Φ.IsRightDerivabilityStructure
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
⊢ TwoSquare.GuitartExact e.hom

Tactic:
simpa only [Φ.isRightDerivabilityStructure_iff L₁ L₂ F e] using h

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem insert_diff_self_of_not_mem {a : α} {s : Set α} (h : a ∉ s) : insert a s \ {a} = s

Proof state:
α : Type u
a : α
s : Set α
h : a ∉ s
⊢ insert a s \ {a} = s

Tactic:
ext x

Result:
case h
α : Type u
a : α
s : Set α
h : a ∉ s
x : α
⊢ x ∈ insert a s \ {a} ↔ x ∈ s
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma P24_neg_right : P24 x₁ x₂ y ↔ P24 x₁ x₂ (-y)

Proof state:
x₁ x₂ y : PGame
⊢ P24 x₁ x₂ y ↔ P24 x₁ x₂ (-y)

Tactic:
rw [P24, P24, P2_neg_right, P4_neg_right]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Completion.lean
theorem lim_mul (f : CauSeq β abv) (x : β) : lim f * x = lim (f * const abv x)

Proof state:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
x : β
⊢ f.lim * x = (f * const abv x).lim

Tactic:
rw [← lim_mul_lim, lim_const]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem isOpen_uniformity {s : Set α} :
    IsOpen s ↔ ∀ x ∈ s, { p : α × α | p.1 = x → p.2 ∈ s } ∈ 𝓤 α

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ IsOpen s ↔ ∀ x ∈ s, {p | p.1 = x → p.2 ∈ s} ∈ 𝓤 α

Tactic:
simp only [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap_prod_mk]

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

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

Tactic:
simpa only [neg_mul, tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos (neg_pos.2 hr)

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma add_div_of_nonneg_right (h : 0 ≤ c) :
    (a + b) / c = a / c + b / c

Proof state:
a b c : EReal
h : 0 ≤ c
⊢ (a + b) / c = a / c + b / c

Tactic:
apply right_distrib_of_nonneg_of_ne_top (inv_nonneg_of_nonneg h) (inv_lt_top c).ne

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_iUnion_mem_option {ι : Type*} (o : Option ι) (s : ι → Set α) :
    (⋃ i ∈ o, s i).einfsep = ⨅ i ∈ o, (s i).einfsep

Proof state:
α : Type u_1
inst✝ : EDist α
ι : Type u_3
o : Option ι
s : ι → Set α
⊢ (⋃ i ∈ o, s i).einfsep = ⨅ i ∈ o, (s i).einfsep

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zip_unzip (l : Vector (α × β) n) : zip (unzip l).1 (unzip l).2 = l

Proof state:
case mk
α : Type u_1
β : Type u_2
l : Array (α × β)
⊢ { toArray := l, size_toArray := ⋯ }.unzip.fst.zip { toArray := l, size_toArray := ⋯ }.unzip.snd =
    { toArray := l, size_toArray := ⋯ }

Tactic:
simp only [unzip_mk, mk_zip_mk, Array.zip_unzip]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
l : Vector (α × β) n
⊢ l.unzip.fst.zip l.unzip.snd = l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
l : Array (α × β)
⊢ { toArray := l, size_toArray := ⋯ }.unzip.fst.zip { toArray := l, size_toArray := ⋯ }.unzip.snd =
    { toArray := l, size_toArray := ⋯ }
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Sized.rotateR_size {l x r} (hl : Sized l) :
    size (@Ordnode.rotateR α l x r) = size l + size r + 1

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Sized
⊢ (l.rotateR x r).size = l.size + r.size + 1

Tactic:
rw [← size_dual, dual_rotateR, hl.dual.rotateL_size, size_dual, size_dual, add_comm (size l)]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
lemma biprod.ext_from_iff {f g : X ⊞ Y ⟶ Z} :
    f = g ↔ biprod.inl ≫ f = biprod.inl ≫ g ∧ biprod.inr ≫ f = biprod.inr ≫ g

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
inst✝ : HasBinaryBiproduct X Y
Z : C
f g : X ⊞ Y ⟶ Z
⊢ f = g ↔ inl ≫ f = inl ≫ g ∧ inr ≫ f = inr ≫ g

Tactic:
aesop

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem swap_eq_update (i j : α) : (Equiv.swap i j : α → α) = update (update id j i) i j :=
  funext fun x => by rw [update_apply _ i j, update_apply _ j i, Equiv.swap_apply_def, id]

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
i j x : α
⊢ (swap i j) x = update (update id j i) i j x

Tactic:
rw [update_apply _ i j, update_apply _ j i, Equiv.swap_apply_def, id]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem valid : ∀ {it}, ValidFor l r it → Valid it
  | _, ⟨⟩ => by simpa [List.reverseAux_eq] using Pos.Valid.mk l.reverse r

Proof state:
l r : List Char
⊢ { s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l } }.Valid

Tactic:
simpa [List.reverseAux_eq] using Pos.Valid.mk l.reverse r

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial.lean
theorem rank_eq {σ : Type v} : Module.rank K (MvPolynomial σ K) = #(σ →₀ ℕ)

Proof state:
K : Type v
inst✝¹ : CommRing K
inst✝ : Nontrivial K
σ : Type v
⊢ Module.rank K (MvPolynomial σ K) = #(σ →₀ ℕ)

Tactic:
rw [← Cardinal.lift_inj, ← (basisMonomials σ K).mk_eq_rank]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
lemma mem_asIdealOpposite {I : TwoSidedIdeal R} {x : Rᵐᵒᵖ} :
    x ∈ asIdealOpposite I ↔ x.unop ∈ I

Proof state:
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
x : Rᵐᵒᵖ
⊢ x ∈ asIdealOpposite I ↔ MulOpposite.unop x ∈ I

Tactic:
simpa [asIdealOpposite, asIdeal, TwoSidedIdeal.mem_iff, RingCon.op_iff] using
  ⟨I.ringCon.symm, I.ringCon.symm⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem nodalWeight_eq_eval_nodal_derative (hi : i ∈ s) :
    nodalWeight s v i = (eval (v i) (Polynomial.derivative (nodal s v)))⁻¹

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hi : i ∈ s
⊢ nodalWeight s v i = (eval (v i) (derivative (nodal s v)))⁻¹

Tactic:
rw [eval_nodal_derivative_eval_node_eq hi, nodalWeight_eq_eval_nodal_erase_inv]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem sum_divisors_eq_sum_properDivisors_add_self :
    ∑ i ∈ divisors n, i = (∑ i ∈ properDivisors n, i) + n

Proof state:
n : ℕ
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
rcases Decidable.eq_or_ne n 0 with (rfl | hn)

Result:
case inl

⊢ ∑ i ∈ divisors 0, i = ∑ i ∈ properDivisors 0, i + 0

case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Proof state:
case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i ∈ n.divisors, i = ∑ i ∈ n.properDivisors, i + n

Tactic:
rw [← cons_self_properDivisors hn, Finset.sum_cons, add_comm]

Result:
no goals

Proof state:
case inl

⊢ ∑ i ∈ divisors 0, i = ∑ i ∈ properDivisors 0, i + 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem ne_zero_of_unit [Nontrivial Γ₀] (v : Valuation K Γ₀) (x : Kˣ) : v x ≠ (0 : Γ₀)

Proof state:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : Nontrivial Γ₀
v : Valuation K Γ₀
x : Kˣ
⊢ v ↑x ≠ 0

Tactic:
simp only [ne_eq, Valuation.zero_iff, Units.ne_zero x, not_false_iff]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
lemma expect_eq_zero_iff_of_nonneg (hs : s.Nonempty) (hf : ∀ i ∈ s, 0 ≤ f i) :
    𝔼 i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : OrderedAddCommMonoid α
inst✝ : Module ℚ≥0 α
s : Finset ι
f : ι → α
hs : s.Nonempty
hf : ∀ i ∈ s, 0 ≤ f i
⊢ 𝔼 i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0

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

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
@[simp] lemma mem_Icc : x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b

Tactic:
rw [Icc, ← Finset.mem_def, Finset.mem_Icc]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean
@[reassoc (attr := simp)]
lemma ι_fromFreeYonedaCoproduct (m : M.Elements) :
    M.ιFreeYonedaCoproduct m ≫ M.fromFreeYonedaCoproduct = m.fromFreeYoneda

Proof state:
C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ M.ιFreeYonedaCoproduct m ≫ M.fromFreeYonedaCoproduct = m.fromFreeYoneda

Tactic:
apply Sigma.ι_desc

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem ker_restrict [AddCommMonoid M₁] [Module R M₁] {p : Submodule R M} {q : Submodule R M₁}
    {f : M →ₗ[R] M₁} (hf : ∀ x : M, x ∈ p → f x ∈ q) :
    ker (f.restrict hf) = (ker f).comap p.subtype

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
p : Submodule R M
q : Submodule R M₁
f : M →ₗ[R] M₁
hf : ∀ x ∈ p, f x ∈ q
⊢ ker (f.restrict hf) = comap p.subtype (ker f)

Tactic:
rw [restrict_eq_codRestrict_domRestrict, ker_codRestrict, ker_domRestrict]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replace_of_not_mem {l : List α} (h : !l.elem a) : l.replace a b = l

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
l : List α
h : (!elem a l) = true
⊢ l.replace a b = l

Tactic:
induction l <;> simp_all [replace_cons]

Result:
no goals
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem alternatization_apply (m : MultilinearMap R (fun _ : ι => M) N') (v : ι → M) :
    alternatization m v = ∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ v

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : MultilinearMap R (fun x => M) N'
v : ι → M
⊢ (alternatization m) v = ∑ σ : Perm ι, Perm.sign σ • (domDomCongr σ m) v

Tactic:
simp only [alternatization_def, smul_apply, sum_apply]

Result:
no goals
-- Mathlib/Algebra/Star/Basic.lean
theorem IsLeftRegular.star [Mul R] [StarMul R] {x : R} (hx : IsLeftRegular x) :
    IsRightRegular (star x) :=
  fun a b h => star_injective <| hx <| by simpa using congr_arg Star.star h

Proof state:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
hx : IsLeftRegular x
a b : R
h : (fun x_1 => x_1 * star x) a = (fun x_1 => x_1 * star x) b
⊢ (fun x_1 => x * x_1) (star a) = (fun x_1 => x * x_1) (star b)

Tactic:
simpa using congr_arg Star.star h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem foldlM_toList [Monad m]
    (f : β → α → m β) (init : β) (arr : Array α) :
    arr.toList.foldlM f init = arr.foldlM f init

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
init : β
arr : Array α
⊢ List.foldlM f init arr.toList = foldlM f init arr

Tactic:
simp [foldlM, foldlM_toList.aux]

Result:
no goals
-- Mathlib/Order/ModularLattice.lean
theorem isModularLattice_iff_inf_sup_inf_assoc [Lattice α] :
    IsModularLattice α ↔ ∀ x y z : α, x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z :=
  ⟨fun h => @IsModularLattice.inf_sup_inf_assoc _ _ h, fun h =>
    ⟨fun y z xz => by rw [← inf_eq_left.2 xz, h]⟩⟩

Proof state:
α : Type u_1
inst✝ : Lattice α
h : ∀ (x y z : α), x ⊓ z ⊔ y ⊓ z = (x ⊓ z ⊔ y) ⊓ z
x✝ y z : α
xz : x✝ ≤ z
⊢ (x✝ ⊔ y) ⊓ z ≤ x✝ ⊔ y ⊓ z

Tactic:
rw [← inf_eq_left.2 xz, h]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_eq_self_iff_disjoint' : x \ y = x ↔ Disjoint x y

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y = x ↔ Disjoint x y

Tactic:
rw [sdiff_eq_self_iff_disjoint, disjoint_comm]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Adjoin.lean
theorem aevalEquivField_algebraMap_apply_coe (a : MvPolynomial ι F) :
    hx.aevalEquivField (algebraMap _ _ a) = aeval x a

Proof state:
ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : AlgebraicIndependent F x
a : MvPolynomial ι F
⊢ ↑(hx.aevalEquivField ((algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F))) a)) = (aeval x) a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Continuity.lean
theorem tendsto_norm_div_self (x : E) : Tendsto (fun a => ‖a / x‖) (𝓝 x) (𝓝 0)

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ Tendsto (fun a => ‖a / x‖) (𝓝 x) (𝓝 0)

Tactic:
simpa [dist_eq_norm_div] using
  tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (x : E)) (𝓝 x) _)

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
/-- This allows us to get `NormedAddCommGroup` and `NormedSpace` instances on `E` via
`NormedAddCommGroup.ofCore` and `NormedSpace.ofCore`. -/
lemma normedSpaceCore : NormedSpace.Core ℂ E where
  norm_nonneg _ := CStarModule.norm_nonneg
  norm_eq_zero_iff x := norm_zero_iff x
  norm_smul c x

Proof state:
A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
c : ℂ
x : E
⊢ ‖c •> x‖ = ‖c‖ * ‖x‖

Tactic:
simp [norm_eq_sqrt_norm_inner_self, norm_smul, ← mul_assoc]

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem isWF_insert {a} : IsWF (insert a s) ↔ IsWF s

Proof state:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
⊢ (insert a s).IsWF ↔ s.IsWF

Tactic:
simp only [← singleton_union, isWF_union, isWF_singleton, true_and]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem eq_nil_iff_forall_not_mem {l : List α} : l = [] ↔ ∀ a, a ∉ l

Proof state:
α : Type u_1
l : List α
⊢ l = [] ↔ ∀ (a : α), ¬a ∈ l

Tactic:
cases l <;> simp [-not_or]

Result:
no goals