harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem HasFTaylorSeriesUpToOn.congr (h : HasFTaylorSeriesUpToOn n f p s)
    (h₁ : ∀ x ∈ s, f₁ x = f x) : HasFTaylorSeriesUpToOn n f₁ p s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
h₁ : ∀ x ∈ s, f₁ x = f x
x : E
hx : x ∈ s
⊢ (p x 0).curry0 = f x

Tactic:
exact h.zero_eq x hx

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
h₁ : ∀ x ∈ s, f₁ x = f x
x : E
hx : x ∈ s
⊢ (p x 0).curry0 = f₁ x

Tactic:
rw [h₁ x hx]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
h₁ : ∀ x ∈ s, f₁ x = f x
x : E
hx : x ∈ s
⊢ (p x 0).curry0 = f x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
h₁ : ∀ x ∈ s, f₁ x = f x
⊢ HasFTaylorSeriesUpToOn n f₁ p s

Tactic:
refine ⟨fun x hx => ?_, h.fderivWithin, h.cont⟩

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
h : HasFTaylorSeriesUpToOn n f p s
h₁ : ∀ x ∈ s, f₁ x = f x
x : E
hx : x ∈ s
⊢ (p x 0).curry0 = f₁ x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem infix_concat_iff {l₁ l₂ : List α} {a : α} :
    l₁ <:+: l₂ ++ [a] ↔ l₁ <:+ l₂ ++ [a] ∨ l₁ <:+: l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
a : α
⊢ l₁ <:+: l₂ ++ [a] ↔ l₁ <:+ l₂ ++ [a] ∨ l₁ <:+: l₂

Tactic:
rw [← reverse_infix, reverse_concat, infix_cons_iff, reverse_infix,
  ← reverse_prefix, reverse_concat]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem le_order {n : ℕ∞} (h : ∀ d : σ →₀ ℕ, degree d < n → coeff R d f = 0) :
    n ≤ f.order

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ∞
h : ∀ (d : σ →₀ ℕ), ↑d.degree < n → (coeff R d) f = 0
⊢ n ≤ f.order

Tactic:
simp_rw [degree_eq_weight_one] at h

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ∞
h : ∀ (d : σ →₀ ℕ), ↑((weight fun x => 1) d) < n → (coeff R d) f = 0
⊢ n ≤ f.order

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ∞
h : ∀ (d : σ →₀ ℕ), ↑((weight fun x => 1) d) < n → (coeff R d) f = 0
⊢ n ≤ f.order

Tactic:
exact le_weightedOrder _ h

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem eq_left_iff {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s)
    {a b c : α} (ha : a ∈ s) (hb : b ∈ s) (hc : c ∈ s) :
    variationOnFromTo f s a b = variationOnFromTo f s a c ↔ variationOnFromTo f s b c = 0

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ variationOnFromTo f s a b = variationOnFromTo f s a c ↔ variationOnFromTo f s b c = 0

Tactic:
simp only [← variationOnFromTo.add hf ha hb hc, self_eq_add_right]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem range_succ_eq_Icc_zero (n : ℕ) : range (n + 1) = Icc 0 n

Proof state:
n : ℕ
⊢ range (n + 1) = Icc 0 n

Tactic:
rw [range_eq_Icc_zero_sub_one _ (Nat.add_one_ne_zero _), Nat.add_sub_cancel_right]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_transpose (M : Matrix n n R) : Mᵀ.det = M.det

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, Mᵀ (σ i) i = ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, M (σ i) i

Tactic:
refine Fintype.sum_bijective _ inv_involutive.bijective _ _ ?_

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∀ (x : Perm n), ↑↑(sign x) * ∏ i : n, Mᵀ (x i) i = ↑↑(sign x⁻¹) * ∏ i : n, M (x⁻¹ i) i

Proof state:
case e_a
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ∏ i : n, Mᵀ (σ i) i = ∏ i : n, M (σ⁻¹ i) i

Tactic:
apply Fintype.prod_equiv σ

Result:
case e_a.h
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ∀ (x : n), Mᵀ (σ x) x = M (σ⁻¹ (σ x)) (σ x)

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ↑↑(sign σ) * ∏ i : n, Mᵀ (σ i) i = ↑↑(sign σ) * ∏ i : n, M (σ⁻¹ i) i

Tactic:
congr 1

Result:
case e_a
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ∏ i : n, Mᵀ (σ i) i = ∏ i : n, M (σ⁻¹ i) i

Proof state:
case e_a.h
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ∀ (x : n), Mᵀ (σ x) x = M (σ⁻¹ (σ x)) (σ x)

Tactic:
simp

Result:
no goals

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ↑↑(sign σ) * ∏ i : n, Mᵀ (σ i) i = ↑↑(sign σ⁻¹) * ∏ i : n, M (σ⁻¹ i) i

