harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Finite/Lattice.lean
theorem Infinite.biUnion {ι : Type*} {s : ι → Set α} {a : Set ι} (ha : a.Infinite)
    (hs : a.InjOn s) : (⋃ i ∈ a, s i).Infinite

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
x✝² : Infinite ↑a
x✝¹ x✝ : ↑a
i : ι
hi : i ∈ a
j : ι
hj : j ∈ a
hij : s ↑⟨i, hi⟩ = s ↑⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
simp [hs hi hj hij]

Result:
no goals

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ i ∈ a, s i).Infinite

Tactic:
rw [biUnion_eq_iUnion]

Result:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ x, s ↑x).Infinite

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ x, s ↑x).Infinite

Tactic:
have _ := ha.to_subtype

Result:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
x✝ : Infinite ↑a
⊢ (⋃ x, s ↑x).Infinite

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
x✝ : Infinite ↑a
⊢ (⋃ x, s ↑x).Infinite

Tactic:
exact infinite_iUnion fun ⟨i,hi⟩ ⟨j,hj⟩ hij ↦ by simp [hs hi hj hij]

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_eq_mulIndicator {t : Set β} {g : β → M} {b : β}
    (h1 : a ∈ s ↔ b ∈ t) (h2 : f a = g b) :
    s.mulIndicator f a = t.mulIndicator g b

Proof state:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
t : Set β
g : β → M
b : β
h1 : a ∈ s ↔ b ∈ t
h2 : f a = g b
⊢ s.mulIndicator f a = t.mulIndicator g b

Tactic:
by_cases a ∈ s <;> simp_all

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem toList_getElem_zero (h : x ∈ p.support) :
    (toList p x)[0]'(length_toList_pos_of_mem_support _ _ h) = x

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
h : x ∈ p.support
⊢ (p.toList x)[0] = x

Tactic:
simp [toList]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/CompactlySupported.lean
lemma coe_compLeft {g : C(β, γ)} (hg : g 0 = 0) (f : C_c(α, β)) : f.compLeft g = g ∘ f

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
γ : Type u_5
inst✝¹ : TopologicalSpace γ
inst✝ : Zero γ
g : C(β, γ)
hg : g 0 = 0
f : α →C_c β
⊢ ⇑(compLeft g f) = ⇑g ∘ ⇑f

Tactic:
simp [compLeft, if_pos hg]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueFree_iff {n : ℕ} : G.CliqueFree n ↔ IsEmpty ((⊤ : SimpleGraph (Fin n)) ↪g G)

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.CliqueFree n ↔ IsEmpty (⊤ ↪g G)

Tactic:
rw [← not_iff_not, not_cliqueFree_iff, not_isEmpty_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_const_sub_Icc : (fun x => a - x) '' Icc b c = Icc (a - c) (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Icc b c = Icc (a - c) (a - b)

Tactic:
dsimp [Function.comp_def] at this

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Icc b c = Icc (a - c) (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' Icc b c = Icc (a - c) (a - b)

Tactic:
have := image_comp (fun x => a + x) fun x => -x

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Icc b c = Icc (a - c) (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Icc b c = Icc (a - c) (a - b)

Tactic:
simp [sub_eq_add_neg, this, add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem bnot_isRight (x : α ⊕ β) : !x.isRight = x.isLeft

Proof state:
α : Type u_1
β : Type u_2
x : α ⊕ β
⊢ (!decide (x.isRight = x.isLeft)) = true

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Data/List/Destutter.lean
theorem destutter'_is_chain' (a) : (l.destutter' R a).Chain' R

Proof state:
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
⊢ Chain' R (if R a b then a :: destutter' R b l else destutter' R a l)

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
h : R a b
⊢ Chain' R (a :: destutter' R b l)

case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
h : ¬R a b
⊢ Chain' R (destutter' R a l)

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

Tactic:
induction' l with b l hl generalizing a

Result:
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ Chain' R (destutter' R a [])

case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
⊢ Chain' R (destutter' R a (b :: l))

Proof state:
case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
h : ¬R a b
⊢ Chain' R (destutter' R a l)

Tactic:
exact hl a

Result:
no goals

Proof state:
case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
h : R a b
⊢ Chain' R (a :: destutter' R b l)

