harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem start_mem_support {u v : V} (p : G.Walk u v) : u ∈ p.support

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u ∈ p.support

Tactic:
cases p <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_neg_one : arcsin (-1) = -(π / 2) :=
  arcsin_eq_of_sin_eq (by rw [sin_neg, sin_pi_div_two]) <|
    left_mem_Icc.2 (neg_le_self pi_div_two_pos.le)

Proof state:
⊢ sin (-(π / 2)) = -1

Tactic:
rw [sin_neg, sin_pi_div_two]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Prod.lean
theorem differentiableAt_finCons :
    DifferentiableAt 𝕜 (fun x => Fin.cons (φ x) (φs x)) x ↔
      DifferentiableAt 𝕜 φ x ∧ DifferentiableAt 𝕜 φs x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ (DifferentiableAt 𝕜 (fun x => Fin.cons (φ x) (φs x) 0) x ∧
      ∀ (i : Fin n), DifferentiableAt 𝕜 (fun x => Fin.cons (φ x) (φs x) i.succ) x) ↔
    DifferentiableAt 𝕜 φ x ∧ ∀ (i : Fin n), DifferentiableAt 𝕜 (fun x => φs x i) x

Tactic:
simp only [Fin.cons_zero, Fin.cons_succ]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ DifferentiableAt 𝕜 (fun x => Fin.cons (φ x) (φs x)) x ↔ DifferentiableAt 𝕜 φ x ∧ DifferentiableAt 𝕜 φs x

Tactic:
rw [differentiableAt_pi, Fin.forall_fin_succ, differentiableAt_pi]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
⊢ (DifferentiableAt 𝕜 (fun x => Fin.cons (φ x) (φs x) 0) x ∧
      ∀ (i : Fin n), DifferentiableAt 𝕜 (fun x => Fin.cons (φ x) (φs x) i.succ) x) ↔
    DifferentiableAt 𝕜 φ x ∧ ∀ (i : Fin n), DifferentiableAt 𝕜 (fun x => φs x i) x
-- Mathlib/LinearAlgebra/Prod.lean
theorem inl_map_mul (a₁ a₂ : A) :
    LinearMap.inl R A B (a₁ * a₂) = LinearMap.inl R A B a₁ * LinearMap.inl R A B a₂ :=
  Prod.ext rfl (by simp)

Proof state:
R : Type u
inst✝⁴ : Semiring R
A : Type u_4
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
B : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : Module R B
a₁ a₂ : A
⊢ ((inl R A B) (a₁ * a₂)).2 = ((inl R A B) a₁ * (inl R A B) a₂).2

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma Opens.isDominant_ι {U : X.Opens} (hU : Dense (X := X) U) : IsDominant U.ι :=
  ⟨by simpa [DenseRange] using hU⟩

Proof state:
X : Scheme
U : X.Opens
hU : Dense ↑U
⊢ DenseRange ⇑(ConcreteCategory.hom U.ι.base)

Tactic:
simpa [DenseRange] using hU

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_comm (s : Finset β) (t : Finset γ) (f : β → γ → α) :
    (s.sup fun b => t.sup (f b)) = t.sup fun c => s.sup fun b => f b c :=
  eq_of_forall_ge_iff fun a => by simpa using forall₂_swap

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
t : Finset γ
f : β → γ → α
a : α
⊢ (s.sup fun b => t.sup (f b)) ≤ a ↔ (t.sup fun c => s.sup fun b => f b c) ≤ a

Tactic:
simpa using forall₂_swap

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
/-- If `f` tends to negative infinity along a nontrivial filter `l`,
then `fun x ↦ f x / r` tends to infinity if and only if `r < 0`. -/
lemma tendsto_div_const_atTop_iff_neg [NeBot l] (h : Tendsto f l atBot) :
    Tendsto (fun x ↦ f x / r) l atTop ↔ r < 0

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

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atTop_iff_neg h]

Result:
no goals
-- Mathlib/Order/Filter/Curry.lean
theorem frequently_curry_iff
    (p : (α × β) → Prop) : (∃ᶠ x in l.curry m, p x) ↔ ∃ᶠ x in l, ∃ᶠ y in m, p (x, y)

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
p : α × β → Prop
⊢ (∃ᶠ (x : α × β) in l.curry m, p x) ↔ ∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, p (x, y)

