harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/ContinuousMap/Units.lean
theorem isUnit_iff_forall_ne_zero (f : C(X, R)) : IsUnit f ↔ ∀ x, f x ≠ 0

Proof state:
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedDivisionRing R
inst✝ : CompleteSpace R
f : C(X, R)
⊢ IsUnit f ↔ ∀ (x : X), f x ≠ 0

Tactic:
simp_rw [f.isUnit_iff_forall_isUnit, isUnit_iff_ne_zero]

Result:
no goals
-- Mathlib/Algebra/Ring/Basic.lean
lemma inv_neg : (-a)⁻¹ = -a⁻¹

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a : R
⊢ (-a)⁻¹ = -a⁻¹

Tactic:
rw [neg_inv]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem measure_le_inter_add_diff (μ : F) (s t : Set α) : μ s ≤ μ (s ∩ t) + μ (s \ t)

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ μ s ≤ μ (s ∩ t) + μ (s \ t)

Tactic:
simpa using measure_union_le (s ∩ t) (s \ t)

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_lt_pow_iff_norm_le_pow_sub_one (x : ℤ_[p]) (n : ℤ) :
    ‖x‖ < (p : ℝ) ^ n ↔ ‖x‖ ≤ (p : ℝ) ^ (n - 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℤ
⊢ ‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)