Tactic:
exact destutter'_is_chain R l h

Result:
no goals

Proof state:
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
⊢ Chain' R (destutter' R a (b :: l))

Tactic:
rw [destutter']

Result:
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
⊢ Chain' R (if R a b then a :: destutter' R b l else destutter' R a l)

Proof state:
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ Chain' R (destutter' R a [])

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
lemma isomorphic_distinguished (T₁ : Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
    (hT₁ : T₁ ∈ distinguishedTriangles C) (T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
    (e : T₂ ≅ T₁) : T₂ ∈ distinguishedTriangles C

Proof state:
case intro.intro.intro.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
e : T₂ ≅ T₁
X Y : CochainComplex C ℤ
f : X ⟶ Y
e' : T₁ ≅ CochainComplex.mappingCone.triangleh f
⊢ T₂ ∈ distinguishedTriangles C

Tactic:
exact ⟨X, Y, f, ⟨e ≪≫ e'⟩⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T₁ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT₁ : T₁ ∈ distinguishedTriangles C
T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
e : T₂ ≅ T₁
⊢ T₂ ∈ distinguishedTriangles C

Tactic:
obtain ⟨X, Y, f, ⟨e'⟩⟩ := hT₁

Result:
case intro.intro.intro.intro
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
e : T₂ ≅ T₁
X Y : CochainComplex C ℤ
f : X ⟶ Y
e' : T₁ ≅ CochainComplex.mappingCone.triangleh f
⊢ T₂ ∈ distinguishedTriangles C
-- Mathlib/Analysis/Normed/Group/Bounded.lean
@[to_additive (attr := simp)]
lemma Filter.inv_cobounded : (cobounded E)⁻¹ = cobounded E

Proof state:
E : Type u_2
inst✝ : SeminormedGroup E
⊢ (cobounded E)⁻¹ = cobounded E

Tactic:
simp only [← comap_norm_atTop', ← Filter.comap_inv, comap_comap, Function.comp_def, norm_inv']

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem neg_one_pow {m n : ℕ} (hm : Odd m) (hn : Odd n) :
    qrSign m n = (-1) ^ (m / 2 * (n / 2))

Proof state:
m n : ℕ
hm : Odd m
hn : Odd n
⊢ qrSign m n = (-1) ^ (m / 2 * (n / 2))

Tactic:
rw [qrSign, pow_mul, ← χ₄_eq_neg_one_pow (odd_iff.mp hm)]

Result:
m n : ℕ
hm : Odd m
hn : Odd n
⊢ J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)

Proof state:
m n : ℕ
hm : Odd m
hn : Odd n
⊢ J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)

Tactic:
rcases odd_mod_four_iff.mp (odd_iff.mp hm) with h | h

Result:
case inl
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 1
⊢ J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)

case inr
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 3
⊢ J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)

Proof state:
case inr
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 3
⊢ J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)

Tactic:
rw [χ₄_nat_three_mod_four h, ← χ₄_eq_neg_one_pow (odd_iff.mp hn), jacobiSym.at_neg_one hn]

Result:
no goals

Proof state:
case inl
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 1
⊢ J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)

Tactic:
rw [χ₄_nat_one_mod_four h, jacobiSym.one_left, one_pow]

Result:
no goals
-- Mathlib/GroupTheory/Coset/Defs.lean
theorem rightRel_eq : ⇑(rightRel s) = fun x y => y * x⁻¹ ∈ s :=
  funext₂ <| by
    simp only [eq_iff_iff]
    apply rightRel_apply

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), (rightRel s) a b = (b * a⁻¹ ∈ s)

Tactic:
simp only [eq_iff_iff]

Result:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), (rightRel s) a b ↔ b * a⁻¹ ∈ s

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), (rightRel s) a b ↔ b * a⁻¹ ∈ s

Tactic:
apply rightRel_apply

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma P4_neg_left : P4 x₁ x₂ y ↔ P4 (-x₂) (-x₁) y

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