Tactic:
simp_rw [Filter.Frequently, not_iff_not, not_not, eventually_curry_iff]

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
@[simp, norm_cast]
lemma coe_prod (s : Finset ι) (ψ : ι → AddChar A M) : ∏ i ∈ s, ψ i = ∏ i ∈ s, ⇑(ψ i)

Proof state:
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
⊢ ⇑(∏ i ∈ s, ψ i) = ∏ i ∈ s, ⇑(ψ i)

Tactic:
induction s using Finset.cons_induction <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Basic.lean
theorem mono_of_kernel_zero {X Y : C} {f : X ⟶ Y} [HasLimit (parallelPair f 0)]
    (w : kernel.ι f = 0) : Mono f :=
  mono_of_cancel_zero f fun g h => by rw [← kernel.lift_ι f g h, w, Limits.comp_zero]

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasLimit (parallelPair f 0)
w : kernel.ι f = 0
P✝ : C
g : P✝ ⟶ X
h : g ≫ f = 0
⊢ g = 0

Tactic:
rw [← kernel.lift_ι f g h, w, Limits.comp_zero]

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem toReal_eq_one_iff (x : ℝ≥0∞) : x.toReal = 1 ↔ x = 1

Proof state:
x : ℝ≥0∞
⊢ x.toReal = 1 ↔ x = 1

Tactic:
rw [ENNReal.toReal, NNReal.coe_eq_one, ENNReal.toNNReal_eq_one_iff]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
@[simp] lemma isLowerSet_shatterer (𝒜 : Finset (Finset α)) :
    IsLowerSet (𝒜.shatterer : Set (Finset α)) := fun s t ↦ by simpa using Shatters.mono_right

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
⊢ t ≤ s → s ∈ ↑𝒜.shatterer → t ∈ ↑𝒜.shatterer

Tactic:
simpa using Shatters.mono_right

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_mul_of_lt {w} {x y : BitVec w} (h : x.toNat * y.toNat < 2^w) :
    (x * y).toNat = x.toNat * y.toNat

Proof state:
w : Nat
x y : BitVec w
h : x.toNat * y.toNat < 2 ^ w
⊢ (x * y).toNat = x.toNat * y.toNat

Tactic:
rw [BitVec.toNat_mul, Nat.mod_eq_of_lt h]

Result:
no goals
-- Mathlib/Data/Finite/Prod.lean
theorem finite_prod : (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅)

Tactic:
simp only [← not_infinite, Set.infinite_prod, not_or, not_and_or, not_nonempty_iff_eq_empty]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_induction_nonempty {M : Type*} [CommMonoid M] (f : α → M) (p : M → Prop)
    (hom : ∀ a b, p a → p b → p (a * b)) (nonempty : s.Nonempty) (base : ∀ x ∈ s, p <| f x) :
    p <| ∏ x ∈ s, f x :=
  Multiset.prod_induction_nonempty p hom (by simp [nonempty_iff_ne_empty.mp nonempty])
    (Multiset.forall_mem_map_iff.mpr base)

Proof state:
α : Type u_3
s : Finset α
M : Type u_6
inst✝ : CommMonoid M
f : α → M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
nonempty : s.Nonempty
base : ∀ x ∈ s, p (f x)
⊢ Multiset.map (fun x => f x) s.val ≠ ∅

