harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_insertListConst [BEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} :
    (List.insertListConst l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
⊢ (insertListConst l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty)

Tactic:
unfold insertListConst

Result:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
⊢ (insertList l (List.map Prod.toSigma toInsert)).isEmpty = (l.isEmpty && toInsert.isEmpty)

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
⊢ (l.isEmpty && (List.map Prod.toSigma toInsert).isEmpty) = true ↔ (l.isEmpty && toInsert.isEmpty) = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
⊢ (insertList l (List.map Prod.toSigma toInsert)).isEmpty = (l.isEmpty && toInsert.isEmpty)

Tactic:
rw [isEmpty_insertList, Bool.eq_iff_iff]

Result:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
⊢ (l.isEmpty && (List.map Prod.toSigma toInsert).isEmpty) = true ↔ (l.isEmpty && toInsert.isEmpty) = true
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem snd_mem_support_of_mem_edges {t u v w : V} (p : G.Walk v w) (he : s(t, u) ∈ p.edges) :
    u ∈ p.support

Proof state:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he : s(t, u) ∈ p.edges
⊢ u ∈ p.support

Tactic:
rw [Sym2.eq_swap] at he

Result:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he : s(u, t) ∈ p.edges
⊢ u ∈ p.support

Proof state:
V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk v w
he : s(u, t) ∈ p.edges
⊢ u ∈ p.support

Tactic:
exact p.fst_mem_support_of_mem_edges he

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/PDeriv.lean
theorem pderiv_C_mul {f : MvPolynomial σ R} {i : σ} : pderiv i (C a * f) = C a * pderiv i f

Proof state:
R : Type u
σ : Type v
a : R
inst✝ : CommSemiring R
f : MvPolynomial σ R
i : σ
⊢ (pderiv i) (C a * f) = C a * (pderiv i) f

Tactic:
rw [C_mul', Derivation.map_smul, C_mul']

Result:
no goals
-- Mathlib/LinearAlgebra/Semisimple.lean
theorem IsSemisimple.minpoly_squarefree : Squarefree (minpoly K f) :=
  IsRadical.squarefree (minpoly.ne_zero <| Algebra.IsIntegral.isIntegral _) <| by
    rw [isRadical_iff_span_singleton, span_minpoly_eq_annihilator]; exact hf.annihilator_isRadical

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
⊢ (annihilator K[X] (AEval' f)).IsRadical

Tactic:
exact hf.annihilator_isRadical

Result:
no goals

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
⊢ IsRadical (minpoly K f)

Tactic:
rw [isRadical_iff_span_singleton, span_minpoly_eq_annihilator]

Result:
M : Type u_2
inst✝³ : AddCommGroup M
K : Type u_3
inst✝² : Field K
inst✝¹ : Module K M
f : End K M
inst✝ : FiniteDimensional K M
hf : f.IsSemisimple
⊢ (annihilator K[X] (AEval' f)).IsRadical
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem monotone_bind
    (m : Type u → Type v) [Bind m] [∀ α, PartialOrder (m α)] [MonoBind m]
    {α β : Type u}
    {γ : Type w} [PartialOrder γ]
    (f : γ → m α) (g : γ → α → m β)
    (hmono₁ : monotone f)
    (hmono₂ : monotone g) :
    monotone (fun (x : γ) => f x >>= g x)

Proof state:
m : Type u → Type v
inst✝³ : Bind m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → m α
g : γ → α → m β
hmono₁ : monotone f
hmono₂ : monotone g
⊢ monotone fun x => f x >>= g x

Tactic:
intro x₁ x₂ hx₁₂

Result:
m : Type u → Type v
inst✝³ : Bind m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → m α
g : γ → α → m β
hmono₁ : monotone f
hmono₂ : monotone g
x₁ x₂ : γ
hx₁₂ : x₁ ⊑ x₂
⊢ (fun x => f x >>= g x) x₁ ⊑ (fun x => f x >>= g x) x₂

Proof state:
case a
m : Type u → Type v
inst✝³ : Bind m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → m α
g : γ → α → m β
hmono₁ : monotone f
hmono₂ : monotone g
x₁ x₂ : γ
hx₁₂ : x₁ ⊑ x₂
⊢ (fun x => f x >>= g x) x₁ ⊑ ?y

Tactic:
apply MonoBind.bind_mono_left (hmono₁ _ _ hx₁₂)

Result:
no goals

Proof state:
m : Type u → Type v
inst✝³ : Bind m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → m α
g : γ → α → m β
hmono₁ : monotone f
hmono₂ : monotone g
x₁ x₂ : γ
hx₁₂ : x₁ ⊑ x₂
⊢ (fun x => f x >>= g x) x₁ ⊑ (fun x => f x >>= g x) x₂

Tactic:
apply PartialOrder.rel_trans

Result:
case a
m : Type u → Type v
inst✝³ : Bind m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → m α
g : γ → α → m β
hmono₁ : monotone f
hmono₂ : monotone g
x₁ x₂ : γ
hx₁₂ : x₁ ⊑ x₂
⊢ (fun x => f x >>= g x) x₁ ⊑ ?y

case a
m : Type u → Type v
inst✝³ : Bind m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → m α
g : γ → α → m β
hmono₁ : monotone f
hmono₂ : monotone g
x₁ x₂ : γ
hx₁₂ : x₁ ⊑ x₂
⊢ ?y ⊑ (fun x => f x >>= g x) x₂

case y
m : Type u → Type v
inst✝³ : Bind m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → m α
g : γ → α → m β
hmono₁ : monotone f
hmono₂ : monotone g
x₁ x₂ : γ
hx₁₂ : x₁ ⊑ x₂
⊢ m β

Proof state:
case a
m : Type u → Type v
inst✝³ : Bind m
inst✝² : (α : Type u) → PartialOrder (m α)
inst✝¹ : MonoBind m
α β : Type u
γ : Type w
inst✝ : PartialOrder γ
f : γ → m α
g : γ → α → m β
hmono₁ : monotone f
hmono₂ : monotone g
x₁ x₂ : γ
hx₁₂ : x₁ ⊑ x₂
⊢ f x₂ >>= g x₁ ⊑ (fun x => f x >>= g x) x₂

Tactic:
apply MonoBind.bind_mono_right (fun y => monotone_apply y _ hmono₂ _ _ hx₁₂)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem Functor.map_unit [Monad m] [LawfulMonad m] {a : m PUnit} : (fun _ => PUnit.unit) <$> a = a

Proof state:
m : Type u_1 → Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : m PUnit
⊢ (fun x => PUnit.unit) <$> a = a

Tactic:
simp [map]

Result:
no goals
-- Mathlib/Data/Int/Order/Units.lean
theorem units_inv_eq_self (u : ℤˣ) : u⁻¹ = u

Proof state:
u : ℤˣ
⊢ u⁻¹ = u

Tactic:
rw [inv_eq_iff_mul_eq_one, units_mul_self]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma δ_comp_ofHom {n : ℤ} (z₁ : Cochain F G n) (f : G ⟶ K) (m : ℤ) :
    δ n m (z₁.comp (Cochain.ofHom f) (add_zero n)) =
      (δ n m z₁).comp (Cochain.ofHom f) (add_zero m)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n : ℤ
z₁ : Cochain F G n
f : G ⟶ K
m : ℤ
⊢ δ n m (z₁.comp (Cochain.ofHom f) ⋯) = (δ n m z₁).comp (Cochain.ofHom f) ⋯

Tactic:
rw [← Cocycle.ofHom_coe, δ_comp_zero_cocycle]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem SuperpolynomialDecay.add [ContinuousAdd β] (hf : SuperpolynomialDecay l k f)
    (hg : SuperpolynomialDecay l k g) : SuperpolynomialDecay l k (f + g) := fun z => by
  simpa only [mul_add, add_zero, Pi.add_apply] using (hf z).add (hg z)

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousAdd β
hf : SuperpolynomialDecay l k f
hg : SuperpolynomialDecay l k g
z : ℕ
⊢ Tendsto (fun a => k a ^ z * (f + g) a) l (𝓝 0)

Tactic:
simpa only [mul_add, add_zero, Pi.add_apply] using (hf z).add (hg z)

Result:
no goals
-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem powHalf_le_one (n : ℕ) : powHalf n ≤ 1

Proof state:
case zero

⊢ powHalf 0 ≤ 1

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case succ
n : ℕ
hn : powHalf n ≤ 1
⊢ powHalf (n + 1) ≤ 1

Tactic:
exact (powHalf_succ_le_powHalf n).trans hn

Result:
no goals

Proof state:
n : ℕ
⊢ powHalf n ≤ 1

Tactic:
induction n with
| zero => exact le_rfl
| succ n hn => exact (powHalf_succ_le_powHalf n).trans hn

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma Odd.sub_even (ha : Odd a) (hb : Even b) : Odd (a - b)

Proof state:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Even b
⊢ Odd (a + -b)

Tactic:
exact ha.add_even hb.neg

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Even b
⊢ Odd (a - b)

Tactic:
rw [sub_eq_add_neg]

Result:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Even b
⊢ Odd (a + -b)
-- Mathlib/Data/Matroid/Map.lean
lemma Indep.exists_bijOn_of_map {I : Set β} (hf) (hI : (M.map f hf).Indep I) :
    ∃ I₀, M.Indep I₀ ∧ BijOn f I₀ I

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I₀ : Set α
hI₀ : M.Indep I₀
⊢ ∃ I₀_1, M.Indep I₀_1 ∧ BijOn f I₀_1 (f '' I₀)

Tactic:
exact ⟨I₀, hI₀, (hf.mono hI₀.subset_ground).bijOn_image⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
I : Set β
hf : InjOn f M.E
hI : (M.map f hf).Indep I
⊢ ∃ I₀, M.Indep I₀ ∧ BijOn f I₀ I

Tactic:
obtain ⟨I₀, hI₀, rfl⟩ := hI

Result:
case intro.intro
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I₀ : Set α
hI₀ : M.Indep I₀
⊢ ∃ I₀_1, M.Indep I₀_1 ∧ BijOn f I₀_1 (f '' I₀)
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem basisSets_nonempty [Nonempty ι] : p.basisSets.Nonempty

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
⊢ p.basisSets.Nonempty

Tactic:
let i := Classical.arbitrary ι

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
i : ι := Classical.arbitrary ι
⊢ p.basisSets.Nonempty

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
i : ι := Classical.arbitrary ι
⊢ p.basisSets.Nonempty

Tactic:
refine nonempty_def.mpr ⟨(p i).ball 0 1, ?_⟩

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
i : ι := Classical.arbitrary ι
⊢ (p i).ball 0 1 ∈ p.basisSets

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
i : ι := Classical.arbitrary ι
⊢ (p i).ball 0 1 ∈ p.basisSets

Tactic:
exact p.basisSets_singleton_mem i zero_lt_one

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_eq_getElem?_get (l : List α) (i : Nat) (h : i < l.length) :
    l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h])

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.length
⊢ l[i] = l[i]?.get ⋯

Tactic:
simp [getElem_eq_iff]

Result:
no goals

Proof state:
α : Type ?u.16122
l : List α
i : Nat
h : i < l.length
⊢ l[i]?.isSome = true

Tactic:
simp [getElem?_eq_getElem, h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem average_add_measure [IsFiniteMeasure μ] {ν : Measure α} [IsFiniteMeasure ν] {f : α → E}
    (hμ : Integrable f μ) (hν : Integrable f ν) :
    ⨍ x, f x ∂(μ + ν) =
      ((μ univ).toReal / ((μ univ).toReal + (ν univ).toReal)) • ⨍ x, f x ∂μ +
        ((ν univ).toReal / ((μ univ).toReal + (ν univ).toReal)) • ⨍ x, f x ∂ν

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
ν : Measure α
inst✝ : IsFiniteMeasure ν
f : α → E
hμ : Integrable f μ
hν : Integrable f ν
⊢ ⨍ (x : α), f x ∂(μ + ν) =
    ((μ univ).toReal / ((μ univ).toReal + (ν univ).toReal)) • ⨍ (x : α), f x ∂μ +
      ((ν univ).toReal / ((μ univ).toReal + (ν univ).toReal)) • ⨍ (x : α), f x ∂ν

Tactic:
simp only [div_eq_inv_mul, mul_smul, measure_smul_average, ← smul_add,
  ← integral_add_measure hμ hν, ← ENNReal.toReal_add (measure_ne_top μ _) (measure_ne_top ν _)]

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
ν : Measure α
inst✝ : IsFiniteMeasure ν
f : α → E
hμ : Integrable f μ
hν : Integrable f ν
⊢ ⨍ (x : α), f x ∂(μ + ν) = (μ univ + ν univ).toReal⁻¹ • ∫ (x : α), f x ∂(μ + ν)

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
ν : Measure α
inst✝ : IsFiniteMeasure ν
f : α → E
hμ : Integrable f μ
hν : Integrable f ν
⊢ ⨍ (x : α), f x ∂(μ + ν) = (μ univ + ν univ).toReal⁻¹ • ∫ (x : α), f x ∂(μ + ν)

Tactic:
rw [average_eq, Measure.add_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_zero [Module.Free A M] :
    LinearMap.det (0 : M →ₗ[A] M) = (0 : A) ^ Module.finrank A M

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module.Free A M
⊢ LinearMap.det 0 = 0 ^ Module.finrank A M

Tactic:
simp only [← zero_smul A (1 : M →ₗ[A] M), det_smul, mul_one, MonoidHom.map_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem basis_ne_zero (hvs : Set.InjOn v s) (hi : i ∈ s) : Lagrange.basis s v i ≠ 0

Proof state:
case intro
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
hij : j ≠ i
hj : j ∈ s
⊢ ¬basisDivisor (v i) (v j) = 0

Tactic:
rw [basisDivisor_eq_zero_iff, hvs.eq_iff hi hj]

Result:
case intro
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
hij : j ≠ i
hj : j ∈ s
⊢ ¬i = j

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∀ (a : ι), a ≠ i ∧ a ∈ s → ¬basisDivisor (v i) (v a) = 0

Tactic:
rintro j ⟨hij, hj⟩

Result:
case intro
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
hij : j ≠ i
hj : j ∈ s
⊢ ¬basisDivisor (v i) (v j) = 0

Proof state:
case intro
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
hij : j ≠ i
hj : j ∈ s
⊢ ¬i = j

Tactic:
exact hij.symm

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ Lagrange.basis s v i ≠ 0

Tactic:
simp_rw [Lagrange.basis, prod_ne_zero_iff, Ne, mem_erase]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∀ (a : ι), a ≠ i ∧ a ∈ s → ¬basisDivisor (v i) (v a) = 0
-- Mathlib/Data/Set/Lattice.lean
lemma forall_sUnion {S : Set (Set α)} {p : α → Prop} :
    (∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x

Proof state:
α : Type u_1
S : Set (Set α)
p : α → Prop
⊢ (∀ x ∈ ⋃₀ S, p x) ↔ ∀ s ∈ S, ∀ x ∈ s, p x

Tactic:
simp_rw [← iInf_Prop_eq, iInf_sUnion]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean
theorem im_exp (q : ℍ[ℝ]) : (exp ℝ q).im = (exp ℝ q.re * (Real.sin ‖q.im‖ / ‖q.im‖)) • q.im

Proof state:
q : ℍ
⊢ (exp ℝ q).im = (exp ℝ q.re * (Real.sin ‖q.im‖ / ‖q.im‖)) • q.im

Tactic:
simp [exp_eq, smul_smul]

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem chain_singleton {a b : α} : Chain R a [b] ↔ R a b

Proof state:
α : Type u
R : α → α → Prop
a b : α
⊢ Chain R a [b] ↔ R a b

Tactic:
simp only [chain_cons, Chain.nil, and_true]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Induced.lean
@[simp]
lemma shiftFunctorZero_hom_app_obj_of_induced (X : C) :
    letI := HasShift.induced F A s i
    (shiftFunctorZero D A).hom.app (F.obj X) =
      (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)

Proof state:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_5, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
this : HasShift D A := HasShift.induced F A s i
⊢ (shiftFunctorZero D A).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)

Tactic:
simp only [ShiftMkCore.shiftFunctorZero_eq, HasShift.Induced.zero_hom_app_obj]

Result:
no goals

Proof state:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_5, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
⊢ (shiftFunctorZero D A).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)

Tactic:
letI := HasShift.induced F A s i

Result:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_5, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
X : C
this : HasShift D A := HasShift.induced F A s i
⊢ (shiftFunctorZero D A).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)
-- Mathlib/Data/Nat/Order/Lemmas.lean
theorem set_eq_univ {S : Set ℕ} : S = Set.univ ↔ 0 ∈ S ∧ ∀ k : ℕ, k ∈ S → k + 1 ∈ S :=
  ⟨by rintro rfl; simp, fun ⟨h0, hs⟩ => Set.eq_univ_of_forall (set_induction h0 hs)⟩

Proof state:
⊢ 0 ∈ Set.univ ∧ ∀ k ∈ Set.univ, k + 1 ∈ Set.univ

Tactic:
simp

Result:
no goals

Proof state:
S : Set ℕ
⊢ S = Set.univ → 0 ∈ S ∧ ∀ k ∈ S, k + 1 ∈ S

Tactic:
rintro rfl

Result:
⊢ 0 ∈ Set.univ ∧ ∀ k ∈ Set.univ, k + 1 ∈ Set.univ
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀' (μ : Measure α) [SFinite μ]
    {f : α → ℝ≥0∞} (s : Set α) (hf : AEMeasurable f (μ.restrict s)) (g : α → ℝ≥0∞)
    (h'f : ∀ᵐ x ∂μ.restrict s, f x < ∞) :
    ∫⁻ a in s, g a ∂μ.withDensity f = ∫⁻ a in s, (f * g) a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
g : α → ℝ≥0∞
h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
rw [restrict_withDensity' s, lintegral_withDensity_eq_lintegral_mul_non_measurable₀ _ hf h'f]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem torusIntegral_neg (f : ℂⁿ → E) (c : ℂⁿ) (R : ℝⁿ) :
    (∯ x in T(c, R), -f x) = -∯ x in T(c, R), f x

Proof state:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
⊢ (∯ (x : Fin n → ℂ) in T(c, R), -f x) = -∯ (x : Fin n → ℂ) in T(c, R), f x

Tactic:
simp [torusIntegral, integral_neg]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
lemma le_nnreal_iff [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {a : A}
    (ha : QuasispectrumRestricts a ContinuousMap.realToNNReal) {r : ℝ≥0} :
    (∀ x ∈ quasispectrum ℝ≥0 a, x ≤ r) ↔ ∀ x ∈ quasispectrum ℝ a, x ≤ r

Proof state:
A : Type u_3
inst✝³ : NonUnitalRing A
inst✝² : Module ℝ A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : SMulCommClass ℝ A A
a : A
ha : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
r : ℝ≥0
⊢ (∀ x ∈ σₙ ℝ≥0 a, x ≤ r) ↔ ∀ x ∈ σₙ ℝ a, x ≤ ↑r

Tactic:
simp [← ha.algebraMap_image]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem eventually_nhds' {x : X} (p : X → Prop) (hx : x ∈ e.source) :
    (∀ᶠ y in 𝓝 (e x), p (e.symm y)) ↔ ∀ᶠ x in 𝓝 x, p x

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
p : X → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (y : Y) in 𝓝 (↑e x), p (↑e.symm y)) ↔ ∀ᶠ (x : X) in 𝓝 x, p x

Tactic:
rw [e.eventually_nhds _ hx]

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
p : X → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (x : X) in 𝓝 x, p (↑e.symm (↑e x))) ↔ ∀ᶠ (x : X) in 𝓝 x, p x

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
p : X → Prop
hx : x ∈ e.source
y : X
hy : ↑e.symm (↑e y) = y
⊢ p (↑e.symm (↑e y)) ↔ p y

Tactic:
rw [hy]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
p : X → Prop
hx : x ∈ e.source
⊢ (∀ᶠ (x : X) in 𝓝 x, p (↑e.symm (↑e x))) ↔ ∀ᶠ (x : X) in 𝓝 x, p x

Tactic:
refine eventually_congr ((e.eventually_left_inverse hx).mono fun y hy => ?_)

Result:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
p : X → Prop
hx : x ∈ e.source
y : X
hy : ↑e.symm (↑e y) = y
⊢ p (↑e.symm (↑e y)) ↔ p y
-- Mathlib/SetTheory/Game/PGame.lean
theorem Subsequent.moveRight_mk_left {xR : xr → PGame} {i : xl} (xL : xl → PGame) (j) :
    Subsequent ((xL i).moveRight j) (mk xl xr xL xR)

Proof state:
xl xr : Type u
xR : xr → PGame
i : xl
xL : xl → PGame
j : (xL i).RightMoves
⊢ ((xL i).moveRight j).Subsequent (mk xl xr xL xR)

Tactic:
pgame_wf_tac

Result:
no goals
-- Mathlib/Combinatorics/Pigeonhole.lean
theorem exists_le_card_fiber_of_nsmul_le_card_of_maps_to (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Nonempty)
    (hb : #t • b ≤ #s) : ∃ y ∈ t, b ≤ #{x ∈ s | f x = y}

Proof state:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝ : LinearOrderedCommSemiring M
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : #t • b ≤ ↑(#s)
⊢ ∃ y ∈ t, b ≤ ↑(#(filter (fun x => f x = y) s))

Tactic:
simp_rw [cast_card] at hb ⊢

Result:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝ : LinearOrderedCommSemiring M
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : #t • b ≤ ∑ x ∈ s, 1
⊢ ∃ y ∈ t, b ≤ ∑ x ∈ filter (fun x => f x = y) s, 1

Proof state:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝ : LinearOrderedCommSemiring M
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : #t • b ≤ ∑ x ∈ s, 1
⊢ ∃ y ∈ t, b ≤ ∑ x ∈ filter (fun x => f x = y) s, 1

Tactic:
exact exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum hf ht hb

Result:
no goals