Tactic:
simp_rw [P4, PGame.neg_lt_neg_iff, moveLeft_neg, ← P3_neg]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem leadingCoeff_ne_zero : leadingCoeff p ≠ 0 ↔ p ≠ 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.leadingCoeff ≠ 0 ↔ p ≠ 0

Tactic:
rw [Ne, leadingCoeff_eq_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem sum_toMatrix_smul_self [Fintype ι] : ∑ i : ι, e.toMatrix v i j • e i = v j

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : Fintype ι
⊢ ∑ i : ι, e.toMatrix v i j • e i = v j

Tactic:
simp_rw [e.toMatrix_apply, e.sum_repr]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Comap.lean
theorem comap_id : comap (AlgHom.id R (MvPolynomial σ R)) = id

Proof state:
case h
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = id x

Tactic:
exact comap_id_apply x

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) = id

Tactic:
funext x

Result:
case h
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = id x
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem lt_log_iff_exp_lt (hy : 0 < y) : x < log y ↔ exp x < y

Proof state:
x y : ℝ
hy : 0 < y
⊢ x < log y ↔ rexp x < y

Tactic:
rw [← exp_lt_exp, exp_log hy]

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem submartingale_of_condExp_sub_nonneg [IsFiniteMeasure μ] {f : ι → Ω → ℝ} (hadp : Adapted ℱ f)
    (hint : ∀ i, Integrable (f i) μ) (hf : ∀ i j, i ≤ j → 0 ≤ᵐ[μ] μ[f j - f i|ℱ i]) :
    Submartingale f ℱ μ

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : IsFiniteMeasure μ
f : ι → Ω → ℝ
hadp : Adapted ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]
i j : ι
hij : i ≤ j
⊢ f i ≤ᶠ[ae μ] μ[f j|↑ℱ i]

Tactic:
rw [← condExp_of_stronglyMeasurable (ℱ.le _) (hadp _) (hint _), ← eventually_sub_nonneg]

Result:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : IsFiniteMeasure μ
f : ι → Ω → ℝ
hadp : Adapted ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]
i j : ι
hij : i ≤ j
⊢ 0 ≤ᶠ[ae μ] μ[f j|↑ℱ i] - μ[f i|↑ℱ i]

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : IsFiniteMeasure μ
f : ι → Ω → ℝ
hadp : Adapted ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]
i j : ι
hij : i ≤ j
⊢ 0 ≤ᶠ[ae μ] μ[f j|↑ℱ i] - μ[f i|↑ℱ i]

Tactic:
exact EventuallyLE.trans (hf i j hij) (condExp_sub (hint _) (hint _) _).le

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : IsFiniteMeasure μ
f : ι → Ω → ℝ
hadp : Adapted ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]
⊢ Submartingale f ℱ μ

Tactic:
refine ⟨hadp, fun i j hij => ?_, hint⟩

Result:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : IsFiniteMeasure μ
f : ι → Ω → ℝ
hadp : Adapted ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
hf : ∀ (i j : ι), i ≤ j → 0 ≤ᶠ[ae μ] μ[f j - f i|↑ℱ i]
i j : ι
hij : i ≤ j
⊢ f i ≤ᶠ[ae μ] μ[f j|↑ℱ i]
-- Mathlib/GroupTheory/Sylow.lean
theorem QuotientGroup.card_preimage_mk (s : Subgroup G) (t : Set (G ⧸ s)) :
    Nat.card (QuotientGroup.mk ⁻¹' t) = Nat.card s * Nat.card t

Proof state:
G : Type u
inst✝ : Group G
s : Subgroup G
t : Set (G ⧸ s)
⊢ Nat.card ↑(mk ⁻¹' t) = Nat.card ↥s * Nat.card ↑t

Tactic:
rw [← Nat.card_prod, Nat.card_congr (preimageMkEquivSubgroupProdSet _ _)]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
theorem IsSymmSndFDerivWithinAt.congr_set (h : IsSymmSndFDerivWithinAt 𝕜 f s x)
    (hst : s =ᶠ[𝓝 x] t) : IsSymmSndFDerivWithinAt 𝕜 f t x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
v w : E
⊢ ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) w) v