Tactic:
simp [nonempty_iff_ne_empty.mp nonempty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_and (x y i : Nat) : (x &&& y).testBit i = (x.testBit i && y.testBit i)

Proof state:
x y i : Nat
⊢ (x &&& y).testBit i = (x.testBit i && y.testBit i)

Tactic:
simp [HAnd.hAnd, AndOp.and, land, testBit_bitwise ]

Result:
no goals
-- Mathlib/Data/Finset/Disjoint.lean
theorem coe_disjUnion {s t : Finset α} (h : Disjoint s t) :
    (disjUnion s t h : Set α) = (s : Set α) ∪ t :=
  Set.ext <| by simp

Proof state:
α : Type u_1
s t : Finset α
h : Disjoint s t
⊢ ∀ (x : α), x ∈ ↑(s.disjUnion t h) ↔ x ∈ ↑s ∪ ↑t

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem of_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : P.toPoly = C P.d

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ P.toPoly = C P.d

Tactic:
rw [of_b_eq_zero ha hb, hc, C_0, zero_mul, zero_add]

Result:
no goals
-- Mathlib/Algebra/Group/Center.lean
theorem units_inv_mem_center {a : Mˣ} (ha : ↑a ∈ Set.center M) : ↑a⁻¹ ∈ Set.center M

Proof state:
M : Type u_1
inst✝ : Monoid M
a : Mˣ
ha : ↑a ∈ center M
⊢ ↑a⁻¹ ∈ center M

Tactic:
rw [Semigroup.mem_center_iff] at *

Result:
M : Type u_1
inst✝ : Monoid M
a : Mˣ
ha : ∀ (g : M), g * ↑a = ↑a * g
⊢ ∀ (g : M), g * ↑a⁻¹ = ↑a⁻¹ * g
-- Mathlib/Topology/GDelta/Basic.lean
/-- A set `s` is closed and nowhere dense iff its complement `sᶜ` is open and dense. -/
lemma isClosed_isNowhereDense_iff_compl {s : Set X} :
    IsClosed s ∧ IsNowhereDense s ↔ IsOpen sᶜ ∧ Dense sᶜ

Proof state:
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed s ∧ IsNowhereDense s ↔ IsOpen sᶜ ∧ Dense sᶜ

Tactic:
rw [and_congr_right IsClosed.isNowhereDense_iff,
  isOpen_compl_iff, interior_eq_empty_iff_dense_compl]

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

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

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Map2.lean
theorem map₂Right_nil_left : map₂Right f [] bs = bs.map (f none)

Proof state:
α : Type u
β : Type v
γ : Type w
f : Option α → β → γ
bs : List β
⊢ map₂Right f [] bs = map (f none) bs

Tactic:
cases bs <;> rfl

Result:
no goals
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem mul_charP_coeff_succ [CharP R p] (x : 𝕎 R) (i : ℕ) :
    (x * p).coeff (i + 1) = x.coeff i ^ p

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
i : ℕ
⊢ (x * ↑p).coeff (i + 1) = x.coeff i ^ p

Tactic:
rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_succ]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Set/Basic.lean
lemma zero_mul_subset (s : Set α) : 0 * s ⊆ 0

Proof state:
α : Type u_1
inst✝ : MulZeroClass α
s : Set α
⊢ 0 * s ⊆ 0

Tactic:
simp [subset_def, mem_mul]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem mul_coeff_zero (x y : 𝕎 R) : (x * y).coeff 0 = x.coeff 0 * y.coeff 0

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ (x * y).coeff 0 = x.coeff 0 * y.coeff 0

Tactic:
simp [mul_coeff, peval, Function.uncurry]

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem source_inter_preimage_inv_preimage (s : Set α) :
    e.source ∩ e ⁻¹' (e.symm ⁻¹' s) = e.source ∩ s :=
  Set.ext fun x => and_congr_right_iff.2 fun hx =>
    by simp only [mem_preimage, e.left_inv hx]

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
x : α
hx : x ∈ e.source
⊢ x ∈ ↑e ⁻¹' (↑e.symm ⁻¹' s) ↔ x ∈ s

Tactic:
simp only [mem_preimage, e.left_inv hx]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
@[simp]
lemma cosKernel_neg (a : UnitAddCircle) (x : ℝ) : cosKernel (-a) x = cosKernel a x

Proof state:
case H
x z✝ : ℝ
⊢ cosKernel (-↑z✝) x = cosKernel (↑z✝) x

Tactic:
simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, cosKernel_def]

Result:
no goals

Proof state:
a : UnitAddCircle
x : ℝ
⊢ cosKernel (-a) x = cosKernel a x

