harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Maps/Basic.lean
theorem id : IsClosedMap (@id X) := fun s hs => by rwa [image_id]

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ IsClosed (id '' s)

Tactic:
rwa [image_id]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma stableUnderGeneralization_singleton {x : PrimeSpectrum R} :
    StableUnderGeneralization {x} ↔ x.asIdeal ∈ minimalPrimes R

Proof state:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ a ≤ x, a = x) ↔ IsMin x

Tactic:
exact ⟨fun H a h ↦ (H a h).ge, fun H a h ↦ le_antisymm h (H h)⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ StableUnderGeneralization {x} ↔ x.asIdeal ∈ minimalPrimes R

Tactic:
simp_rw [← isMin_iff, StableUnderGeneralization, ← le_iff_specializes, Set.mem_singleton_iff,
  @forall_comm _ (_ = _), forall_eq]

Result:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ a ≤ x, a = x) ↔ IsMin x
-- Mathlib/Algebra/Homology/ComplexShape.lean
lemma next_eq_self' (c : ComplexShape ι) (j : ι) (hj : ∀ k, ¬ c.Rel j k) :
    c.next j = j :=
  dif_neg (by simpa using hj)

Proof state:
ι : Type u_1
c : ComplexShape ι
j : ι
hj : ∀ (k : ι), ¬c.Rel j k
⊢ ¬∃ j_1, c.Rel j j_1

Tactic:
simpa using hj

Result:
no goals
-- Mathlib/Data/List/Destutter.lean
theorem destutter'_cons_neg (h : ¬R b a) : (a :: l).destutter' R b = l.destutter' R b

Proof state:
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : ¬R b a
⊢ destutter' R b (a :: l) = destutter' R b l