Tactic:
exact h v w

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
v w : E
⊢ ((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x) w) v

Tactic:
rw [fderivWithin_fderivWithin_eq_of_eventuallyEq hst.symm]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
v w : E
⊢ ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s x) w) v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
⊢ IsSymmSndFDerivWithinAt 𝕜 f t x

Tactic:
intro v w

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
f : E → F
x : E
h : IsSymmSndFDerivWithinAt 𝕜 f s x
hst : s =ᶠ[𝓝 x] t
v w : E
⊢ ((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x) v) w = ((fderivWithin 𝕜 (fderivWithin 𝕜 f t) t x) w) v
-- Mathlib/MeasureTheory/Function/Egorov.lean
theorem mem_notConvergentSeq_iff [Preorder ι] {x : α} :
    x ∈ notConvergentSeq f g n j ↔ ∃ k ≥ j, 1 / (n + 1 : ℝ) < dist (f k x) (g x)

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : MetricSpace β
n : ℕ
j : ι
f : ι → α → β
g : α → β
inst✝ : Preorder ι
x : α
⊢ x ∈ notConvergentSeq f g n j ↔ ∃ k ≥ j, 1 / (↑n + 1) < dist (f k x) (g x)

Tactic:
simp_rw [notConvergentSeq, Set.mem_iUnion, exists_prop, mem_setOf]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem map_valEmbedding_Ico : (Ico a b).map Fin.valEmbedding = Ico ↑a ↑b

Proof state:
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ico a b) = Ico ↑a ↑b

Tactic:
simp [Ico_eq_finset_subtype, Finset.fin, Finset.map_map]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem isoOfComponents_app (f : ∀ i, C₁.X i ≅ C₂.X i)
    (hf : ∀ i j, c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom) (i : ι) :
    isoApp (isoOfComponents f hf) i = f i

Proof state:
case w
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ (isoApp (isoOfComponents f hf) i).hom = (f i).hom

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ isoApp (isoOfComponents f hf) i = f i

Tactic:
ext

Result:
case w
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ (isoApp (isoOfComponents f hf) i).hom = (f i).hom
-- Mathlib/Combinatorics/Additive/Dissociation.lean
@[to_additive (attr := simp)]
lemma mem_mulSpan :
    a ∈ mulSpan s ↔ ∃ ε : α → ℤ, (∀ a, ε a = -1 ∨ ε a = 0 ∨ ε a = 1) ∧ ∏ a ∈ s, a ^ ε a = a

Proof state:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
a : α
⊢ a ∈ s.mulSpan ↔ ∃ ε, (∀ (a : α), ε a = -1 ∨ ε a = 0 ∨ ε a = 1) ∧ ∏ a ∈ s, a ^ ε a = a