Tactic:
rw [norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem fderiv_continuousMultilinear_apply_const_apply (hc : DifferentiableAt 𝕜 c x)
    (u : ∀ i, M i) (m : E) :
    (fderiv 𝕜 (fun y ↦ (c y) u) x) m = (fderiv 𝕜 c x) m u

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
x : E
ι : Type u_5
inst✝⁴ : Fintype ι
M : ι → Type u_6
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
H : Type u_7
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → ContinuousMultilinearMap 𝕜 M H
hc : DifferentiableAt 𝕜 c x
u : (i : ι) → M i
m : E
⊢ (fderiv 𝕜 (fun y => (c y) u) x) m = ((fderiv 𝕜 c x) m) u

Tactic:
simp [fderiv_continuousMultilinear_apply_const hc]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem pow_lt_one_of_lt {a : M} {n : ℕ} (h : a < 1) (hn : n ≠ 0) : a ^ n < 1

Proof state:
case intro
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
h : a < 1
k : ℕ
hn : k.succ ≠ 0
⊢ a * a ^ k < 1

Tactic:
exact mul_lt_one_of_lt_of_le h (pow_le_one_of_le h.le _)

Result:
no goals

Proof state:
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
n : ℕ
h : a < 1
hn : n ≠ 0
⊢ a ^ n < 1

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨k, rfl⟩

Result:
case intro
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
h : a < 1
k : ℕ
hn : k.succ ≠ 0
⊢ a ^ k.succ < 1

Proof state:
case intro
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
h : a < 1
k : ℕ
hn : k.succ ≠ 0
⊢ a ^ k.succ < 1

Tactic:
rw [pow_succ']

Result:
case intro
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
h : a < 1
k : ℕ
hn : k.succ ≠ 0
⊢ a * a ^ k < 1
-- Mathlib/Data/Finset/Filter.lean
theorem filter_False {h} (s : Finset α) : @filter _ (fun _ => False) h s = ∅

Proof state:
case h
α : Type u_1
h : DecidablePred fun x => False
s : Finset α
a✝ : α
⊢ a✝ ∈ filter (fun x => False) s ↔ a✝ ∈ ∅

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
h : DecidablePred fun x => False
s : Finset α
⊢ filter (fun x => False) s = ∅

Tactic:
ext

Result:
case h
α : Type u_1
h : DecidablePred fun x => False
s : Finset α
a✝ : α
⊢ a✝ ∈ filter (fun x => False) s ↔ a✝ ∈ ∅
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem modifyHead_nil (f : α → α) : [].modifyHead f = []

Proof state:
α : Type u
f : α → α
⊢ modifyHead f nil = nil

Tactic:
rw [modifyHead]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem map_pow (n : ℕ) :
    spectrum ℂ (a ^ n) = (· ^ n) '' spectrum ℂ a

Proof state:
A : Type u_2
inst✝³ : NormedRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
inst✝ : Nontrivial A
a : A
n : ℕ
⊢ spectrum ℂ (a ^ n) = (fun x => x ^ n) '' spectrum ℂ a

Tactic:
simpa only [aeval_X_pow, eval_pow, eval_X] using map_polynomial_aeval a (X ^ n)

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
theorem shift_shiftFunctorCompIsoId_add_neg_cancel_inv_app (n : A) (X : C) :
    ((shiftFunctorCompIsoId C n (-n) (add_neg_cancel n)).inv.app X)⟦n⟧' =
    (shiftFunctorCompIsoId C (-n) n (neg_add_cancel n)).inv.app (X⟦n⟧)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n : A
X : C
⊢ (shiftFunctor C n).map ((shiftFunctorCompIsoId C n (-n) ⋯).inv.app X) =
    (shiftFunctorCompIsoId C (-n) n ⋯).inv.app ((shiftFunctor C n).obj X)

Tactic:
apply shift_shiftFunctorCompIsoId_inv_app

Result:
no goals
-- Mathlib/Algebra/Module/BigOperators.lean
lemma Finset.sum_smul_sum (s : Finset α) (t : Finset β) {f : α → R} {g : β → M} :
    (∑ i ∈ s, f i) • ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i • g j

Proof state:
α : Type u_3
β : Type u_4
R : Type u_5
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
t : Finset β
f : α → R
g : β → M
⊢ (∑ i ∈ s, f i) • ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i • g j

Tactic:
simp_rw [sum_smul, ← smul_sum]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem tensor_hom_inv_id {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
    (g ⊗ f.hom) ≫ (h ⊗ f.inv) = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ (g ⊗ f.hom) ≫ (h ⊗ f.inv) = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V)

Tactic:
rw [← tensor_comp, f.hom_inv_id]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ g ≫ h ⊗ 𝟙 V = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ g ≫ h ⊗ 𝟙 V = (g ⊗ 𝟙 V) ≫ (h ⊗ 𝟙 V)

Tactic:
simp [tensorHom_id]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem withTopEquiv_zero : withTopEquiv 0 = 0

Proof state:
⊢ withTopEquiv 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem tail_zip_snd {l : List (α × β)} : l.unzip.2.tail = l.tail.unzip.2

Proof state:
α : Type u_1
β : Type u_2
l : List (α × β)
⊢ l.unzip.snd.tail = l.tail.unzip.snd

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
theorem IsFormalAdjoint.le_adjoint (h : T.IsFormalAdjoint S) : S ≤ T† :=
  ⟨-- Trivially, every `x : S.domain` is in `T.adjoint.domain`
  fun x hx =>
    mem_adjoint_domain_of_exists _
      ⟨S ⟨x, hx⟩, h.symm ⟨x, hx⟩⟩,-- Equality on `S.domain` follows from equality
  -- `⟪v, S x⟫ = ⟪v, T.adjoint y⟫` for all `v : T.domain`:
  fun _ _ hxy => (adjoint_apply_eq hT _ fun _ => by rw [h.symm, hxy]).symm⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
h : T.IsFormalAdjoint S
x✝² : ↥S.domain
x✝¹ : ↥T†.domain
hxy : ↑x✝² = ↑x✝¹
x✝ : ↥T.domain
⊢ inner (↑S x✝²) ↑x✝ = inner (↑x✝¹) (↑T x✝)

Tactic:
rw [h.symm, hxy]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem mul_T_assoc (f : R[T;T⁻¹]) (m n : ℤ) : f * T m * T n = f * T (m + n)

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
m n : ℤ
⊢ f * T m * T n = f * T (m + n)

Tactic:
simp [← T_add, mul_assoc]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem has_pointwise_sum_fourier_series_of_summable (h : Summable (fourierCoeff f))
    (x : AddCircle T) : HasSum (fun i => fourierCoeff f i • fourier i x) (f x)

Proof state:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
h : Summable (fourierCoeff ⇑f)
x : AddCircle T
⊢ HasSum (fun i => fourierCoeff (⇑f) i • (fourier i) x) (f x)

Tactic:
convert (ContinuousMap.evalCLM ℂ x).hasSum (hasSum_fourier_series_of_summable h)

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
lemma isLocallyConstant_rankAtStalk [Module.FinitePresentation R M] [Module.Flat R M] :
    IsLocallyConstant (rankAtStalk (R := R) M)

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FinitePresentation R M
inst✝ : Flat R M
e : ↑(freeLocus R M) ≃ₜ PrimeSpectrum R := (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.univ (PrimeSpectrum R))
⊢ IsLocallyConstant (rankAtStalk M)

Tactic:
convert isLocallyConstant_rankAtStalk_freeLocus.comp_continuous e.symm.continuous

Result:
no goals

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FinitePresentation R M
inst✝ : Flat R M
⊢ IsLocallyConstant (rankAtStalk M)

Tactic:
let e : freeLocus R M ≃ₜ PrimeSpectrum R :=
  (Homeomorph.setCongr freeLocus_eq_univ).trans (Homeomorph.Set.univ (PrimeSpectrum R))

Result:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : FinitePresentation R M
inst✝ : Flat R M
e : ↑(freeLocus R M) ≃ₜ PrimeSpectrum R := (Homeomorph.setCongr ⋯).trans (Homeomorph.Set.univ (PrimeSpectrum R))
⊢ IsLocallyConstant (rankAtStalk M)
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem zeroLocus_span (s : Set A) : zeroLocus 𝒜 (Ideal.span s) = zeroLocus 𝒜 s

Proof state:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s : Set A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ zeroLocus 𝒜 ↑(Ideal.span s) ↔ x ∈ zeroLocus 𝒜 s

Tactic:
exact (Submodule.gi _ _).gc s x.asHomogeneousIdeal.toIdeal

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s : Set A
⊢ zeroLocus 𝒜 ↑(Ideal.span s) = zeroLocus 𝒜 s

Tactic:
ext x

Result:
case h
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
s : Set A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ zeroLocus 𝒜 ↑(Ideal.span s) ↔ x ∈ zeroLocus 𝒜 s
-- Mathlib/Order/CompleteLattice/Finset.lean
theorem minimal_iff_forall_diff_singleton (hP : ∀ ⦃s t⦄, P t → t ⊆ s → P s) :
    Minimal P s ↔ P s ∧ ∀ x ∈ s, ¬ P (s.erase x) where
  mp h := ⟨h.prop, fun x hxs hx ↦ by simpa using h.le_of_le hx (erase_subset _ _) hxs⟩
  mpr h := ⟨h.1, fun t ht hts x hxs ↦ by_contra fun hxt ↦
    h.2 x hxs <| hP ht (subset_erase.2 ⟨hts, hxt⟩)⟩

Proof state:
α : Type u_2
inst✝ : DecidableEq α
P : Finset α → Prop
s : Finset α
hP : ∀ ⦃s t : Finset α⦄, P t → t ⊆ s → P s
h : Minimal P s
x : α
hxs : x ∈ s
hx : P (s.erase x)
⊢ False

Tactic:
simpa using h.le_of_le hx (erase_subset _ _) hxs

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_union (s t : Set X) : dimH (s ∪ t) = max (dimH s) (dimH t)

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
s t : Set X
⊢ dimH (s ∪ t) = dimH s ⊔ dimH t

Tactic:
rw [union_eq_iUnion, dimH_iUnion, iSup_bool_eq, cond, cond]

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

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

Tactic:
rw [← pow_mod_period_smul, Nat.add_mod_left, pow_mod_period_smul]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_eq_tprod_of_ne_one_bij {g : γ → α} (i : mulSupport g → β) (hi : Injective i)
    (hf : mulSupport f ⊆ Set.range i) (hfg : ∀ x, f (i x) = g x) : ∏' x, f x = ∏' y, g y

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
g : γ → α
i : ↑(mulSupport g) → β
hi : Injective i
hf : mulSupport f ⊆ Set.range i
hfg : ∀ (x : ↑(mulSupport g)), f (i x) = g ↑x
⊢ ∏' (x : β), f x = ∏' (y : γ), g y

Tactic:
rw [← tprod_subtype_mulSupport g, ← hi.tprod_eq hf]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
g : γ → α
i : ↑(mulSupport g) → β
hi : Injective i
hf : mulSupport f ⊆ Set.range i
hfg : ∀ (x : ↑(mulSupport g)), f (i x) = g ↑x
⊢ ∏' (c : ↑(mulSupport g)), f (i c) = ∏' (x : ↑(mulSupport g)), g ↑x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
g : γ → α
i : ↑(mulSupport g) → β
hi : Injective i
hf : mulSupport f ⊆ Set.range i
hfg : ∀ (x : ↑(mulSupport g)), f (i x) = g ↑x
⊢ ∏' (c : ↑(mulSupport g)), f (i c) = ∏' (x : ↑(mulSupport g)), g ↑x

Tactic:
simp only [hfg]

Result:
no goals
-- Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
theorem MultilinearMap.domCoprod_alternization_eq [DecidableEq ιa] [DecidableEq ιb]
    (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) :
    MultilinearMap.alternatization
      (MultilinearMap.domCoprod a b : MultilinearMap R' (fun _ : ιa ⊕ ιb => Mᵢ) (N₁ ⊗ N₂)) =
      ((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b

Proof state:
ιa : Type u_1
ιb : Type u_2
inst✝¹⁰ : Fintype ιa
inst✝⁹ : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R' N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R' N₂
inst✝³ : AddCommMonoid Mᵢ
inst✝² : Module R' Mᵢ
inst✝¹ : DecidableEq ιa
inst✝ : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
⊢ alternatization ((↑a).domCoprod ↑b) = ((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b

Tactic:
rw [MultilinearMap.domCoprod_alternization, coe_alternatization, coe_alternatization, mul_smul,
  ← AlternatingMap.domCoprod'_apply, ← AlternatingMap.domCoprod'_apply,
  ← TensorProduct.smul_tmul', TensorProduct.tmul_smul,
  LinearMap.map_smul_of_tower AlternatingMap.domCoprod',
  LinearMap.map_smul_of_tower AlternatingMap.domCoprod']

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_nadd_lt₃ {a' b' c' : Ordinal} (ha : a' < a) (hb : b' < b) (hc : c' < c) :
    a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' <
      a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'

Proof state:
a b c a' b' c' : Ordinal.{u}
ha : a' < a
hb : b' < b
hc : c' < c
⊢ a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'

Tactic:
simpa only [nadd_nmul, ← nadd_assoc] using nmul_nadd_lt (nmul_nadd_lt ha hb) hc

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma exists_eq_graphOn [Nonempty β] {s : Set (α × β)} :
    (∃ f t, s = graphOn f t) ↔ InjOn Prod.fst s :=
  .trans ⟨fun ⟨f, t, hs⟩ ↦ ⟨f, by rw [hs, image_fst_graphOn]⟩, fun ⟨f, hf⟩ ↦ ⟨f, _, hf⟩⟩
    exists_eq_graphOn_image_fst

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
s : Set (α × β)
x✝ : ∃ f t, s = graphOn f t
f : α → β
t : Set α
hs : s = graphOn f t
⊢ s = graphOn f (Prod.fst '' s)

Tactic:
rw [hs, image_fst_graphOn]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem cauchySeq_of_edist_le_of_tsum_ne_top {f : ℕ → α} (d : ℕ → ℝ≥0∞)
    (hf : ∀ n, edist (f n) (f n.succ) ≤ d n) (hd : tsum d ≠ ∞) : CauchySeq f

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
hd : tsum d ≠ ⊤
⊢ CauchySeq f

Tactic:
lift d to ℕ → NNReal using fun i => ENNReal.ne_top_of_tsum_ne_top hd i

Result:
case intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n
hd : ∑' (i : ℕ), ↑(d i) ≠ ⊤
⊢ CauchySeq f

Proof state:
case intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n
hd : ∑' (i : ℕ), ↑(d i) ≠ ⊤
⊢ CauchySeq f

Tactic:
rw [ENNReal.tsum_coe_ne_top_iff_summable] at hd

Result:
case intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n
hd : Summable d
⊢ CauchySeq f

Proof state:
case intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (fun i => ↑(d i)) n
hd : Summable d
⊢ CauchySeq f

Tactic:
exact cauchySeq_of_edist_le_of_summable d hf hd

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

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

Tactic:
simp only [torusIntegral, Fin.prod_univ_zero, one_smul,
  Subsingleton.elim (fun _ : Fin 0 => 2 * π) 0, Icc_self, Measure.restrict_singleton, volume_pi,
  integral_smul_measure, integral_dirac, Measure.pi_of_empty (fun _ : Fin 0 ↦ volume) 0,
  Measure.dirac_apply_of_mem (mem_singleton _), Subsingleton.elim (torusMap c R 0) c]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
    (m.insert k v).getKey? k = some k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
v : β k
⊢ (m.insert k v).getKey? k = some k

Tactic:
simp_to_model [insert] using List.getKey?_insertEntry_self

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem comp_eq_sum_left : p.comp q = p.sum fun e a => C a * q ^ e

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.comp q = p.sum fun e a => C a * q ^ e

Tactic:
rw [comp, eval₂_eq_sum]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem getD_eq_getValueCastD [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (hm : Raw.WFImp m.1)
    {a : α} {fallback : β a} :
    m.getD a fallback = getValueCastD a (toListModel m.1.buckets) fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
fallback : β a
⊢ m.getD a fallback = getValueCastD a (toListModel m.val.buckets) fallback

Tactic:
rw [getD_eq_getDₘ, getDₘ_eq_getValueCastD hm]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem HasFPowerSeriesWithinOnBall.sub (hf : HasFPowerSeriesWithinOnBall f pf s x r)
    (hg : HasFPowerSeriesWithinOnBall g pg s x r) :
    HasFPowerSeriesWithinOnBall (f - g) (pf - pg) s x r

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
hg : HasFPowerSeriesWithinOnBall g pg s x r
⊢ HasFPowerSeriesWithinOnBall (f - g) (pf - pg) s x r

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/Topology/Algebra/MulAction.lean
/-- Suppose that `N` acts on `X` and `M` continuously acts on `Y`.
Suppose that `g : Y → X` is an action homomorphism in the following sense:
there exists a continuous function `f : N → M` such that `g (c • x) = f c • g x`.
Then the action of `N` on `X` is continuous as well.

In many cases, `f = id` so that `g` is an action homomorphism in the sense of `MulActionHom`.
However, this version also works for semilinear maps and `f = Units.val`. -/
@[to_additive
  "Suppose that `N` additively acts on `X` and `M` continuously additively acts on `Y`.
Suppose that `g : Y → X` is an additive action homomorphism in the following sense:
there exists a continuous function `f : N → M` such that `g (c +ᵥ x) = f c +ᵥ g x`.
Then the action of `N` on `X` is continuous as well.

In many cases, `f = id` so that `g` is an action homomorphism in the sense of `AddActionHom`.
However, this version also works for `f = AddUnits.val`."]
lemma Topology.IsInducing.continuousSMul {N : Type*} [SMul N Y] [TopologicalSpace N] {f : N → M}
    (hg : IsInducing g) (hf : Continuous f) (hsmul : ∀ {c x}, g (c • x) = f c • g x) :
    ContinuousSMul N Y where
  continuous_smul

Proof state:
M : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : SMul M X
inst✝² : ContinuousSMul M X
g : Y → X
N : Type u_5
inst✝¹ : SMul N Y
inst✝ : TopologicalSpace N
f : N → M
hg : IsInducing g
hf : Continuous f
hsmul : ∀ {c : N} {x : Y}, g (c • x) = f c • g x
⊢ Continuous fun p => p.1 • p.2

Tactic:
simpa only [hg.continuous_iff, Function.comp_def, hsmul]
  using (hf.comp continuous_fst).smul <| hg.continuous.comp continuous_snd

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem mem_direction_iff_eq_vsub_right {s : AffineSubspace k P} {p : P} (hp : p ∈ s) (v : V) :
    v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p

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
v : V
⊢ v ∈ (fun x => x -ᵥ p) '' ↑s ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p

Tactic:
exact ⟨fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩, fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩⟩

Result:
no goals

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
v : V
⊢ v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p

Tactic:
rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_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
v : V
⊢ v ∈ (fun x => x -ᵥ p) '' ↑s ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m

Proof state:
m n : Nat
H : 0 < n
⊢ n * m / n = m

Tactic:
rw [Nat.mul_comm, Nat.mul_div_cancel _ H]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem cylinder_eq_pi (x : ∀ n, E n) (n : ℕ) :
    cylinder x n = Set.pi (Finset.range n : Set ℕ) fun i : ℕ => {x i}

Proof state:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
⊢ cylinder x n = (↑(Finset.range n)).pi fun i => {x i}

Tactic:
ext y

Result:
case h
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ y ∈ cylinder x n ↔ y ∈ (↑(Finset.range n)).pi fun i => {x i}

Proof state:
case h
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
y : (n : ℕ) → E n
⊢ y ∈ cylinder x n ↔ y ∈ (↑(Finset.range n)).pi fun i => {x i}

Tactic:
simp [cylinder]

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
theorem pairwise_ofFn {R : α → α → Prop} {n} {f : Fin n → α} :
    (ofFn f).Pairwise R ↔ ∀ ⦃i j⦄, i < j → R (f i) (f j)

Proof state:
α : Type u
R : α → α → Prop
n : ℕ
f : Fin n → α
⊢ Pairwise R (ofFn f) ↔ ∀ ⦃i j : Fin n⦄, i < j → R (f i) (f j)

Tactic:
simp only [pairwise_iff_getElem, length_ofFn, List.getElem_ofFn,
  (Fin.rightInverse_cast (length_ofFn f)).surjective.forall, Fin.forall_iff, Fin.cast_mk,
  Fin.mk_lt_mk, forall_comm (α := (_ : Prop)) (β := ℕ)]

Result:
no goals