Tactic:
rw [destutter', if_neg h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
@[simp]
lemma ideal_iInf {ι : Type*} (I : ι → IdealSheafData X) [Finite ι] :
    (⨅ i, I i).ideal = ⨅ i, (I i).ideal

Proof state:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
inst✝ : Finite ι
⊢ (⨅ i, I i).ideal = ⨅ i, (I i).ideal

Tactic:
simpa using ideal_biInf I Set.finite_univ

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
@[simp] nonrec lemma iInf_of_isEmpty [IsEmpty ι] (f : ι → ℝ) : ⨅ i, f i = 0

Proof state:
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ ⨅ i, f i = 0

Tactic:
rw [iInf_of_isEmpty, sInf_empty]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
@[simp] protected lemma inv_one (n : ℕ) : (1⁻¹ : ZMod n) = 1

Proof state:
case inr
n : ℕ
hn : n ≠ 1
⊢ 1⁻¹ = 1

Tactic:
simpa [ZMod.val_one'' hn] using mul_inv_eq_gcd (1 : ZMod n)

Result:
no goals

Proof state:
case inl

⊢ 1⁻¹ = 1

Tactic:
exact Subsingleton.elim _ _

Result:
no goals

Proof state:
n : ℕ
⊢ 1⁻¹ = 1

Tactic:
obtain rfl | hn := eq_or_ne n 1

Result:
case inl

⊢ 1⁻¹ = 1

case inr
n : ℕ
hn : n ≠ 1
⊢ 1⁻¹ = 1
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem sInter_singleton {x : ZFSet.{u}} : ⋂₀ ({x} : ZFSet) = x :=
  ext fun y => by simp_rw [mem_sInter (singleton_nonempty x), mem_singleton, forall_eq]

Proof state:
x y : ZFSet.{u}
⊢ y ∈ ⋂₀ {x} ↔ y ∈ x

Tactic:
simp_rw [mem_sInter (singleton_nonempty x), mem_singleton, forall_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem subNatNat_add_left : subNatNat (m + n) m = n

Proof state:
m n : Nat
⊢ subNatNat (m + n) m = ↑n

Tactic:
unfold subNatNat

Result:
m n : Nat
⊢ (match m - (m + n) with
    | 0 => ofNat (m + n - m)
    | k.succ => -[k+1]) =
    ↑n

Proof state:
m n : Nat
⊢ (match m - (m + n) with
    | 0 => ofNat (m + n - m)
    | k.succ => -[k+1]) =
    ↑n

Tactic:
rw [Nat.sub_eq_zero_of_le (Nat.le_add_right ..), Nat.add_sub_cancel_left, ofNat_eq_coe]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem right_mem_Ioc : b ∈ Ioc a b ↔ a < b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ b ∈ Ioc a b ↔ a < b

Tactic:
simp [le_refl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem eraseKey_cons_of_beq [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'}
    (h : k' == k) : eraseKey k (⟨k', v'⟩ :: l) = l :=
  by simp [eraseKey_cons, h]

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k k' : α
v' : β k'
h : (k' == k) = true
⊢ eraseKey k (⟨k', v'⟩ :: l) = l

Tactic:
simp [eraseKey_cons, h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_bot [IsProbabilityMeasure μ] (f : α → E) : μ[f|⊥] = fun _ => ∫ x, f x ∂μ

Proof state:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
f : α → E
⊢ μ[f|⊥] = fun x => ∫ (x : α), f x ∂μ

Tactic:
refine (condExp_bot' f).trans ?_

Result:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
f : α → E
⊢ (fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ) = fun x => ∫ (x : α), f x ∂μ

Proof state:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
f : α → E
⊢ (fun x => (μ Set.univ).toReal⁻¹ • ∫ (x : α), f x ∂μ) = fun x => ∫ (x : α), f x ∂μ

Tactic:
rw [measure_univ, ENNReal.one_toReal, inv_one, one_smul]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem deriv.neg : deriv (fun y => -f y) x = -deriv f x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
⊢ deriv (fun y => -f y) x = -deriv f x

Tactic:
simp only [deriv, fderiv_neg, ContinuousLinearMap.neg_apply]

Result:
no goals
-- Mathlib/Computability/TuringMachine.lean
theorem supports_run (S : Finset Λ) {k : K} (s : StAct K Γ σ k) (q : TM2.Stmt Γ Λ σ) :
    TM2.SupportsStmt S (stRun s q) ↔ TM2.SupportsStmt S q

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ TM2.SupportsStmt S (stRun s q) ↔ TM2.SupportsStmt S q

Tactic:
cases s <;> rfl

Result:
no goals
-- Mathlib/Algebra/Order/UpperLower.lean
theorem IsUpperSet.mul_right (hs : IsUpperSet s) : IsUpperSet (s * t)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (s * t)

Tactic:
rw [mul_comm]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (t * s)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
hs : IsUpperSet s
⊢ IsUpperSet (t * s)

Tactic:
exact hs.mul_left

Result:
no goals
-- Mathlib/CategoryTheory/NatIso.lean
theorem naturality_1' (α : F ⟶ G) (f : X ⟶ Y) {_ : IsIso (α.app X)} :
    inv (α.app X) ≫ F.map f ≫ α.app Y = G.map f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
α : F ⟶ G
f : X ⟶ Y
x✝ : IsIso (α.app X)
⊢ inv (α.app X) ≫ F.map f ≫ α.app Y = G.map f

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma Nonempty.zpow (hs : s.Nonempty) : ∀ {n : ℤ}, (s ^ n).Nonempty
  | (n : ℕ) => hs.pow
  | .negSucc n => by simpa using hs.pow

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
hs : s.Nonempty
n : ℕ
⊢ (s ^ Int.negSucc n).Nonempty

Tactic:
simpa using hs.pow

Result:
no goals
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem hasSum_coe {f : α → ℝ≥0} {r : ℝ≥0} : HasSum (fun a => (f a : ℝ)) (r : ℝ) ↔ HasSum f r

Proof state:
α : Type u_1
f : α → ℝ≥0
r : ℝ≥0
⊢ HasSum (fun a => ↑(f a)) ↑r ↔ HasSum f r

Tactic:
simp only [HasSum, ← coe_sum, tendsto_coe]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem smul_induction_on {C : A → Prop} {a : A} (ha : a ∈ M • N)
    (hm : ∀ m ∈ M, ∀ n ∈ N, C (m • n)) (hadd : ∀ x y, C x → C y → C (x + y)) : C a :=
  (@smul_le _ _ _ _ _ _ _ ⟨⟨setOf C, hadd _ _⟩, by
    simpa only [smul_zero] using hm _ (zero_mem _) _ (zero_mem _)⟩).2 hm ha

Proof state:
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
M : AddSubmonoid R
N : AddSubmonoid A
C : A → Prop
a : A
ha : a ∈ M • N
hm : ∀ m ∈ M, ∀ n ∈ N, C (m • n)
hadd : ∀ (x y : A), C x → C y → C (x + y)
⊢ 0 ∈ { carrier := setOf C, add_mem' := ⋯ }.carrier

Tactic:
simpa only [smul_zero] using hm _ (zero_mem _) _ (zero_mem _)

Result:
no goals
-- Mathlib/Analysis/Convex/Topology.lean
theorem closedConvexHull_closure_eq_closedConvexHull {s : Set E} :
    closedConvexHull 𝕜 (closure s) = closedConvexHull 𝕜 s :=
  subset_antisymm (by
    simpa using ((closedConvexHull 𝕜).monotone (closure_subset_closedConvexHull (𝕜 := 𝕜) (E := E))))
    ((closedConvexHull 𝕜).monotone subset_closure)

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
s : Set E
⊢ (closedConvexHull 𝕜) (closure s) ⊆ (closedConvexHull 𝕜) s

Tactic:
simpa using ((closedConvexHull 𝕜).monotone (closure_subset_closedConvexHull (𝕜 := 𝕜) (E := E)))

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_natCast_le (n : ℕ) : degree (n : R[X]) ≤ 0 := degree_le_of_natDegree_le (by simp)

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (↑n).natDegree ≤ Zero.zero

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_un : eval assign (.un op operand) = op.eval (operand.eval assign)

Proof state:
assign : Assignment
op : BVUnOp
a✝ : Nat
operand : BVExpr a✝
⊢ eval assign (un op operand) = op.eval (eval assign operand)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_zero (h : i < w) : (0#w)[i] = false

Proof state:
i w : Nat
h : i < w
⊢ (0#w)[i] = false

Tactic:
simp [getElem_eq_testBit_toNat]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Construction.lean
@[reassoc]
lemma FunctorObjIndex.comm (x : FunctorObjIndex f πX) :
    f x.i ≫ Sigma.ι (functorObjTgtFamily f πX) x ≫ ρFunctorObj f πX = x.t ≫ ιFunctorObj f πX

Proof state:
C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S X : C
πX : X ⟶ S
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasPushout (functorObjTop f πX) (functorObjLeft f πX)
x : FunctorObjIndex f πX
⊢ f x.i ≫ Sigma.ι (functorObjTgtFamily f πX) x ≫ ρFunctorObj f πX = x.t ≫ ιFunctorObj f πX

Tactic:
simpa using (Sigma.ι (functorObjSrcFamily f πX) x ≫= functorObj_comm f πX).symm

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem add_one_pow_unbounded_of_pos (x : α) (hy : 0 < y) : ∃ n : ℕ, x < (y + 1) ^ n :=
  have : 0 ≤ 1 + y := add_nonneg zero_le_one hy.le
  (Archimedean.arch x hy).imp fun n h ↦
    calc
      x ≤ n • y := h
      _ = n * y := nsmul_eq_mul _ _
      _ < 1 + n * y := lt_one_add _
      _ ≤ (1 + y) ^ n :=
        one_add_mul_le_pow' (mul_nonneg hy.le hy.le) (mul_nonneg this this)
          (add_nonneg zero_le_two hy.le) _
      _ = (y + 1) ^ n

Proof state:
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
inst✝ : Archimedean α
y x : α
hy : 0 < y
this : 0 ≤ 1 + y
n : ℕ
h : x ≤ n • y
⊢ (1 + y) ^ n = (y + 1) ^ n

Tactic:
rw [add_comm]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem left_lt_add_div_two : a < (a + b) / 2 ↔ a < b

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
⊢ a < (a + b) / 2 ↔ a < b

Tactic:
simp [lt_div_iff₀, mul_two]

Result:
no goals
-- Mathlib/CategoryTheory/Conj.lean
theorem symm_self_conj (f : End X) : α.symm.conj (α.conj f) = f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : End X
⊢ α.symm.conj (α.conj f) = f

Tactic:
rw [← trans_conj, α.self_symm_id, refl_conj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem add_mul_div_right (x y : Nat) {z : Nat} (H : 0 < z) : (x + y * z) / z = x / z + y

Proof state:
x y z : Nat
H : 0 < z
⊢ (x + y * z) / z = x / z + y

Tactic:
rw [Nat.mul_comm, add_mul_div_left _ _ H]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
lemma measure_compl₀ (h : NullMeasurableSet s μ) (hs : μ s ≠ ∞) :
    μ sᶜ = μ Set.univ - μ s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
hs : μ s ≠ ⊤
⊢ μ sᶜ = μ univ - μ s

Tactic:
rw [← measure_add_measure_compl₀ h, ENNReal.add_sub_cancel_left hs]

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

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

Tactic:
simpa only [mul_comm] using preimage_mul_const_Ico_of_neg a b h

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_self_eq_norm_mul_norm (x : F) : re ⟪x, x⟫ = ‖x‖ * ‖x‖

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ re ⟪x, x⟫_𝕜 = ‖x‖ * ‖x‖

Tactic:
rw [norm_eq_sqrt_inner, ← sqrt_mul inner_self_nonneg (re ⟪x, x⟫), sqrt_mul_self inner_self_nonneg]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycleOn.zpow_apply_eq {s : Finset α} (hf : f.IsCycleOn s) (ha : a ∈ s) :
    ∀ {n : ℤ}, (f ^ n) a = a ↔ (#s : ℤ) ∣ n
  | Int.ofNat _ => (hf.pow_apply_eq ha).trans Int.natCast_dvd_natCast.symm
  | Int.negSucc n => by
    rw [zpow_negSucc, ← inv_pow]
    exact (hf.inv.pow_apply_eq ha).trans (dvd_neg.trans Int.natCast_dvd_natCast).symm

Proof state:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
⊢ (f⁻¹ ^ (n + 1)) a = a ↔ ↑(#s) ∣ Int.negSucc n

Tactic:
exact (hf.inv.pow_apply_eq ha).trans (dvd_neg.trans Int.natCast_dvd_natCast).symm

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
⊢ (f ^ Int.negSucc n) a = a ↔ ↑(#s) ∣ Int.negSucc n

Tactic:
rw [zpow_negSucc, ← inv_pow]

Result:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
⊢ (f⁻¹ ^ (n + 1)) a = a ↔ ↑(#s) ∣ Int.negSucc n
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem affineIndependent_iff_not_collinear_set {p₁ p₂ p₃ : P} :
    AffineIndependent k ![p₁, p₂, p₃] ↔ ¬Collinear k ({p₁, p₂, p₃} : Set P)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
⊢ AffineIndependent k ![p₁, p₂, p₃] ↔ ¬Collinear k {p₁, p₂, p₃}

Tactic:
rw [affineIndependent_iff_not_collinear]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
⊢ ¬Collinear k (Set.range ![p₁, p₂, p₃]) ↔ ¬Collinear k {p₁, p₂, p₃}

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p₁ p₂ p₃ : P
⊢ ¬Collinear k (Set.range ![p₁, p₂, p₃]) ↔ ¬Collinear k {p₁, p₂, p₃}

Tactic:
simp_rw [Matrix.range_cons, Matrix.range_empty, Set.singleton_union, insert_emptyc_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_exponent_zero {f : α → ε} : eLpNorm' f 0 μ = 1

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
⊢ eLpNorm' f 0 μ = 1

Tactic:
rw [eLpNorm', div_zero, ENNReal.rpow_zero]

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
@[simp] lemma iIndepSets_zero_right : iIndepSets π κ 0

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
π : ι → Set (Set Ω)
⊢ iIndepSets π κ 0

Tactic:
simp [iIndepSets]

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem joinedIn_iff_joined (x_in : x ∈ F) (y_in : y ∈ F) :
    JoinedIn F x y ↔ Joined (⟨x, x_in⟩ : F) (⟨y, y_in⟩ : F) :=
  ⟨fun h => h.joined_subtype, fun h => ⟨h.somePath.map continuous_subtype_val, by simp⟩⟩

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
x_in : x ∈ F
y_in : y ∈ F
h : Joined ⟨x, x_in⟩ ⟨y, y_in⟩
⊢ ∀ (t : ↑I), (h.somePath.map ⋯) t ∈ F

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[simp 1100] lemma enorm_natCast (n : ℕ) : ‖(n : ℝ)‖ₑ = n

Proof state:
n : ℕ
⊢ ‖↑n‖ₑ = ↑n

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem mul_int_iff (hm : m ≠ 0) : LiouvilleWith p (x * m) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
m : ℤ
hm : m ≠ 0
⊢ LiouvilleWith p (x * ↑m) ↔ LiouvilleWith p x

Tactic:
rw [← Rat.cast_intCast, mul_rat_iff (Int.cast_ne_zero.2 hm)]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
theorem ι_desc {Z : C} (Δ : SimplexCategoryᵒᵖ) (F : ∀ A : IndexSet Δ, s.N A.1.unop.len ⟶ Z)
    (A : IndexSet Δ) : (s.cofan Δ).inj A ≫ s.desc Δ F = F A

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
Z : C
Δ : SimplexCategoryᵒᵖ
F : (A : IndexSet Δ) → s.N (unop A.fst).len ⟶ Z
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ s.desc Δ F = F A

Tactic:
apply Cofan.IsColimit.fac

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_ofBoolListLE :
    (ofBoolListLE bs).getMsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)

Proof state:
bs : List Bool
i : Nat
⊢ (ofBoolListLE bs).getMsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)

Tactic:
simp [getMsbD_eq_getLsbD]

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

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

Tactic:
rw [Iic_eq_cons_Iio, prod_cons]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
protected lemma map_inv (g : GL n R) : map f g⁻¹ = (map f g)⁻¹

Proof state:
case a.a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
i✝ j✝ : n
⊢ ↑((map f) g⁻¹) i✝ j✝ = ↑((map f) g)⁻¹ i✝ j✝

Tactic:
simp only [_root_.map_inv, coe_units_inv]

Result:
no goals

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ (map f) g⁻¹ = ((map f) g)⁻¹

Tactic:
ext

Result:
case a.a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
i✝ j✝ : n
⊢ ↑((map f) g⁻¹) i✝ j✝ = ↑((map f) g)⁻¹ i✝ j✝
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem expSeries_radius_pos : 0 < (expSeries 𝕂 𝔸).radius

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
⊢ 0 < (expSeries 𝕂 𝔸).radius

Tactic:
rw [expSeries_radius_eq_top]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
⊢ 0 < ⊤

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
⊢ 0 < ⊤

Tactic:
exact WithTop.top_pos

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem deleteEdges_sdiff_eq_of_le {H : SimpleGraph V} (h : H ≤ G) :
    G.deleteEdges (G.edgeSet \ H.edgeSet) = H

Proof state:
V : Type u
G H : SimpleGraph V
h : H ≤ G
⊢ G.deleteEdges (G.edgeSet \ H.edgeSet) = H

Tactic:
rw [← edgeSet_sdiff, deleteEdges_edgeSet, sdiff_sdiff_eq_self h]

Result:
no goals
-- Mathlib/Data/List/Duplicate.lean
theorem exists_duplicate_iff_not_nodup : (∃ x : α, x ∈+ l) ↔ ¬Nodup l

Proof state:
α : Type u_1
l : List α
⊢ (∃ x, x ∈+ l) ↔ ¬l.Nodup

Tactic:
simp [nodup_iff_forall_not_duplicate]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma one_le_pow (n m : ℕ) (h : 0 < m) : 1 ≤ m ^ n

Proof state:
n m : ℕ
h : 0 < m
⊢ 1 ≤ m ^ n

Tactic:
simpa using Nat.pow_le_pow_of_le_left h n

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem Specializes.not_disjoint (h : x ⤳ y) : ¬Disjoint (𝓝 x) (𝓝 y) := fun hd ↦
  absurd (hd.mono_right h) <| by simp [NeBot.ne']

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ⤳ y
hd : _root_.Disjoint (𝓝 x) (𝓝 y)
⊢ ¬_root_.Disjoint (𝓝 x) (𝓝 x)

Tactic:
simp [NeBot.ne']

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integrableOn_Ioi_comp_mul_right_iff (f : ℝ → E) (c : ℝ) {a : ℝ} (ha : 0 < a) :
    IntegrableOn (fun x => f (x * a)) (Ioi c) ↔ IntegrableOn f (Ioi <| c * a)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ IntegrableOn (fun x => f (x * a)) (Ioi c) volume ↔ IntegrableOn f (Ioi (c * a)) volume

Tactic:
simpa only [mul_comm, mul_zero] using integrableOn_Ioi_comp_mul_left_iff f c ha

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_C_mul_X' (c : R) : Polynomial.support (C c * X) ⊆ singleton 1

Proof state:
R : Type u
inst✝ : Semiring R
c : R
⊢ (C c * X).support ⊆ {1}

Tactic:
simpa only [C_mul_X_eq_monomial] using support_monomial' 1 c

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem biproduct.matrix_map {f : J → C} {g : K → C} {h : K → C} (m : ∀ j k, f j ⟶ g k)
    (n : ∀ k, g k ⟶ h k) :
    biproduct.matrix m ≫ biproduct.map n = biproduct.matrix fun j k => m j k ≫ n k

Proof state:
case w.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J K : Type
inst✝² : Finite J
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite K
f : J → C
g h : K → C
m : (j : J) → (k : K) → f j ⟶ g k
n : (k : K) → g k ⟶ h k
j✝¹ : K
j✝ : J
⊢ ι f j✝ ≫ (matrix m ≫ map n) ≫ π h j✝¹ = ι f j✝ ≫ (matrix fun j k => m j k ≫ n k) ≫ π h j✝¹

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J K : Type
inst✝² : Finite J
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite K
f : J → C
g h : K → C
m : (j : J) → (k : K) → f j ⟶ g k
n : (k : K) → g k ⟶ h k
⊢ matrix m ≫ map n = matrix fun j k => m j k ≫ n k

Tactic:
ext

Result:
case w.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J K : Type
inst✝² : Finite J
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite K
f : J → C
g h : K → C
m : (j : J) → (k : K) → f j ⟶ g k
n : (k : K) → g k ⟶ h k
j✝¹ : K
j✝ : J
⊢ ι f j✝ ≫ (matrix m ≫ map n) ≫ π h j✝¹ = ι f j✝ ≫ (matrix fun j k => m j k ≫ n k) ≫ π h j✝¹
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem top_prod (s : Subring S) : (⊤ : Subring R).prod s = s.comap (RingHom.snd R S) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_snd]

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
s : Subring S
x : R × S
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (RingHom.snd R S) s

Tactic:
simp [mem_prod, MonoidHom.coe_snd]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem splitMany_insert (I : Box ι) (s : Finset (ι × ℝ)) (p : ι × ℝ) :
    splitMany I (insert p s) = splitMany I s ⊓ split I p.1 p.2

Proof state:
ι : Type u_1
I : Box ι
s : Finset (ι × ℝ)
p : ι × ℝ
⊢ splitMany I (insert p s) = splitMany I s ⊓ split I p.1 p.2

Tactic:
rw [splitMany, Finset.inf_insert, inf_comm, splitMany]

Result:
no goals
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem lie_le_left : ⁅I, J⁆ ≤ I

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅I, J⁆ ≤ I

Tactic:
rw [lie_comm]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅J, I⁆ ≤ I

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I J : LieIdeal R L
⊢ ⁅J, I⁆ ≤ I

Tactic:
exact lie_le_right I J

Result:
no goals