Tactic:
simp [mulSpan]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem UniformSpace.hasBasis_nhds (x : α) :
    HasBasis (𝓝 x) (fun s : Set (α × α) => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => ball x s :=
  ⟨fun t => by simp [UniformSpace.mem_nhds_iff_symm, and_assoc]⟩

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
t : Set α
⊢ t ∈ 𝓝 x ↔ ∃ i, (i ∈ 𝓤 α ∧ SymmetricRel i) ∧ ball x i ⊆ t

Tactic:
simp [UniformSpace.mem_nhds_iff_symm, and_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
lemma continuous_integral_boundedContinuousFunction
    {α : Type*} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (f : α →ᵇ ℝ) :
    Continuous fun μ : ProbabilityMeasure α ↦ ∫ x, f x ∂μ

Proof state:
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : ProbabilityMeasure α
⊢ ContinuousAt (fun μ => ∫ (x : α), f x ∂↑μ) μ

Tactic:
exact continuousAt_of_tendsto_nhds
  (ProbabilityMeasure.tendsto_iff_forall_integral_tendsto.mp tendsto_id f)

Result:
no goals

Proof state:
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
⊢ Continuous fun μ => ∫ (x : α), f x ∂↑μ

Tactic:
rw [continuous_iff_continuousAt]

Result:
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
⊢ ∀ (x : ProbabilityMeasure α), ContinuousAt (fun μ => ∫ (x : α), f x ∂↑μ) x

Proof state:
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
⊢ ∀ (x : ProbabilityMeasure α), ContinuousAt (fun μ => ∫ (x : α), f x ∂↑μ) x

Tactic:
intro μ

Result:
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : α →ᵇ ℝ
μ : ProbabilityMeasure α
⊢ ContinuousAt (fun μ => ∫ (x : α), f x ∂↑μ) μ
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem insertManyIfNewUnit_nil (h : m.WF) :
    insertManyIfNewUnit m [] = m

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => Unit
h : m.WF
⊢ (Raw₀.Const.insertManyIfNewUnit ⟨m, ⋯⟩ []).val.val = m

Tactic:
rw [Raw₀.Const.insertManyIfNewUnit_nil]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => Unit
h : m.WF
⊢ insertManyIfNewUnit m [] = m

Tactic:
simp_to_raw

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => Unit
h : m.WF
⊢ (Raw₀.Const.insertManyIfNewUnit ⟨m, ⋯⟩ []).val.val = m
-- Mathlib/CategoryTheory/Sites/Localization.lean
lemma W_eq_inverseImage_isomorphisms_of_adjunction (adj : G ⊣ sheafToPresheaf J A) :
    J.W = (MorphismProperty.isomorphisms _).inverseImage G

Proof state:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_3, u_2} A
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
⊢ J.W = (MorphismProperty.isomorphisms (Sheaf J A)).inverseImage G

Tactic:
rw [W_eq_W_range_sheafToPresheaf_obj,
  LeftBousfield.W_eq_inverseImage_isomorphisms adj]

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
lemma le_liminf_mul (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) :
    liminf u f * liminf v f ≤ liminf (u * v) f

Proof state:
case h
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
a : EReal
ha : a ∈ Ico 0 (liminf u f)
b : EReal
hb : b ∈ Ico 0 (liminf v f)
c : EReal
c_ab : c < a * b
x : α
xa : a < u x
xb : b < v x
⊢ c < u x * v x

Tactic:
exact c_ab.trans_le (mul_le_mul xa.le xb.le (mem_Ico.1 hb).1 ((mem_Ico.1 ha).1.trans xa.le))

Result:
no goals

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
a : EReal
ha : a ∈ Ico 0 (liminf u f)
b : EReal
hb : b ∈ Ico 0 (liminf v f)
c : EReal
c_ab : c < a * b
⊢ ∀ᶠ (a : α) in f, c < u a * v a

Tactic:
filter_upwards [eventually_lt_of_lt_liminf (mem_Ico.1 ha).2,
  eventually_lt_of_lt_liminf (mem_Ico.1 hb).2] with x xa xb

Result:
case h
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
a : EReal
ha : a ∈ Ico 0 (liminf u f)
b : EReal
hb : b ∈ Ico 0 (liminf v f)
c : EReal
c_ab : c < a * b
x : α
xa : a < u x
xb : b < v x
⊢ c < u x * v x

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
⊢ liminf u f * liminf v f ≤ liminf (u * v) f

Tactic:
apply mul_le_of_forall_lt_of_nonneg ((le_liminf_of_le) hu)
  <| (le_liminf_of_le) ((hu.and hv).mono fun x ⟨u0, v0⟩ ↦ mul_nonneg u0 v0)

Result:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
⊢ ∀ a' ∈ Ico 0 (liminf u f), ∀ b' ∈ Ico 0 (liminf v f), a' * b' ≤ liminf (fun x => u x * v x) f

Proof state:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
⊢ ∀ a' ∈ Ico 0 (liminf u f), ∀ b' ∈ Ico 0 (liminf v f), a' * b' ≤ liminf (fun x => u x * v x) f

Tactic:
refine fun a ha b hb ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_

Result:
α : Type u_3
f : Filter α
u v : α → EReal
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
a : EReal
ha : a ∈ Ico 0 (liminf u f)
b : EReal
hb : b ∈ Ico 0 (liminf v f)
c : EReal
c_ab : c < a * b
⊢ ∀ᶠ (a : α) in f, c < u a * v a