Tactic:
rw [sign_inv]

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ↑↑(sign σ) * ∏ i : n, Mᵀ (σ i) i = ↑↑(sign σ) * ∏ i : n, M (σ⁻¹ i) i

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∀ (x : Perm n), ↑↑(sign x) * ∏ i : n, Mᵀ (x i) i = ↑↑(sign x⁻¹) * ∏ i : n, M (x⁻¹ i) i

Tactic:
intro σ

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ↑↑(sign σ) * ∏ i : n, Mᵀ (σ i) i = ↑↑(sign σ⁻¹) * ∏ i : n, M (σ⁻¹ i) i

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ Mᵀ.det = M.det

Tactic:
rw [det_apply', det_apply']

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, Mᵀ (σ i) i = ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, M (σ i) i
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem toComplex_inj {x y : ℤ[i]} : (x : ℂ) = y ↔ x = y

Proof state:
case mk.mk
re✝¹ im✝¹ re✝ im✝ : ℤ
⊢ toComplex { re := re✝¹, im := im✝¹ } = toComplex { re := re✝, im := im✝ } ↔
    { re := re✝¹, im := im✝¹ } = { re := re✝, im := im✝ }

Tactic:
simp [toComplex_def₂]

Result:
no goals

Proof state:
case mk
y : ℤ[i]
re✝ im✝ : ℤ
⊢ toComplex { re := re✝, im := im✝ } = toComplex y ↔ { re := re✝, im := im✝ } = y

Tactic:
cases y

Result:
case mk.mk
re✝¹ im✝¹ re✝ im✝ : ℤ
⊢ toComplex { re := re✝¹, im := im✝¹ } = toComplex { re := re✝, im := im✝ } ↔
    { re := re✝¹, im := im✝¹ } = { re := re✝, im := im✝ }

Proof state:
x y : ℤ[i]
⊢ toComplex x = toComplex y ↔ x = y

Tactic:
cases x

Result:
case mk
y : ℤ[i]
re✝ im✝ : ℤ
⊢ toComplex { re := re✝, im := im✝ } = toComplex y ↔ { re := re✝, im := im✝ } = y
-- Mathlib/Data/DFinsupp/Defs.lean
theorem mk_sub [∀ i, AddGroup (β i)] {s : Finset ι} {x y : ∀ i : (↑s : Set ι), β i.1} :
    mk s (x - y) = mk s x - mk s y :=
  ext fun i => by simp only [sub_apply, mk_apply]; split_ifs <;> [rfl; rw [sub_zero]]

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (x - y) ⟨i, H⟩ else 0) = (if H : i ∈ s then x ⟨i, H⟩ else 0) - if H : i ∈ s then y ⟨i, H⟩ else 0

Tactic:
split_ifs <;> [rfl; rw [sub_zero]]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
⊢ (mk s (x - y)) i = (mk s x - mk s y) i

Tactic:
simp only [sub_apply, mk_apply]

Result:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x y : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (x - y) ⟨i, H⟩ else 0) = (if H : i ∈ s then x ⟨i, H⟩ else 0) - if H : i ∈ s then y ⟨i, H⟩ else 0
-- Mathlib/Data/Real/EReal.lean
theorem addLECancellable_coe (x : ℝ) : AddLECancellable (x : EReal)
  | _, ⊤, _ => le_top
  | ⊥, _, _ => bot_le
  | ⊤, (z : ℝ), h => by simp only [coe_add_top, ← coe_add, top_le_iff, coe_ne_top] at h
  | _, ⊥, h => by simpa using h
  | (y : ℝ), (z : ℝ), h => by
    simpa only [← coe_add, EReal.coe_le_coe_iff, add_le_add_iff_left] using h

Proof state:
x : ℝ
x✝ : EReal
h : ↑x + x✝ ≤ ↑x + ⊥
⊢ x✝ ≤ ⊥

Tactic:
simpa using h

Result:
no goals

Proof state:
x y z : ℝ
h : ↑x + ↑y ≤ ↑x + ↑z
⊢ ↑y ≤ ↑z

Tactic:
simpa only [← coe_add, EReal.coe_le_coe_iff, add_le_add_iff_left] using h

Result:
no goals

Proof state:
x z : ℝ
h : ↑x + ⊤ ≤ ↑x + ↑z
⊢ ⊤ ≤ ↑z

Tactic:
simp only [coe_add_top, ← coe_add, top_le_iff, coe_ne_top] at h

