harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiffWithinAt.div {f g : E → 𝕜} {n} (hf : ContDiffWithinAt 𝕜 n f s x)
    (hg : ContDiffWithinAt 𝕜 n g s x) (hx : g x ≠ 0) :
    ContDiffWithinAt 𝕜 n (fun x => f x / g x) s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type uE
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x : E
f g : E → 𝕜
n : WithTop ℕ∞
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
hx : g x ≠ 0
⊢ ContDiffWithinAt 𝕜 n (fun x => f x / g x) s x

Tactic:
simpa only [div_eq_mul_inv] using hf.mul (hg.inv hx)

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem pow_period_smul (m : M) (a : α) : m ^ (period m a) • a = a

Proof state:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
⊢ m ^ period m a • a = a

Tactic:
rw [period_eq_minimalPeriod, ← smul_iterate_apply, iterate_minimalPeriod]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_add_cosh : sinh x + cosh x = exp x

Proof state:
x : ℝ
⊢ sinh x + cosh x = rexp x

Tactic:
rw [add_comm, cosh_add_sinh]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.equiv_trans {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) {v' : Basis ι' 𝕜 E'}
    (hv' : Orthonormal 𝕜 v') (e : ι ≃ ι') {v'' : Basis ι'' 𝕜 E''} (hv'' : Orthonormal 𝕜 v'')
    (e' : ι' ≃ ι'') : (hv.equiv hv' e).trans (hv'.equiv hv'' e') = hv.equiv hv'' (e.trans e') :=
  v.ext_linearIsometryEquiv fun i => by
    simp only [LinearIsometryEquiv.trans_apply, Orthonormal.equiv_apply, e.coe_trans,
      Function.comp_apply]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
ι'' : Type u_6
E' : Type u_7
inst✝³ : SeminormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
E'' : Type u_8
inst✝¹ : SeminormedAddCommGroup E''
inst✝ : InnerProductSpace 𝕜 E''
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
v' : Basis ι' 𝕜 E'
hv' : Orthonormal 𝕜 ⇑v'
e : ι ≃ ι'
v'' : Basis ι'' 𝕜 E''
hv'' : Orthonormal 𝕜 ⇑v''
e' : ι' ≃ ι''
i : ι
⊢ ((hv.equiv hv' e).trans (hv'.equiv hv'' e')) (v i) = (hv.equiv hv'' (e.trans e')) (v i)

Tactic:
simp only [LinearIsometryEquiv.trans_apply, Orthonormal.equiv_apply, e.coe_trans,
  Function.comp_apply]

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem pellZd_succ (n : ℕ) : pellZd a1 (n + 1) = pellZd a1 n * ⟨a, 1⟩

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ pellZd a1 (n + 1) = pellZd a1 n * { re := ↑a, im := 1 }

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
lemma add_ne_top : x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Proof state:
α : Type u
inst✝ : Add α
x y : WithTop α
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.smul {c : 𝕜} (hc : 0 ≤ c) (hf : ConvexOn 𝕜 s f) : ConvexOn 𝕜 s fun x => c • f x :=
  ⟨hf.1, fun x hx y hy a b ha hb hab =>
    calc
      c • f (a • x + b • y) ≤ c • (a • f x + b • f y) :=
        smul_le_smul_of_nonneg_left (hf.2 hx hy ha hb hab) hc
      _ = a • c • f x + b • c • f y

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedCommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
c : 𝕜
hc : 0 ≤ c
hf : ConvexOn 𝕜 s f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ c • (a • f x + b • f y) = a • c • f x + b • c • f y

Tactic:
rw [smul_add, smul_comm c, smul_comm c]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma rightHomologyMap'_add :
    rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ +
      rightHomologyMap' φ' h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
γ' : RightHomologyMapData φ' h₁ h₂
⊢ rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂

Tactic:
simp only [γ.rightHomologyMap'_eq, γ'.rightHomologyMap'_eq,
  (γ.add γ').rightHomologyMap'_eq, RightHomologyMapData.add_φH]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂

Tactic:
have γ' : RightHomologyMapData φ' h₁ h₂ := default

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
γ' : RightHomologyMapData φ' h₁ h₂
⊢ rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem add_eq_zero' : a + b = 0 ↔ a = b :=
  calc
    a + b = 0 ↔ a = -b := add_eq_zero_iff_eq_neg
    _ ↔ a = b

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a = -b ↔ a = b

Tactic:
rw [neg_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem arctan_eq_zero_iff {x : ℝ} : arctan x = 0 ↔ x = 0 :=
  .trans (by rw [arctan_zero]) arctan_injective.eq_iff

Proof state:
x : ℝ
⊢ arctan x = 0 ↔ arctan x = arctan 0

Tactic:
rw [arctan_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma natDegree_Φ_pos [Nontrivial R] {n : ℤ} (hn : n ≠ 0) : 0 < (W.Φ n).natDegree

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℤ
hn : n ≠ 0
⊢ 0 < (W.Φ n).natDegree

Tactic:
rwa [natDegree_Φ, pow_pos_iff two_ne_zero, Int.natAbs_pos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem lt_length_drop (L : List α) {i j : Nat} (h : i + j < L.length) : j < (L.drop i).length

Proof state:
α : Type u_1
L : List α
i j : Nat
h : i + j < (take i L ++ drop i L).length
A : i < L.length
⊢ j < (drop i L).length

Tactic:
simpa only [Nat.le_of_lt A, Nat.min_eq_left, Nat.add_lt_add_iff_left, length_take,
  length_append] using h

Result:
no goals

Proof state:
α : Type u_1
L : List α
i j : Nat
h : i + j < L.length
A : i < L.length
⊢ j < (drop i L).length

Tactic:
rw [(take_append_drop i L).symm] at h

Result:
α : Type u_1
L : List α
i j : Nat
h : i + j < (take i L ++ drop i L).length
A : i < L.length
⊢ j < (drop i L).length

Proof state:
α : Type u_1
L : List α
i j : Nat
h : i + j < L.length
⊢ j < (drop i L).length

Tactic:
have A : i < L.length := Nat.lt_of_le_of_lt (Nat.le.intro rfl) h

Result:
α : Type u_1
L : List α
i j : Nat
h : i + j < L.length
A : i < L.length
⊢ j < (drop i L).length
-- Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
theorem disjoint_right (C : G.ComponentCompl K) : Disjoint K C

Proof state:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
⊢ K ∩ ↑C ⊆ ∅

Tactic:
exact fun v ⟨vK, vC⟩ => vC.choose vK

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
⊢ Disjoint K ↑C

Tactic:
rw [Set.disjoint_iff]

Result:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
⊢ K ∩ ↑C ⊆ ∅
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_mul_relrank_eq_inf_relrank (h : B ≤ C) :
    relrank A B * relrank B C = (A ⊓ B).relrank C

Proof state:
E : Type v
inst✝ : Field E
A B C : Subfield E
h : B ≤ C
⊢ A.relrank B * B.relrank C = (A ⊓ B).relrank C

Tactic:
simpa only [inf_of_le_left h] using relrank_inf_mul_relrank A B C

Result:
no goals
-- Mathlib/Data/Nat/PrimeFin.lean
@[simp] lemma primeFactors_zero : primeFactors 0 = ∅

Proof state:
case h
a✝ : ℕ
⊢ a✝ ∈ primeFactors 0 ↔ a✝ ∈ ∅

Tactic:
simp

Result:
no goals

Proof state:
⊢ primeFactors 0 = ∅

Tactic:
ext

Result:
case h
a✝ : ℕ
⊢ a✝ ∈ primeFactors 0 ↔ a✝ ∈ ∅
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem Finset.ciInf_mem_image {s : Finset ι} (h : ∃ x ∈ s, f x ≤ sInf ∅) :
    ⨅ i ∈ s, f i ∈ s.image f

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ i ∈ s, f i ∈ image f s

Tactic:
rw [ciInf_eq_min'_image _ h]

Result:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ (image f s).min' ⋯ ∈ image f s

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ (image f s).min' ⋯ ∈ image f s

Tactic:
exact min'_mem (image f s) _

Result:
no goals
-- Mathlib/RingTheory/Localization/Submodule.lean
theorem coeSubmodule_span_singleton (x : R) :
    coeSubmodule S (Ideal.span {x}) = Submodule.span R {(algebraMap R S) x}

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : R
⊢ coeSubmodule S (Ideal.span {x}) = Submodule.span R {(algebraMap R S) x}

Tactic:
rw [coeSubmodule_span, Set.image_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_zero_length (x : BitVec 0) : x.getMsbD i = false

Proof state:
i : Nat
x : BitVec 0
⊢ x.getMsbD i = false

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/BinaryRec.lean
theorem bit_testBit_zero_shiftRight_one (n : Nat) : bit (n.testBit 0) (n >>> 1) = n

Proof state:
n : Nat
⊢ bit (n.testBit 0) (n >>> 1) = n

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_ofReal_mul (c : ℝ) (a : ℝ≥0∞) (h : 0 ≤ c) :
    ENNReal.toReal (ENNReal.ofReal c * a) = c * ENNReal.toReal a

Proof state:
c : ℝ
a : ℝ≥0∞
h : 0 ≤ c
⊢ (ENNReal.ofReal c * a).toReal = c * a.toReal

Tactic:
rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal h]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Basic.lean
/-- The cardinality of the fiber of a coproduct is the sum of the cardinalities of the fibers. -/
lemma card_fiber_coprod_eq_sum (X Y : C) :
    Nat.card (F.obj (X ⨿ Y)) = Nat.card (F.obj X) + Nat.card (F.obj Y)

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
e : (F.obj (X ⨿ Y)).carrier ≃ (F.obj X).carrier ⊕ (F.obj Y).carrier :=
  ((PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm ≪≫
      Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))).toEquiv
⊢ Nat.card (F.obj (X ⨿ Y)).carrier = Nat.card ((F.obj X).carrier ⊕ (F.obj Y).carrier)

Tactic:
exact Nat.card_eq_of_bijective e.toFun (Equiv.bijective e)

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
⊢ Nat.card (F.obj (X ⨿ Y)).carrier = Nat.card (F.obj X).carrier + Nat.card (F.obj Y).carrier

Tactic:
let e : F.obj (X ⨿ Y) ≃ F.obj X ⊕ F.obj Y := Iso.toEquiv
  <| (PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm.trans
  <| Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
e : (F.obj (X ⨿ Y)).carrier ≃ (F.obj X).carrier ⊕ (F.obj Y).carrier :=
  ((PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm ≪≫
      Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))).toEquiv
⊢ Nat.card (F.obj (X ⨿ Y)).carrier = Nat.card (F.obj X).carrier + Nat.card (F.obj Y).carrier

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
e : (F.obj (X ⨿ Y)).carrier ≃ (F.obj X).carrier ⊕ (F.obj Y).carrier :=
  ((PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm ≪≫
      Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))).toEquiv
⊢ Nat.card (F.obj (X ⨿ Y)).carrier = Nat.card (F.obj X).carrier + Nat.card (F.obj Y).carrier

Tactic:
rw [← Nat.card_sum]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : PreGaloisCategory C
inst✝ : FiberFunctor F
X Y : C
e : (F.obj (X ⨿ Y)).carrier ≃ (F.obj X).carrier ⊕ (F.obj Y).carrier :=
  ((PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm ≪≫
      Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))).toEquiv
⊢ Nat.card (F.obj (X ⨿ Y)).carrier = Nat.card ((F.obj X).carrier ⊕ (F.obj Y).carrier)
-- Mathlib/Data/Finset/Filter.lean
lemma filter_inj' : s.filter p = s.filter q ↔ ∀ ⦃a⦄, a ∈ s → (p a ↔ q a)

Proof state:
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ filter p s = filter q s ↔ ∀ ⦃a : α⦄, a ∈ s → (p a ↔ q a)

Tactic:
simp [Finset.ext_iff]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem constantCoeff_monomial [DecidableEq σ] (d : σ →₀ ℕ) (r : R) :
    constantCoeff (monomial d r) = if d = 0 then r else 0

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
d : σ →₀ ℕ
r : R
⊢ constantCoeff ((monomial d) r) = if d = 0 then r else 0

Tactic:
rw [constantCoeff_eq, coeff_monomial]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_add : cosh (x + y) = cosh x * cosh y + sinh x * sinh y

Proof state:
x y : ℝ
⊢ cosh (x + y) = cosh x * cosh y + sinh x * sinh y

Tactic:
rw [← ofReal_inj]

Result:
x y : ℝ
⊢ ↑(cosh (x + y)) = ↑(cosh x * cosh y + sinh x * sinh y)

Proof state:
x y : ℝ
⊢ ↑(cosh (x + y)) = ↑(cosh x * cosh y + sinh x * sinh y)

Tactic:
simp [cosh_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_mkVector_self (a : α) (n : Nat) : count a (mkVector n a) = n

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
n : Nat
⊢ count a (mkVector n a) = n

Tactic:
simp only [mkVector_eq_mk_mkArray, count_cast, count_mk]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
n : Nat
⊢ Array.count a (mkArray n a) = n

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
n : Nat
⊢ Array.count a (mkArray n a) = n

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
lemma restrict_comap (μ : Measure β) (s : Set α) :
    (μ.comap f).restrict s = (μ.restrict (f '' s)).comap f

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set α
⊢ (Measure.comap f μ).restrict s = Measure.comap f (μ.restrict (f '' s))

Tactic:
rw [comap_restrict hf, preimage_image_eq _ hf.injective]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem DistinctKeys.nil [BEq α] : DistinctKeys ([] : List ((a : α) × β a)) :=
  ⟨by simp⟩

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
⊢ List.Pairwise (fun a b => (a == b) = false) (keys [])

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_eq_zero_of_ae_zero {f : α → E} (hf : f =ᵐ[μ] 0) : eLpNorm f p μ = 0

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : f =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = eLpNorm 0 p μ

Tactic:
exact eLpNorm_congr_ae hf

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : f =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = 0

Tactic:
rw [← eLpNorm_zero (p := p) (μ := μ) (α := α) (F := E)]

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : f =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = eLpNorm 0 p μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_ofNatLt {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
  getLsbD (x#'lt) i = x.testBit i

Proof state:
n x : Nat
lt : x < 2 ^ n
i : Nat
⊢ (x#'lt).getLsbD i = x.testBit i

Tactic:
simp [getLsbD, BitVec.ofNatLt]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_pi {β : α → Type*} [Fintype α] : Nat.card (∀ a, β a) = ∏ a, Nat.card (β a)

Proof state:
α : Type u_1
β : α → Type u_3
inst✝ : Fintype α
⊢ Nat.card ((a : α) → β a) = ∏ a : α, Nat.card (β a)

Tactic:
simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, map_prod]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem dropLast_append {l₁ l₂ : List α} :
    (l₁ ++ l₂).dropLast = if l₂.isEmpty then l₁.dropLast else l₁ ++ l₂.dropLast

Proof state:
α : Type u_1
l₁ l₂ : List α
⊢ (l₁ ++ l₂).dropLast = if l₂.isEmpty = true then l₁.dropLast else l₁ ++ l₂.dropLast

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_nonneg_iff (hx : 0 < x) : 0 ≤ log x ↔ 1 ≤ x

Proof state:
x : ℝ
hx : 0 < x
⊢ 0 ≤ log x ↔ 1 ≤ x

Tactic:
rw [← not_lt, log_neg_iff hx, not_lt]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma comma_iso_iff (P : MorphismProperty C) [P.RespectsIso] {A B : Type*} [Category A] [Category B]
    {L : A ⥤ C} {R : B ⥤ C} {f g : Comma L R} (e : f ≅ g) :
    P f.hom ↔ P g.hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.RespectsIso
A : Type u_2
B : Type u_3
inst✝¹ : Category.{u_4, u_2} A
inst✝ : Category.{u_5, u_3} B
L : A ⥤ C
R : B ⥤ C
f g : Comma L R
e : f ≅ g
⊢ P f.hom ↔ P g.hom

Tactic:
simp [← Comma.inv_left_hom_right e.hom, cancel_left_of_respectsIso, cancel_right_of_respectsIso]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
@[to_additive (attr := simp)]
lemma inv_Ico (a b : α) : (Ico a b)⁻¹ = Ioc b⁻¹ a⁻¹

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ (Ico a b)⁻¹ = Ioc b⁻¹ a⁻¹

Tactic:
simp [← Ici_inter_Iio, ← Ioi_inter_Iic, inter_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem Int.ofNat_sub_ofNat_of_lt {n m : Nat} (hlt : n < m) :
    (n : Int) - (m : Int) = -(↑(m - 1 - n) + 1)

Proof state:
n m : Nat
hlt : n < m
⊢ ↑n - ↑m = -(↑(m - 1 - n) + 1)

Tactic:
omega

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

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

Tactic:
simp [range', Nat.add_succ, Nat.mul_succ]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_add_mul_right_right (m n k : ℕ) : gcd m (n + k * m) = gcd m n

Proof state:
m n k : ℕ
⊢ m.gcd (n + k * m) = m.gcd n

Tactic:
simp [gcd_rec m (n + k * m), gcd_rec m n]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Defs.lean
/-- Equality holds when `b ≠ 0`. See `inv_mul_cancel_right`. -/
lemma inv_mul_right_le (ha : 0 ≤ a) : a * b⁻¹ * b ≤ a

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
ha : 0 ≤ a
⊢ a * b⁻¹ * b ≤ a

Tactic:
obtain rfl | hb := eq_or_ne b 0 <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_neg (θ : Angle) : (-θ).sign = -θ.sign

Proof state:
θ : Angle
⊢ (-θ).sign = -θ.sign

Tactic:
simp_rw [sign, sin_neg, Left.sign_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_eq_of_eq_add {a b c : Nat} (h : a = c + b) : a - b = c

Proof state:
a b c : Nat
h : a = c + b
⊢ a - b = c

Tactic:
rw [h, Nat.add_sub_cancel]

Result:
no goals
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem dist_div_left [Group G] [PseudoMetricSpace G] [IsometricSMul G G]
    [IsometricSMul Gᵐᵒᵖ G] (a b c : G) : dist (a / b) (a / c) = dist b c

Proof state:
G : Type v
inst✝³ : Group G
inst✝² : PseudoMetricSpace G
inst✝¹ : IsometricSMul G G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ dist (a / b) (a / c) = dist b c

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Analysis/Convex/AmpleSet.lean
theorem ampleSet_univ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] :
    AmpleSet (univ : Set F)

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
a✝ : x ∈ univ
⊢ (convexHull ℝ) (connectedComponentIn univ x) = univ

Tactic:
rw [connectedComponentIn_univ, PreconnectedSpace.connectedComponent_eq_univ, convexHull_univ]

Result:
no goals

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
⊢ AmpleSet univ

Tactic:
intro x _

Result:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
a✝ : x ∈ univ
⊢ (convexHull ℝ) (connectedComponentIn univ x) = univ
-- Mathlib/SetTheory/Game/Basic.lean
theorem inv_eq_of_pos {x : PGame} (h : 0 < x) : x⁻¹ = inv' x

Proof state:
x : PGame
h : 0 < x
⊢ x⁻¹ = x.inv'

Tactic:
classical exact (if_neg h.lf.not_equiv').trans (if_pos h)

Result:
no goals

Proof state:
x : PGame
h : 0 < x
⊢ x⁻¹ = x.inv'

Tactic:
exact (if_neg h.lf.not_equiv').trans (if_pos h)

Result:
no goals
-- Mathlib/CategoryTheory/NatIso.lean
theorem cancel_natIso_inv_left {X : C} {Z : D} (g g' : F.obj X ⟶ Z) :
    α.inv.app X ≫ g = α.inv.app X ≫ g' ↔ g = g'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
X : C
Z : D
g g' : F.obj X ⟶ Z
⊢ α.inv.app X ≫ g = α.inv.app X ≫ g' ↔ g = g'

Tactic:
simp only [cancel_epi, refl]

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma rnDeriv_add (κ ν η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel ν] [IsFiniteKernel η]
    (a : α) :
    rnDeriv (κ + ν) η a =ᵐ[η a] rnDeriv κ η a + rnDeriv ν η a

Proof state:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ ν η : Kernel α γ
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel ν
inst✝ : IsFiniteKernel η
a : α
x : γ
h1 : (κ + ν).rnDeriv η a x = (∂(κ + ν) a/∂η a) x
h2 : κ.rnDeriv η a x = (∂κ a/∂η a) x
h3 : ν.rnDeriv η a x = (∂ν a/∂η a) x
h4 : (∂κ a + ν a/∂η a) x = (∂κ a/∂η a + ∂ν a/∂η a) x
⊢ (κ + ν).rnDeriv η a x = (κ.rnDeriv η a + ν.rnDeriv η a) x

Tactic:
rw [h1, Pi.add_apply, h2, h3, coe_add, Pi.add_apply, h4, Pi.add_apply]

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ ν η : Kernel α γ
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel ν
inst✝ : IsFiniteKernel η
a : α
⊢ (κ + ν).rnDeriv η a =ᶠ[ae (η a)] κ.rnDeriv η a + ν.rnDeriv η a

Tactic:
filter_upwards [(κ + ν).rnDeriv_eq_rnDeriv_measure, κ.rnDeriv_eq_rnDeriv_measure,
  ν.rnDeriv_eq_rnDeriv_measure, (κ a).rnDeriv_add (ν a) (η a)] with x h1 h2 h3 h4

Result:
case h
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ ν η : Kernel α γ
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel ν
inst✝ : IsFiniteKernel η
a : α
x : γ
h1 : (κ + ν).rnDeriv η a x = (∂(κ + ν) a/∂η a) x
h2 : κ.rnDeriv η a x = (∂κ a/∂η a) x
h3 : ν.rnDeriv η a x = (∂ν a/∂η a) x
h4 : (∂κ a + ν a/∂η a) x = (∂κ a/∂η a + ∂ν a/∂η a) x
⊢ (κ + ν).rnDeriv η a x = (κ.rnDeriv η a + ν.rnDeriv η a) x
-- Mathlib/Data/DFinsupp/Interval.lean
lemma card_Ico : #(Ico f g) = (∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i))) - 1

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Ico f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 1

Tactic:
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]

Result:
no goals