Tactic:
induction a using QuotientAddGroup.induction_on with
| H => simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, cosKernel_def]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddTorsor.lean
theorem dist_vadd_vadd_le (v v' : V) (p p' : P) :
    dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p'

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v v' : V
p p' : P
⊢ dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p'

Tactic:
simpa using dist_triangle (v +ᵥ p) (v' +ᵥ p) (v' +ᵥ p')

Result:
no goals
-- Mathlib/Algebra/DirectSum/Basic.lean
theorem fromAddMonoid_of (i : ι) (f : γ →+ β i) : fromAddMonoid (of _ i f) = (of _ i).comp f

Proof state:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
⊢ (AddMonoidHom.compHom (of β i)) f = (of β i).comp f

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
⊢ fromAddMonoid ((of (fun i => γ →+ β i) i) f) = (of β i).comp f

Tactic:
rw [fromAddMonoid, toAddMonoid_of]

Result:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
⊢ (AddMonoidHom.compHom (of β i)) f = (of β i).comp f
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem ι_mul_ι_mul_of_isOrtho (x : CliffordAlgebra Q) {a b : M} (h : Q.IsOrtho a b) :
    ι Q a * (ι Q b * x) = -(ι Q b * (ι Q a * x))

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
a b : M
h : QuadraticMap.IsOrtho Q a b
⊢ (ι Q) a * ((ι Q) b * x) = -((ι Q) b * ((ι Q) a * x))

Tactic:
rw [← mul_assoc, ι_mul_ι_comm_of_isOrtho h, neg_mul, mul_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/ContinuousFunctions.lean
theorem hasSum_of_hasSum_Lp {β : Type*} [μ.IsOpenPosMeasure] [NormedField 𝕜] [NormedSpace 𝕜 E]
    {g : β → C(α, E)} {f : C(α, E)} (hg : Summable g)
    (hg2 : HasSum (toLp (E := E) p μ 𝕜 ∘ g) (toLp (E := E) p μ 𝕜 f)) : HasSum g f

Proof state:
case h.e'_6
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : CompactSpace α
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
β : Type u_4
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
g : β → C(α, E)
f : C(α, E)
hg : Summable g
hg2 : HasSum (⇑(toLp p μ 𝕜) ∘ g) ((toLp p μ 𝕜) f)
⊢ f = ∑' (b : β), g b

Tactic:
exact toLp_injective μ (hg2.unique ((toLp p μ 𝕜).hasSum <| Summable.hasSum hg))

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : CompactSpace α
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
β : Type u_4
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
g : β → C(α, E)
f : C(α, E)
hg : Summable g
hg2 : HasSum (⇑(toLp p μ 𝕜) ∘ g) ((toLp p μ 𝕜) f)
⊢ HasSum g f

Tactic:
convert Summable.hasSum hg

Result:
case h.e'_6
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopologyEither α E
inst✝⁵ : CompactSpace α
inst✝⁴ : IsFiniteMeasure μ
𝕜 : Type u_3
inst✝³ : Fact (1 ≤ p)
β : Type u_4
inst✝² : μ.IsOpenPosMeasure
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
g : β → C(α, E)
f : C(α, E)
hg : Summable g
hg2 : HasSum (⇑(toLp p μ 𝕜) ∘ g) ((toLp p μ 𝕜) f)
⊢ f = ∑' (b : β), g b
-- Mathlib/Order/LiminfLimsup.lean
theorem cofinite.liminf_set_eq : liminf s cofinite = { x | { n | x ∉ s n }.Finite }

Proof state:
α : Type u_1
ι : Type u_4
s : ι → Set α
⊢ liminf s cofinite = {x | {n | x ∉ s n}.Finite}

Tactic:
simp only [← cofinite.bliminf_true s, cofinite.bliminf_set_eq, true_and]

Result:
no goals
-- Mathlib/Analysis/Convex/Hull.lean
theorem mem_convexHull_iff : x ∈ convexHull 𝕜 s ↔ ∀ t, s ⊆ t → Convex 𝕜 t → x ∈ t

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
x : E
⊢ x ∈ (convexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → Convex 𝕜 t → x ∈ t

Tactic:
simp_rw [convexHull_eq_iInter, mem_iInter]

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

Tactic:
simpa only [mul_comm] using tendsto_const_mul_atBot_of_neg hr

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem add_one : ∀ n : ZNum, n + 1 = succ n
  | 0 => rfl
  | pos p => congr_arg pos p.add_one
  | neg p => by cases p <;> rfl

Proof state:
p : PosNum
⊢ neg p + 1 = (neg p).succ

Tactic:
cases p <;> rfl

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
lemma XIsoOfEq_shift (K : CochainComplex C ℤ) (n : ℤ) {p q : ℤ} (hpq : p = q) :
    (K⟦n⟧).XIsoOfEq hpq = K.XIsoOfEq (show p + n = q + n by rw [hpq]) := rfl

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
n p q : ℤ
hpq : p = q
⊢ p + n = q + n

Tactic:
rw [hpq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
theorem arg_exp {x : ℝ} (h₁ : -π < x) (h₂ : x ≤ π) : arg (exp x) = x

Proof state:
x : ℝ
h₁ : -π < x
h₂ : x ≤ π
⊢ (↑(exp x)).arg = x

Tactic:
rw [coe_exp, exp_mul_I, arg_cos_add_sin_mul_I ⟨h₁, h₂⟩]

Result:
no goals
-- Mathlib/Order/Filter/FilterProduct.lean
theorem const_min [LinearOrder β] (x y : β) : (↑(min x y : β) : β*) = min ↑x ↑y

Proof state:
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : β
⊢ ↑(x ⊓ y) = ↑x ⊓ ↑y

Tactic:
rw [min_def, map₂_const]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem filter_eq_sum (p : α → Prop) [DecidablePred p] (f : α →₀ M) :
    f.filter p = ∑ i ∈ f.support.filter p, single i (f i) :=
  (f.filter p).sum_single.symm.trans <|
    Finset.sum_congr rfl fun x hx => by
      rw [filter_apply_pos _ _ (mem_filter.1 hx).2]

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : AddCommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f : α →₀ M
x : α
hx : x ∈ Finset.filter p f.support
⊢ single x ((filter p f) x) = single x (f x)

Tactic:
rw [filter_apply_pos _ _ (mem_filter.1 hx).2]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem vsub_right_mem_direction_iff_mem {s : AffineSubspace k P} {p : P} (hp : p ∈ s) (p₂ : P) :
    p₂ -ᵥ p ∈ s.direction ↔ p₂ ∈ s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p₂ : P
⊢ p₂ -ᵥ p ∈ s.direction ↔ p₂ ∈ s

Tactic:
rw [mem_direction_iff_eq_vsub_right hp]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p₂ : P
⊢ (∃ p₂_1 ∈ s, p₂ -ᵥ p = p₂_1 -ᵥ p) ↔ p₂ ∈ s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
p₂ : P
⊢ (∃ p₂_1 ∈ s, p₂ -ᵥ p = p₂_1 -ᵥ p) ↔ p₂ ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem RedRed.balance2 {l : RBNode α} {v : α} {r : RBNode α}
    (hl : l.Balanced c n) (hr : r.RedRed p n) : ∃ c, (balance2 l v r).Balanced c (n + 1) :=
  (hr.reverse.balance1 hl.reverse (v := v)).imp fun _ h => by simpa using h.reverse

Proof state:
α : Type u_1
c : RBColor
n : Nat
p : Prop
l : RBNode α
v : α
r : RBNode α
hl : l.Balanced c n
hr : RedRed p r n
x✝ : RBColor
h : (r.reverse.balance1 v l.reverse).Balanced x✝ (n + 1)
⊢ (l.balance2 v r).Balanced x✝ (n + 1)

Tactic:
simpa using h.reverse

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_filter_ne_nil [DecidablePred fun l : List α => l ≠ []] {L : List (List α)} :
    flatten (L.filter fun l => l ≠ []) = L.flatten

Proof state:
α : Type u_1
inst✝ : DecidablePred fun l => l ≠ []
L : List (List α)
⊢ (filter (fun l => decide (l ≠ [])) L).flatten = L.flatten

Tactic:
simp only [ne_eq, ← isEmpty_iff, Bool.not_eq_true, Bool.decide_eq_false,
  flatten_filter_not_isEmpty]

Result:
no goals
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem eq_of_comp_right_eq' (f g : Y ⟶ Z)
    (w : (fun {X} (h : X ⟶ Y) => h ≫ f) = fun {X} (h : X ⟶ Y) => h ≫ g) : f = g :=
  eq_of_comp_right_eq @fun X h => by convert congr_fun (congr_fun w X) h

Proof state:
C : Type u
inst✝ : Category.{v, u} C
Y Z : C
f g : Y ⟶ Z
w : (fun {X} h => h ≫ f) = fun {X} h => h ≫ g
X : C
h : X ⟶ Y
⊢ h ≫ f = h ≫ g

Tactic:
convert congr_fun (congr_fun w X) h

Result:
no goals
-- Mathlib/Data/Nat/Cast/Defs.lean
theorem two_add_two_eq_four [AddMonoidWithOne R] : 2 + 2 = (4 : R)

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 2 + 2 = 4

Tactic:
simp [← one_add_one_eq_two, ← Nat.cast_one, ← three_add_one_eq_four,
  ← two_add_one_eq_three, add_assoc]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem eventually_imp_distrib_left {f : Filter α} {p : Prop} {q : α → Prop} :
    (∀ᶠ x in f, p → q x) ↔ p → ∀ᶠ x in f, q x

Proof state:
α : Type u
f : Filter α
p : Prop
q : α → Prop
⊢ (∀ᶠ (x : α) in f, p → q x) ↔ p → ∀ᶠ (x : α) in f, q x

Tactic:
simp only [imp_iff_not_or, eventually_or_distrib_left]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_X_sub_C_sq (c : R) : derivative ((X - C c) ^ 2) = C 2 * (X - C c)

Proof state:
R : Type u
inst✝ : CommRing R
c : R
⊢ derivative ((X - C c) ^ 2) = C 2 * (X - C c)

Tactic:
rw [derivative_sq, derivative_X_sub_C, mul_one]

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem codisjoint_inf_left : Codisjoint (a ⊓ b) c ↔ Codisjoint a c ∧ Codisjoint b c

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
⊢ Codisjoint (a ⊓ b) c ↔ Codisjoint a c ∧ Codisjoint b c

Tactic:
simp only [codisjoint_iff, sup_inf_right, inf_eq_top_iff]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Tower.lean
theorem aeval_algebraMap_apply (x : A) (p : R[X]) :
    aeval (algebraMap A B x) p = algebraMap A B (aeval x p)

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
p : R[X]
⊢ (aeval ((algebraMap A B) x)) p = (algebraMap A B) ((aeval x) p)

Tactic:
rw [aeval_def, aeval_def, hom_eval₂, ← IsScalarTower.algebraMap_eq]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem support_finRotate {n : ℕ} : support (finRotate (n + 2)) = Finset.univ

Proof state:
case h
n : ℕ
a✝ : Fin (n + 2)
⊢ a✝ ∈ (finRotate (n + 2)).support ↔ a✝ ∈ Finset.univ

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ (finRotate (n + 2)).support = Finset.univ

Tactic:
ext

Result:
case h
n : ℕ
a✝ : Fin (n + 2)
⊢ a✝ ∈ (finRotate (n + 2)).support ↔ a✝ ∈ Finset.univ
-- Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean
@[to_additive]
lemma sInf_div : sInf (s / t) = sInf s / sSup t

Proof state:
M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
⊢ sInf (s / t) = sInf s / sSup t

Tactic:
simp_rw [div_eq_mul_inv, sInf_mul, sInf_inv]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem infDist_smul₀ {c : 𝕜} (hc : c ≠ 0) (s : Set E) (x : E) :
    Metric.infDist (c • x) (c • s) = ‖c‖ * Metric.infDist x s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ infDist (c • x) (c • s) = ‖c‖ * infDist x s

Tactic:
simp_rw [Metric.infDist, infEdist_smul₀ hc s, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm,
  smul_eq_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem fst_zero : fst (0 : Measure (α × β)) = 0

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ fst 0 = 0

Tactic:
simp [fst]

Result:
no goals