Result:
no goals
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem IsTransitive.sUnion (h : x.IsTransitive) :
    (⋃₀ x : ZFSet).IsTransitive := fun y hy z hz => by
  rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩
  exact mem_sUnion_of_mem hz (h.mem_trans hw' hw)

Proof state:
case intro.intro
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
w : ZFSet.{u}
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x

Tactic:
exact mem_sUnion_of_mem hz (h.mem_trans hw' hw)

Result:
no goals

Proof state:
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ ⋃₀ x

Tactic:
rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩

Result:
case intro.intro
x : ZFSet.{u}
h : x.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
w : ZFSet.{u}
hw : w ∈ x
hw' : y ∈ w
⊢ z ∈ ⋃₀ x
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem toPermHom_apply_toCentralizer :
    (toPermHom g) (toCentralizer a τ) = (τ : Perm g.cycleFactorsFinset)

Proof state:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ ∀ (x : { x // x ∈ g.cycleFactorsFinset }), ((OnCycleFactors.toPermHom g) (a.toCentralizer τ)) x = ↑τ x

Tactic:
intro c

Result:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : { x // x ∈ g.cycleFactorsFinset }
⊢ ((OnCycleFactors.toPermHom g) (a.toCentralizer τ)) c = ↑τ c

Proof state:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : { x // x ∈ g.cycleFactorsFinset }
⊢ ((OnCycleFactors.toPermHom g) (a.toCentralizer τ)) c = ↑τ c

Tactic:
rw [OnCycleFactors.toPermHom_apply, toCentralizer_equivariant]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ (OnCycleFactors.toPermHom g) (a.toCentralizer τ) = ↑τ

Tactic:
apply ext

Result:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ ∀ (x : { x // x ∈ g.cycleFactorsFinset }), ((OnCycleFactors.toPermHom g) (a.toCentralizer τ)) x = ↑τ x
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem mem_closedBall_one_iff : a ∈ closedBall (1 : E) r ↔ ‖a‖ ≤ r

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ
⊢ a ∈ closedBall 1 r ↔ ‖a‖ ≤ r

Tactic:
rw [mem_closedBall, dist_one_right]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem continuous_lift₂ {f : X → Y → Z} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d} :
    Continuous (uncurry <| lift₂ f hf) ↔ Continuous (uncurry f)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
⊢ Continuous (uncurry (lift₂ f hf)) ↔ Continuous (uncurry f)

Tactic:
simp only [continuous_iff_continuousOn_univ, continuousOn_lift₂, preimage_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_alter {k k' fallback : α} (h : m.1.WF) {f : Option β → Option β} :
    (Const.alter m k f).getKeyD k' fallback =
      if k == k' then
        if (f (Const.get? m k)).isSome then k else fallback
      else
        m.getKeyD k' fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
k k' fallback : α
h : m.val.WF
f : Option β → Option β
⊢ (alter m k f).getKeyD k' fallback =
    if (k == k') = true then if (f (get? m k)).isSome = true then k else fallback else m.getKeyD k' fallback

Tactic:
simp_to_model [Const.alter] using List.Const.getKeyD_alterKey

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
/-- Binary **rearrangement inequality**. -/
lemma mul_add_mul_le_mul_add_mul' [ExistsAddOfLE α] [MulPosMono α]
    [AddLeftMono α] [AddLeftReflectLE α]
    (hba : b ≤ a) (hdc : d ≤ c) : a * d + b * c ≤ a * c + b * d

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c d : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
hba : b ≤ a
hdc : d ≤ c
⊢ a * d + b * c ≤ a * c + b * d

Tactic:
rw [add_comm (a * d), add_comm (a * c)]

Result:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c d : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
hba : b ≤ a
hdc : d ≤ c
⊢ b * c + a * d ≤ b * d + a * c

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b c d : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddLeftMono α
inst✝ : AddLeftReflectLE α
hba : b ≤ a
hdc : d ≤ c
⊢ b * c + a * d ≤ b * d + a * c

Tactic:
exact mul_add_mul_le_mul_add_mul hba hdc

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_mul_I : sinh (x * I) = sin x * I

Proof state:
x : ℂ
⊢ sinh (x * I) = sin x * I

Tactic:
rw [← mul_right_inj' (two_ne_zero' ℂ), two_sinh, ← mul_assoc, two_sin, mul_assoc, I_mul_I,
  mul_neg_one, neg_sub, neg_mul_eq_neg_mul]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Prod.lean
theorem sup'_product_left {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
    (s ×ˢ t).sup' h f = s.sup' h.fst fun i => t.sup' h.snd fun i' => f ⟨i, i'⟩ :=
  eq_of_forall_ge_iff fun a => by simp [@forall_swap _ γ]

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SemilatticeSup α
s : Finset β
t : Finset γ
h : (s ×ˢ t).Nonempty
f : β × γ → α
a : α
⊢ (s ×ˢ t).sup' h f ≤ a ↔ (s.sup' ⋯ fun i => t.sup' ⋯ fun i' => f (i, i')) ≤ a

Tactic:
simp [@forall_swap _ γ]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem norm_div_cos_angle_sub_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0 ∨ y = 0) :
    ‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ -y = 0
⊢ ‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖

Tactic:
rw [sub_eq_add_neg, norm_div_cos_angle_add_of_inner_eq_zero h h0]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y = 0
⊢ ‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ y = 0
⊢ ‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ y = 0
⊢ ‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖

Tactic:
rw [← neg_eq_zero] at h0

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ -y = 0
⊢ ‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The `LSeries` of the arithmetic function `ζ` is the same as the `LSeries` associated
to the constant sequence `1`. -/
lemma LSeries_zeta_eq : L ↗ζ = L 1

Proof state:
⊢ (L fun n => ↑(ζ n)) = L 1

Tactic:
ext s

Result:
case h
s : ℂ
⊢ L (fun n => ↑(ζ n)) s = L 1 s

Proof state:
case h
s : ℂ
⊢ L (fun n => ↑(ζ n)) s = L 1 s

Tactic:
exact (LSeries_congr s const_one_eq_zeta).symm

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_le_iff (f g : R → R) (a : A) (hf : ContinuousOn f (σₙ R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommRing R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalRing R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type ?u.1076395) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f g : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfcₙ f a ≤ cfcₙ g a ↔ ∀ x ∈ σₙ R a, f x ≤ g x

Tactic:
rw [cfcₙ_apply f a, cfcₙ_apply g a, cfcₙHom_le_iff (show p a from ha), ContinuousMapZero.le_def]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommRing R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalRing R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f g : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ (∀ (x : ↑(σₙ R a)),
      { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } x ≤
        { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ } x) ↔
    ∀ x ∈ σₙ R a, f x ≤ g x

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommRing R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalRing R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type u_1) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f g : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ (∀ (x : ↑(σₙ R a)),
      { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } x ≤
        { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ } x) ↔
    ∀ x ∈ σₙ R a, f x ≤ g x

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem eq_zero_iff {P Q : C} (f : P ⟶ Q) : f = 0 ↔ ∀ a, f a = 0 :=
  ⟨fun h a => by simp [h], zero_morphism_ext _⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : f = 0
a : Pseudoelement P
⊢ pseudoApply f a = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
lemma collapse_of_mem (ha : a ∉ s) (ht : t ∈ 𝒜) (hu : u ∈ 𝒜) (hts : t = s)
    (hus : u = insert a s) : collapse 𝒜 a f s = f t + f u

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t u : Finset α
ha : a ∉ s
ht : t ∈ 𝒜
hu : u ∈ 𝒜
hts : t = s
hus : u = insert a s
⊢ collapse 𝒜 a f s = f t + f u

Tactic:
subst hts

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t u : Finset α
ht : t ∈ 𝒜
hu : u ∈ 𝒜
ha : a ∉ t
hus : u = insert a t
⊢ collapse 𝒜 a f t = f t + f u

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
ht : t ∈ 𝒜
ha : a ∉ t
hu : insert a t ∈ 𝒜
⊢ collapse 𝒜 a f t = f t + f (insert a t)

Tactic:
simp_rw [collapse_eq ha, if_pos ht, if_pos hu]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t u : Finset α
ht : t ∈ 𝒜
hu : u ∈ 𝒜
ha : a ∉ t
hus : u = insert a t
⊢ collapse 𝒜 a f t = f t + f u

Tactic:
subst hus

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : LinearOrderedCommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
ht : t ∈ 𝒜
ha : a ∉ t
hu : insert a t ∈ 𝒜
⊢ collapse 𝒜 a f t = f t + f (insert a t)
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_abs_sub_abs_le_abs_sub (a b : α) : |(|a| - |b|)| ≤ |a - b| :=
  abs_sub_le_iff.2
    ⟨abs_sub_abs_le_abs_sub _ _, by rw [abs_sub_comm]; apply abs_sub_abs_le_abs_sub⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ |b| - |a| ≤ |a - b|

Tactic:
rw [abs_sub_comm]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ |b| - |a| ≤ |b - a|

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ |b| - |a| ≤ |b - a|

Tactic:
apply abs_sub_abs_le_abs_sub

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem mem_nhdsWithin_iff_eventuallyEq {s t : Set α} {x : α} :
    t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] (s ∩ t : Set α)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
x : α
⊢ t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] s ∩ t

Tactic:
simp_rw [mem_nhdsWithin_iff_eventually, eventuallyEq_set, mem_inter_iff, iff_self_and]

Result:
no goals