harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_neg_iff_of_base_lt_one (h : 0 < x) : logb b x < 0 ↔ 1 < x

Proof state:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
⊢ logb b x < 0 ↔ 1 < x

Tactic:
rw [← @logb_one b, logb_lt_logb_iff_of_base_lt_one b_pos b_lt_one h zero_lt_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem negOfNat_eq_subNatNat_zero (n) : negOfNat n = subNatNat 0 n

Proof state:
n : Nat
⊢ negOfNat n = subNatNat 0 n

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Tactic/Module.lean
theorem sub_eq_eval₁ [SMul R M] [AddGroup M] (a₁ : R × M) {a₂ : R × M} {l₁ l₂ l : NF R M}
    (h : l₁.eval - (a₂ ::ᵣ l₂).eval = l.eval) :
    (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

Proof state:
R : Type u_2
M : Type u_3
inst✝¹ : SMul R M
inst✝ : AddGroup M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : l₁.eval - (a₂ ::ᵣ l₂).eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h, sub_eq_add_neg, add_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem le_add_caratheodory (m₁ m₂ : OuterMeasure α) :
    m₁.caratheodory ⊓ m₂.caratheodory ≤ (m₁ + m₂ : OuterMeasure α).caratheodory :=
  fun s ⟨hs₁, hs₂⟩ t => by simp [hs₁ t, hs₂ t, add_left_comm, add_assoc]

Proof state:
α : Type u_1
m₁ m₂ : OuterMeasure α
s : Set α
x✝ : MeasurableSet s
t : Set α
hs₁ : s ∈ (fun m => {t | MeasurableSet t}) m₁.caratheodory
hs₂ : s ∈ (fun m => {t | MeasurableSet t}) m₂.caratheodory
⊢ (m₁ + m₂) t = (m₁ + m₂) (t ∩ s) + (m₁ + m₂) (t \ s)

Tactic:
simp [hs₁ t, hs₂ t, add_left_comm, add_assoc]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem rank_pair (x y : ZFSet) : rank {x, y} = max (succ (rank x)) (succ (rank y))

Proof state:
x y : ZFSet.{u_1}
⊢ {x, y}.rank = succ x.rank ⊔ succ y.rank

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Lemmas.lean
theorem iff_left_comm {a b c : Prop} : (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))

Proof state:
a b c : Prop
⊢ (a ↔ (b ↔ c)) ↔ (b ↔ (a ↔ c))

Tactic:
tauto

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem add_zero {X Y : C} (a : X ⟶ Y) : a + 0 = a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a + 0 = a

Tactic:
rw [add_def, neg_def, sub_self, sub_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Simple.lean
theorem zero_not_simple [Simple (0 : C)] : False :=
  (Simple.mono_isIso_iff_nonzero (0 : (0 : C) ⟶ (0 : C))).mp ⟨⟨0, by simp⟩⟩ rfl

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
inst✝ : Simple 0
⊢ 0 ≫ 0 = 𝟙 0 ∧ 0 ≫ 0 = 𝟙 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem forIn'_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
    (l : Array α) (f : (a : α) → a ∈ l → β → β) (init : β) :
    forIn' l init (fun a m b => pure (.yield (f a m b))) =
      pure (f := m) (l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Array α
f : (a : α) → a ∈ l → β → β
init : β
⊢ (forIn' l init fun a m_1 b => pure (ForInStep.yield (f a m_1 b))) =
    pure
      (foldl
        (fun b x =>
          match x with
          | ⟨a, h⟩ => f a h b)
        init l.attach)

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
init : β
toList✝ : List α
f : (a : α) → a ∈ { toList := toList✝ } → β → β
⊢ (forIn' { toList := toList✝ } init fun a m_1 b => pure (ForInStep.yield (f a m_1 b))) =
    pure
      (foldl
        (fun b x =>
          match x with
          | ⟨a, h⟩ => f a h b)
        init { toList := toList✝ }.attach)

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
init : β
toList✝ : List α
f : (a : α) → a ∈ { toList := toList✝ } → β → β
⊢ (forIn' { toList := toList✝ } init fun a m_1 b => pure (ForInStep.yield (f a m_1 b))) =
    pure
      (foldl
        (fun b x =>
          match x with
          | ⟨a, h⟩ => f a h b)
        init { toList := toList✝ }.attach)

Tactic:
simp [List.forIn'_pure_yield_eq_foldl, List.foldl_map]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem WalkingParallelPairHom.comp_id
    {X Y : WalkingParallelPair} (f : WalkingParallelPairHom X Y) : comp f (id Y) = f

Proof state:
X Y : WalkingParallelPair
f : WalkingParallelPairHom X Y
⊢ f.comp (id Y) = f

Tactic:
cases f <;> rfl

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_prod_eq (a b : α × β) : Icc a b = Icc a.1 b.1 ×ˢ Icc a.2 b.2

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α × β
⊢ Icc a b = Icc a.1 b.1 ×ˢ Icc a.2 b.2

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_eq_of_eq_div' (h : b = c / a) : a * b = c

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c : G
h : b = c / a
⊢ a * b = c

Tactic:
rw [h, div_eq_mul_inv, mul_comm c, mul_inv_cancel_left]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_union [DecidableEq β] : (s₁ ∪ s₂).sup f = s₁.sup f ⊔ s₂.sup f :=
  eq_of_forall_ge_iff fun c => by simp [or_imp, forall_and]

Proof state:
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
c : α
⊢ (s₁ ∪ s₂).sup f ≤ c ↔ s₁.sup f ⊔ s₂.sup f ≤ c

Tactic:
simp [or_imp, forall_and]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getThenInsertIfNew?_snd {k : α} {v : β} :
    (getThenInsertIfNew? m k v).2 = m.insertIfNew k v

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw₀ α fun x => β
k : α
v : β
⊢ (getThenInsertIfNew? m k v).snd = m.insertIfNew k v

Tactic:
rw [getThenInsertIfNew?_eq_insertIfNewₘ, insertIfNew_eq_insertIfNewₘ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_insertEntry_self [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k : α}
    {v : β k} : getKey? k (insertEntry k v l) = some k

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ getKey? k (insertEntry k v l) = some k

Tactic:
simp [getKey?_insertEntry]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
lemma negPart_smul_of_nonpos {r : ℝ} (hr : r ≤ 0) {a : A} : (r • a)⁻ = -r • a⁺

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
⊢ (r • a)⁻ = -r • a⁺

Tactic:
conv_lhs => rw [← neg_neg r, neg_smul, negPart_neg, posPart_smul_of_nonneg (by simpa)]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : T2Space A
inst✝ : StarModule ℝ A
r : ℝ
hr : r ≤ 0
a : A
⊢ 0 ≤ -r

Tactic:
simpa

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem nat_lt_one_iff (m : ℕ) : padicNorm p m < 1 ↔ p ∣ m

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
⊢ padicNorm p ↑m < 1 ↔ p ∣ m

Tactic:
rw [← Int.natCast_dvd_natCast, ← int_lt_one_iff, Int.cast_natCast]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem inter_singleton_of_not_mem {a : α} {s : Finset α} (h : a ∉ s) : s ∩ {a} = ∅

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ s ∩ {a} = ∅

Tactic:
rw [inter_comm, singleton_inter_of_not_mem h]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/Basic.lean
lemma zeroLocus_singleton {U : Opens X} (f : X.presheaf.obj (op U)) :
    X.zeroLocus {f} = (X.basicOpen f).carrierᶜ

Proof state:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
⊢ X.zeroLocus {f} = (X.basicOpen f).carrierᶜ

Tactic:
simp [zeroLocus]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_subset_Ico_iff {a₁ b₁ a₂ b₂ : α} (h : a₁ < b₁) :
    Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

Tactic:
rw [← coe_subset, coe_Ico, coe_Ico, Set.Ico_subset_Ico_iff h]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Basic.lean
lemma mk_eq_mk (x y : K) (hx hy) : (⟨x, hx⟩ : 𝓞 K) = ⟨y, hy⟩ ↔ x = y

Proof state:
K : Type u_1
inst✝ : Field K
x y : K
hx : x ∈ integralClosure ℤ K
hy : y ∈ integralClosure ℤ K
⊢ ⟨x, hx⟩ = ⟨y, hy⟩ ↔ x = y

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/DecidableEq.lean
theorem isEqv_toArray [BEq α] (a b : List α) : (a.toArray.isEqv b.toArray r) = (a.isEqv b r)

Proof state:
α : Type u_1
r : α → α → Bool
inst✝ : BEq α
a b : List α
⊢ a.toArray.isEqv b.toArray r = a.isEqv b r

Tactic:
simp [isEqv_eq_decide, Array.isEqv_eq_decide]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem associator_naturality_left {X X' : C} (f : X ⟶ X') (Y Z : C) :
    f ▷ Y ▷ Z ≫ (α_ X' Y Z).hom = (α_ X Y Z).hom ≫ f ▷ (Y ⊗ Z)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ f ▷ Y ▷ Z ≫ (α_ X' Y Z).hom = (α_ X Y Z).hom ≫ f ▷ (Y ⊗ Z)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem inter_erase (a : α) (s t : Finset α) : s ∩ t.erase a = (s ∩ t).erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ s ∩ t.erase a = (s ∩ t).erase a

Tactic:
simp only [erase_eq, inter_sdiff_assoc]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma nnnorm_spectrum_le (a : A) ⦃x : 𝕜⦄ (hx : x ∈ σ 𝕜 a) (ha : p a

Proof state:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
x : 𝕜
hx : x ∈ σ 𝕜 a
ha : autoParam (p a) _auto✝
⊢ ‖x‖₊ ≤ ‖a‖₊

Tactic:
simpa only [cfc_id 𝕜 a] using nnnorm_apply_le_nnnorm_cfc (id : 𝕜 → 𝕜) a hx

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
@[reassoc (attr := simp)]
lemma unit_app_shift_commShiftIso_inv_app [adj.CommShift A] (a : A) (X : C) :
    (adj.unit.app X)⟦a⟧' ≫ ((F ⋙ G).commShiftIso a).inv.app X = adj.unit.app (X⟦a⟧)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
inst✝ : adj.CommShift A
a : A
X : C
⊢ (shiftFunctor C a).map (adj.unit.app X) ≫ ((F ⋙ G).commShiftIso a).inv.app X = adj.unit.app ((shiftFunctor C a).obj X)

Tactic:
simp [← cancel_mono (((F ⋙ G).commShiftIso _).hom.app _)]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.map (f : α → β) (hl : l.HasBasis p s) : (l.map f).HasBasis p fun i => f '' s i :=
  ⟨fun t => by simp only [mem_map, image_subset_iff, hl.mem_iff, preimage]⟩

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : α → β
hl : l.HasBasis p s
t : Set β
⊢ t ∈ Filter.map f l ↔ ∃ i, p i ∧ f '' s i ⊆ t

Tactic:
simp only [mem_map, image_subset_iff, hl.mem_iff, preimage]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma cliqueFinset_eq_map [NoAccidental t] : (graph t).cliqueFinset 3 = t.map toTriangle

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : NoAccidental t
⊢ (graph t).cliqueFinset 3 = map toTriangle t

Tactic:
simp [cliqueFinset_eq_image, map_eq_image]

Result:
no goals
-- Mathlib/Order/Category/BoolAlg.lean
lemma id_apply (X : BoolAlg) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : BoolAlg
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem add_toZNum (m n : Num) : Num.toZNum (m + n) = m.toZNum + n.toZNum

Proof state:
m n : Num
⊢ (m + n).toZNum = m.toZNum + n.toZNum

Tactic:
cases m <;> cases n <;> rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem double_dual_bound (x : E) : ‖(inclusionInDoubleDual 𝕜 E) x‖ ≤ ‖x‖

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ ‖(inclusionInDoubleDual 𝕜 E) x‖ ≤ ‖x‖

Tactic:
simpa using ContinuousLinearMap.le_of_opNorm_le _ (inclusionInDoubleDual_norm_le 𝕜 E) x

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem monic_expand_iff {p : ℕ} {f : R[X]} (hp : 0 < p) : (expand R p f).Monic ↔ f.Monic

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : 0 < p
⊢ ((expand R p) f).Monic ↔ f.Monic

Tactic:
simp only [Monic, leadingCoeff_expand hp]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_iUnion_eq' {f : ι → α} {g : α → Set β} :
    ⋃ (x) (y) (_ : f y = x), g x = ⋃ y, g (f y)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → Set β
⊢ ⋃ x, ⋃ y, ⋃ (_ : f y = x), g x = ⋃ y, g (f y)

Tactic:
simpa using biUnion_range

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/CompareExp.lean
theorem of_isBigO_im_re_rpow (hre : Tendsto re l atTop) (r : ℝ) (hr : im =O[l] fun z => z.re ^ r) :
    IsExpCmpFilter l :=
  ⟨hre, fun n =>
    IsLittleO.isBigO <|
      calc
        (fun z : ℂ => z.im ^ n) =O[l] fun z => (z.re ^ r) ^ n := hr.pow n
        _ =ᶠ[l] fun z => z.re ^ (r * n) :=
          ((hre.eventually_ge_atTop 0).mono fun z hz => by
            simp only [Real.rpow_mul hz r n, Real.rpow_natCast])
        _ =o[l] fun z => Real.exp z.re := (isLittleO_rpow_exp_atTop _).comp_tendsto hre ⟩

Proof state:
l : Filter ℂ
hre : Tendsto re l atTop
r : ℝ
hr : im =O[l] fun z => z.re ^ r
n : ℕ
z : ℂ
hz : 0 ≤ z.re
⊢ (fun z => (z.re ^ r) ^ n) z = (fun z => z.re ^ (r * ↑n)) z

Tactic:
simp only [Real.rpow_mul hz r n, Real.rpow_natCast]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem toNat_le_toNat {b₀ b₁ : Bool} (h : b₀ ≤ b₁) : toNat b₀ ≤ toNat b₁

Proof state:
b₀ b₁ : Bool
h : b₀ ≤ b₁
⊢ b₀.toNat ≤ b₁.toNat

Tactic:
cases b₀ <;> cases b₁ <;> simp_all +decide

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobject_le_mk {A B : C} {X : C} (g : X ⟶ B) [Mono g] (f : A ⟶ B) [HasImage f]
    (h : A ⟶ X) (w : h ≫ g = f) : imageSubobject f ≤ Subobject.mk g :=
  imageSubobject_le f (h ≫ (Subobject.underlyingIso g).inv) (by simp [w])

Proof state:
C : Type u
inst✝² : Category.{v, u} C
A B X : C
g : X ⟶ B
inst✝¹ : Mono g
f : A ⟶ B
inst✝ : HasImage f
h : A ⟶ X
w : h ≫ g = f
⊢ (h ≫ (underlyingIso g).inv) ≫ (Subobject.mk g).arrow = f

Tactic:
simp [w]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
theorem Cotrident.app_one (s : Cotrident f) (j : J) : f j ≫ s.ι.app one = s.ι.app zero

Proof state:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Cotrident f
j : J
⊢ f j ≫ s.ι.app one = s.ι.app zero

Tactic:
rw [← s.w (line j), parallelFamily_map_left]

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem coe_centralizer_centralizer (s : Set A) :
    (centralizer R (centralizer R s : Set A)) = (s ∪ star s).centralizer.centralizer

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R ↑(centralizer R s)) = (s ∪ star s).centralizer.centralizer

Tactic:
rw [coe_centralizer, StarMemClass.star_coe_eq, Set.union_self, coe_centralizer]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem singleton_subset_singleton : ({a} : Finset α) ⊆ {b} ↔ a = b

Proof state:
α : Type u_1
a b : α
⊢ {a} ⊆ {b} ↔ a = b

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem join_eq_some : x.join = some a ↔ x = some (some a)

Proof state:
α✝ : Type u_1
a : α✝
x : Option (Option α✝)
⊢ x.join = some a ↔ x = some (some a)

Tactic:
simp [bind_eq_some]

Result:
no goals
-- Mathlib/RingTheory/QuotSMulTop.lean
lemma map_surjective {f : M →ₗ[R] M'} (hf : Surjective f) : Surjective (map r f) :=
  have H₁ := (mkQ_surjective (r • ⊤ : Submodule R M')).comp hf
  @Surjective.of_comp _ _ _ _ (mkQ (r • ⊤ : Submodule R M)) <| by
    rwa [← LinearMap.coe_comp, map_comp_mkQ, LinearMap.coe_comp]

Proof state:
R : Type u_2
inst✝⁴ : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Surjective ⇑f
H₁ : Surjective (⇑(r • ⊤).mkQ ∘ ⇑f)
⊢ Surjective (⇑((map r) f) ∘ ⇑(r • ⊤).mkQ)

Tactic:
rwa [← LinearMap.coe_comp, map_comp_mkQ, LinearMap.coe_comp]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem subset_support_append_left {V : Type u} {G : SimpleGraph V} {u v w : V}
    (p : G.Walk u v) (q : G.Walk v w) : p.support ⊆ (p.append q).support

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ p.support ⊆ (p.append q).support

Tactic:
simp only [Walk.support_append, List.subset_append_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h  = last n' :=
  Fin.ext (by rw [coe_cast, val_last, val_last, Nat.succ.inj h])

Proof state:
n n' : Nat
h : n + 1 = n' + 1
⊢ ↑(Fin.cast h (last n)) = ↑(last n')

Tactic:
rw [coe_cast, val_last, val_last, Nat.succ.inj h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem decide_false_eq {b : Bool} [Decidable (false = b)] : decide (false = b) = !b

Proof state:
b : Bool
inst✝ : Decidable (false = b)
⊢ decide (false = b) = !b

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
lemma le_iff_sdiff_subset_lowerClosure {s t : Colex α} :
    s ≤ t ↔ (ofColex s : Set α) \ ofColex t ⊆ lowerClosure (ofColex t \ ofColex s : Set α)

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t : Colex α
⊢ s ≤ t ↔ ↑s.ofColex \ ↑t.ofColex ⊆ ↑(lowerClosure (↑t.ofColex \ ↑s.ofColex))

Tactic:
simp [le_def, Set.subset_def, and_assoc]

Result:
no goals
-- Mathlib/Analysis/Calculus/DSlope.lean
theorem sub_smul_dslope (f : 𝕜 → E) (a b : 𝕜) : (b - a) • dslope f a b = f b - f a

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
⊢ (b - a) • dslope f a b = f b - f a

Tactic:
rcases eq_or_ne b a with (rfl | hne) <;> simp [dslope_of_ne, *]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
/-- Consider a parameterized integral `x ↦ ∫ y, f x y` where `f` is continuous and uniformly
compactly supported. Then the integral depends continuously on `x`. -/
lemma continuousOn_integral_of_compact_support
    {f : X → Y → E} {s : Set X} {k : Set Y} [IsFiniteMeasureOnCompacts μ]
    (hk : IsCompact k) (hf : ContinuousOn f.uncurry (s ×ˢ univ))
    (hfs : ∀ p, ∀ x, p ∈ s → x ∉ k → f p x = 0) :
    ContinuousOn (fun x ↦ ∫ y, f x y ∂μ) s

Proof state:
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : OpensMeasurableSpace Y
μ : Measure Y
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → Y → E
s : Set X
k : Set Y
inst✝ : IsFiniteMeasureOnCompacts μ
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
⊢ ContinuousOn (fun x => ∫ (y : Y), f x y ∂μ) s

Tactic:
simpa using continuousOn_integral_bilinear_of_locally_integrable_of_compact_support (lsmul ℝ ℝ)
  hk hf hfs (integrableOn_const.2 (Or.inr hk.measure_lt_top)) (μ := μ) (g := fun _ ↦ 1)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
lemma natTrailingDegree_ne_zero : natTrailingDegree p ≠ 0 ↔ p ≠ 0 ∧ coeff p 0 = 0 :=
  natTrailingDegree_eq_zero.not.trans <| by rw [not_or, not_ne_iff]

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ¬(p = 0 ∨ p.coeff 0 ≠ 0) ↔ p ≠ 0 ∧ p.coeff 0 = 0

Tactic:
rw [not_or, not_ne_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Relabel.lean
theorem relabel_comp (decl : Decl α) (g : α → β) (h : β → γ) :
    relabel (h ∘ g) decl = relabel h (relabel g decl)

Proof state:
α β γ : Type
decl : Decl α
g : α → β
h : β → γ
⊢ relabel (h ∘ g) decl = relabel h (relabel g decl)

Tactic:
cases decl <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insertMany_list_le [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)} :
    (insertMany m l).1.1.size ≤ m.1.size + l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
⊢ (insertMany m l).val.val.size ≤ m.val.size + l.length

Tactic:
simp_to_model [Const.insertMany] using List.length_insertListConst_le

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem coe_image : ↑(s.image f) = f '' ↑s :=
  Set.ext <| by simp only [mem_coe, mem_image, Set.mem_image, implies_true]

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ ∀ (x : β), x ∈ ↑(image f s) ↔ x ∈ f '' ↑s

Tactic:
simp only [mem_coe, mem_image, Set.mem_image, implies_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
theorem Bool.decide_eq_true (a : Bool) : (decide (a = true)) = a

Proof state:
a : Bool
⊢ decide (a = true) = a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem iff_and_not_self : ∀ {a b : Bool}, (b = (a && !b)) ↔ !a ∧ !b

Proof state:
⊢ ∀ {a b : Bool}, b = (a && !b) ↔ (!a) = true ∧ (!b) = true

Tactic:
decide

Result:
no goals
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem ratio_of_subsingleton [Subsingleton α] [DilationClass F α β] (f : F) : ratio f = 1 :=
  if_pos fun x y ↦ by simp [Subsingleton.elim x y]

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : FunLike F α β
inst✝¹ : Subsingleton α
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist x y = 0 ∨ edist x y = ⊤

Tactic:
simp [Subsingleton.elim x y]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Defs.lean
theorem mul_self_lt_one_iff : a * a < 1 ↔ a < 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommMonoid α
a : α
⊢ a * a < 1 ↔ a < 1

Tactic:
simp [← not_iff_not]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem beq_comm {α} [BEq α] [LawfulBEq α] {a b : α} : (a == b) = (b == a) :=
  Bool.coe_iff_coe.mp (by simp [@eq_comm α])

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = true ↔ (b == a) = true

Tactic:
simp [@eq_comm α]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)} {k : α} {fallback : β}
    (h' : (l.map Prod.fst).contains k = false) :
    getD (insertMany m l).1 k fallback = getD m k fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
k : α
fallback : β
h' : (List.map Prod.fst l).contains k = false
⊢ getD (insertMany m l).val k fallback = getD m k fallback

Tactic:
simp_to_model [Const.insertMany] using List.getValueD_insertListConst_of_contains_eq_false

Result:
no goals