harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_apply_getElem_length (x : α) (xs : List α) :
    formPerm (x :: xs) (x :: xs)[xs.length] = x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ (x :: xs).formPerm (x :: xs)[xs.length] = x

Tactic:
rw [getElem_cons_length _ _ _ rfl, formPerm_apply_getLast]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_nonpos_iff' (hx : 0 ≤ x) : logb b x ≤ 0 ↔ x ≤ 1

Proof state:
case inl
b : ℝ
hb : 1 < b
hx : 0 ≤ 0
⊢ logb b 0 ≤ 0 ↔ 0 ≤ 1

Tactic:
simp [le_refl, zero_le_one]

Result:
no goals

Proof state:
case inr
b x : ℝ
hb : 1 < b
hx✝ : 0 ≤ x
hx : 0 < x
⊢ logb b x ≤ 0 ↔ x ≤ 1

Tactic:
exact logb_nonpos_iff hb hx

Result:
no goals

Proof state:
b x : ℝ
hb : 1 < b
hx : 0 ≤ x
⊢ logb b x ≤ 0 ↔ x ≤ 1

Tactic:
rcases hx.eq_or_lt with (rfl | hx)

Result:
case inl
b : ℝ
hb : 1 < b
hx : 0 ≤ 0
⊢ logb b 0 ≤ 0 ↔ 0 ≤ 1

case inr
b x : ℝ
hb : 1 < b
hx✝ : 0 ≤ x
hx : 0 < x
⊢ logb b x ≤ 0 ↔ x ≤ 1
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem mul_continuousOn {f g : ℝ → A} (hf : IntervalIntegrable f μ a b)
    (hg : ContinuousOn g [[a, b]]) : IntervalIntegrable (fun x => f x * g x) μ a b

Proof state:
A : Type u_5
inst✝ : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntervalIntegrable f μ a b
hg : ContinuousOn g [[a, b]]
⊢ IntervalIntegrable (fun x => f x * g x) μ a b

Tactic:
rw [intervalIntegrable_iff] at hf ⊢

Result:
A : Type u_5
inst✝ : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntegrableOn f (Ι a b) μ
hg : ContinuousOn g [[a, b]]
⊢ IntegrableOn (fun x => f x * g x) (Ι a b) μ

Proof state:
A : Type u_5
inst✝ : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntegrableOn f (Ι a b) μ
hg : ContinuousOn g [[a, b]]
⊢ IntegrableOn (fun x => f x * g x) (Ι a b) μ

Tactic:
exact hf.mul_continuousOn_of_subset hg measurableSet_Ioc isCompact_uIcc Ioc_subset_Icc_self

Result:
no goals
-- Mathlib/Deprecated/Logic.lean
theorem decide_True' (h : Decidable True) : decide True = true

Proof state:
h : Decidable True
⊢ decide True = true

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem homogeneousComponent_apply :
    homogeneousComponent n φ = ∑ d ∈ φ.support with d.degree = n, monomial d (coeff d φ)

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
⊢ (homogeneousComponent n) φ =
    ∑ x ∈ Finset.filter (fun d => (weight fun x => 1) d = n) φ.support, (monomial x) (coeff x φ)

Tactic:
convert weightedHomogeneousComponent_apply n φ

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
⊢ (homogeneousComponent n) φ = ∑ d ∈ Finset.filter (fun d => d.degree = n) φ.support, (monomial d) (coeff d φ)

Tactic:
simp_rw [degree_eq_weight_one]

Result:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
n : ℕ
φ : MvPolynomial σ R
⊢ (homogeneousComponent n) φ =
    ∑ x ∈ Finset.filter (fun d => (weight fun x => 1) d = n) φ.support, (monomial x) (coeff x φ)
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_strict_mono {f g : α → ℝ≥0∞} {s : Set α} (hsm : MeasurableSet s)
    (hs : μ s ≠ 0) (hg : Measurable g) (hfi : ∫⁻ x in s, f x ∂μ ≠ ∞)
    (h : ∀ᵐ x ∂μ, x ∈ s → f x < g x) : ∫⁻ x in s, f x ∂μ < ∫⁻ x in s, g x ∂μ :=
  lintegral_strict_mono (by simp [hs]) hg.aemeasurable hfi ((ae_restrict_iff' hsm).mpr h)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
hsm : MeasurableSet s
hs : μ s ≠ 0
hg : Measurable g
hfi : ∫⁻ (x : α) in s, f x ∂μ ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x < g x
⊢ μ.restrict s ≠ 0

Tactic:
simp [hs]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem SuperpolynomialDecay.trans_eventually_abs_le (hf : SuperpolynomialDecay l k f)
    (hfg : abs ∘ g ≤ᶠ[l] abs ∘ f) : SuperpolynomialDecay l k g

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |k x ^ z * g x| ≤ |k x ^ z * f x|

Tactic:
calc
  |k x ^ z * g x| = |k x ^ z| * |g x| := abs_mul (k x ^ z) (g x)
  _ ≤ |k x ^ z| * |f x| := by gcongr _ * ?_; exact hx
  _ = |k x ^ z * f x| := (abs_mul (k x ^ z) (f x)).symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * g a|) l (𝓝 0)

Tactic:
refine fun z =>
  tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (hf z)
    (Eventually.of_forall fun x => abs_nonneg _) (hfg.mono fun x hx => ?_)

Result:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |k x ^ z * g x| ≤ |k x ^ z * f x|

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |k x ^ z| * |g x| ≤ |k x ^ z| * |f x|

Tactic:
gcongr _ * ?_

Result:
case h
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |g x| ≤ |f x|

Proof state:
case h
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |g x| ≤ |f x|

Tactic:
exact hx

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : SuperpolynomialDecay l k f
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ SuperpolynomialDecay l k g

Tactic:
rw [superpolynomialDecay_iff_abs_tendsto_zero] at hf ⊢

Result:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * g a|) l (𝓝 0)
-- Mathlib/Data/Set/Prod.lean
theorem pi_update_of_not_mem [DecidableEq ι] (hi : i ∉ s) (f : ∀ j, α j) (a : α i)
    (t : ∀ j, α j → Set (β j)) : (s.pi fun j => t j (update f i a j)) = s.pi fun j => t j (f j) :=
  (pi_congr rfl) fun j hj => by
    rw [update_of_ne]
    exact fun h => hi (h ▸ hj)

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∉ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
j : ι
hj : j ∈ s
⊢ j ≠ i

Tactic:
exact fun h => hi (h ▸ hj)

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∉ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
j : ι
hj : j ∈ s
⊢ t j (update f i a j) = t j (f j)

Tactic:
rw [update_of_ne]

Result:
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
s : Set ι
i : ι
inst✝ : DecidableEq ι
hi : i ∉ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
j : ι
hj : j ∈ s
⊢ j ≠ i
-- Mathlib/RingTheory/RootsOfUnity/Basic.lean
theorem map_rootsOfUnity (f : Mˣ →* Nˣ) (k : ℕ) : (rootsOfUnity k M).map f ≤ rootsOfUnity k N

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : Mˣ →* Nˣ
k : ℕ
⊢ Subgroup.map f (rootsOfUnity k M) ≤ rootsOfUnity k N

Tactic:
rintro _ ⟨ζ, h, rfl⟩

Result:
case intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : Mˣ →* Nˣ
k : ℕ
ζ : Mˣ
h : ζ ∈ ↑(rootsOfUnity k M)
⊢ f ζ ∈ rootsOfUnity k N

Proof state:
case intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : Mˣ →* Nˣ
k : ℕ
ζ : Mˣ
h : ζ ∈ ↑(rootsOfUnity k M)
⊢ f ζ ∈ rootsOfUnity k N

Tactic:
simp_all only [← map_pow, mem_rootsOfUnity, SetLike.mem_coe, MonoidHom.map_one]

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
lemma isMinOn_of_leftDeriv_eq_zero (hf : ConvexOn ℝ S f) (hx : x ∈ interior S)
    (hf_ld : derivWithin f (Iio x) x = 0) :
    IsMinOn f S x

Proof state:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x = 0
⊢ IsMinOn f S x

Tactic:
refine hf.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg hx hf_ld.le ?_

Result:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x = 0
⊢ 0 ≤ derivWithin f (Ioi x) x

Proof state:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x = 0
⊢ 0 ≤ derivWithin f (Ioi x) x

Tactic:
exact hf_ld.symm.le.trans (hf.leftDeriv_le_rightDeriv_of_mem_interior hx)

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem equalizerSubobject_factors_iff {W : C} (h : W ⟶ X) :
    (equalizerSubobject f g).Factors h ↔ h ≫ f = h ≫ g :=
  ⟨fun w => by
    rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, equalizerSubobject_arrow_comp,
      Category.assoc],
    equalizerSubobject_factors f g h⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
W : C
h : W ⟶ X
w : (equalizerSubobject f g).Factors h
⊢ h ≫ f = h ≫ g

Tactic:
rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, equalizerSubobject_arrow_comp,
  Category.assoc]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem IsPrimitive.ne_zero [Nontrivial R] {p : R[X]} (hp : p.IsPrimitive) : p ≠ 0

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
p : R[X]
hp : p.IsPrimitive
⊢ p ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hp : IsPrimitive 0
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
hp : IsPrimitive 0
⊢ False

Tactic:
exact (hp 0 (dvd_zero (C 0))).ne_zero rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem mul_sub_left_distrib (a b c : α) : a * (b - c) = a * b - a * c

Proof state:
α : Type u
inst✝ : NonUnitalNonAssocRing α
a b c : α
⊢ a * (b - c) = a * b - a * c

Tactic:
simpa only [sub_eq_add_neg, neg_mul_eq_mul_neg] using mul_add a b (-c)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem isSome_or : (or o o').isSome = (o.isSome || o'.isSome)

Proof state:
α✝ : Type u_1
o o' : Option α✝
⊢ (o.or o').isSome = (o.isSome || o'.isSome)

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem le_nhds_infty {f : Filter (OnePoint X)} :
    f ≤ 𝓝 ∞ ↔ ∀ s : Set X, IsClosed s → IsCompact s → (↑) '' sᶜ ∪ {∞} ∈ f

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
f : Filter (OnePoint X)
⊢ f ≤ 𝓝 ∞ ↔ ∀ (s : Set X), IsClosed s → IsCompact s → some '' sᶜ ∪ {∞} ∈ f

Tactic:
simp only [hasBasis_nhds_infty.ge_iff, and_imp]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Module/FiniteDimensional.lean
theorem isTorsion_of_aeval_eq_zero [CommSemiring R] [NoZeroDivisors R] [Semiring A] [Algebra R A]
    [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M]
    {p : R[X]} (h : aeval a p = 0) (h' : p ≠ 0) :
    IsTorsion R[X] (AEval R M a)

Proof state:
R : Type u_1
M : Type u_3
A : Type u_4
a : A
inst✝⁷ : CommSemiring R
inst✝⁶ : NoZeroDivisors R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p : R[X]
h : (aeval a) p = 0
h' : p ≠ 0
hp : p ∈ nonZeroDivisors R[X]
⊢ IsTorsion R[X] (AEval R M a)

Tactic:
exact fun x ↦ ⟨⟨p, hp⟩, (of R M a).symm.injective <| by simp [h]⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
A : Type u_4
a : A
inst✝⁷ : CommSemiring R
inst✝⁶ : NoZeroDivisors R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p : R[X]
h : (aeval a) p = 0
h' : p ≠ 0
⊢ IsTorsion R[X] (AEval R M a)

Tactic:
have hp : p ∈ nonZeroDivisors R[X] := fun q hq ↦ Or.resolve_right (mul_eq_zero.mp hq) h'

Result:
R : Type u_1
M : Type u_3
A : Type u_4
a : A
inst✝⁷ : CommSemiring R
inst✝⁶ : NoZeroDivisors R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p : R[X]
h : (aeval a) p = 0
h' : p ≠ 0
hp : p ∈ nonZeroDivisors R[X]
⊢ IsTorsion R[X] (AEval R M a)

Proof state:
R : Type u_1
M : Type u_3
A : Type u_4
a : A
inst✝⁷ : CommSemiring R
inst✝⁶ : NoZeroDivisors R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
p : R[X]
h : (aeval a) p = 0
h' : p ≠ 0
hp : p ∈ nonZeroDivisors R[X]
x : AEval R M a
⊢ (of R M a).symm (⟨p, hp⟩ • x) = (of R M a).symm 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem jacobson_quotient_of_le {I : Ideal R} [I.IsTwoSided] (le : I ≤ jacobson R) :
    jacobson (R ⧸ I) = Submodule.map (Ideal.Quotient.mk I).toSemilinearMap (jacobson R) :=
  .symm <| Module.map_jacobson_of_ker_le (by exact Ideal.Quotient.mk_surjective) <| by
    rwa [← I.ker_mkQ] at le

Proof state:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
le : I ≤ jacobson R
⊢ LinearMap.ker (Ideal.Quotient.mk I).toSemilinearMap ≤ Module.jacobson R R

Tactic:
rwa [← I.ker_mkQ] at le

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
le : I ≤ jacobson R
⊢ Function.Surjective ⇑(Ideal.Quotient.mk I).toSemilinearMap

Tactic:
exact Ideal.Quotient.mk_surjective

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem map_succ (a : Fin (n + 1) → ℕ) :
    map d a = a 0 + (∑ x : Fin n, a x.succ * d ^ (x : ℕ)) * d

Proof state:
n d : ℕ
a : Fin (n + 1) → ℕ
⊢ (map d) a = a 0 + (∑ x : Fin n, a x.succ * d ^ ↑x) * d

Tactic:
simp [map, Fin.sum_univ_succ, _root_.pow_succ, ← mul_assoc, ← sum_mul]

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

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

Tactic:
simp_to_raw using Raw₀.getKey?_insert

Result:
no goals
-- Mathlib/Topology/ShrinkingLemma.lean
theorem subset (v : PartialRefinement u s p) (i : ι) : v i ⊆ u i

Proof state:
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
v : PartialRefinement u s p
i : ι
⊢ v.toFun i ⊆ u i

Tactic:
classical
exact if h : i ∈ v.carrier then subset_closure.trans (v.closure_subset h) else (v.apply_eq h).le

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
u : ι → Set X
s : Set X
p : Set X → Prop
v : PartialRefinement u s p
i : ι
⊢ v.toFun i ⊆ u i

Tactic:
exact if h : i ∈ v.carrier then subset_closure.trans (v.closure_subset h) else (v.apply_eq h).le

Result:
no goals
-- Mathlib/RingTheory/Ideal/Cotangent.lean
lemma CotangentSpace.span_image_eq_top_iff [IsNoetherianRing R] {s : Set (maximalIdeal R)} :
    Submodule.span (ResidueField R) ((maximalIdeal R).toCotangent '' s) = ⊤ ↔
      Submodule.span R s = ⊤

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Submodule.span R (⇑(maximalIdeal R).toCotangent '' s) = Submodule.restrictScalars R ⊤ ↔
    Submodule.map (maximalIdeal R).toCotangent (Submodule.span R s) = ⊤

Tactic:
simp only [Ideal.toCotangent_apply, Submodule.restrictScalars_top, Submodule.map_span]

Result:
no goals

Proof state:
case hsur
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Function.Surjective ⇑(algebraMap R (ResidueField R))

Tactic:
exact Ideal.Quotient.mk_surjective

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s) = ⊤ ↔ Submodule.span R s = ⊤

Tactic:
rw [← map_eq_top_iff, ← (Submodule.restrictScalars_injective R ..).eq_iff,
  Submodule.restrictScalars_span]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Submodule.span R (⇑(maximalIdeal R).toCotangent '' s) = Submodule.restrictScalars R ⊤ ↔
    Submodule.map (maximalIdeal R).toCotangent (Submodule.span R s) = ⊤

case hsur
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Function.Surjective ⇑(algebraMap R (ResidueField R))
-- Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean
lemma unitization_nnnorm_inr (x : A) : ‖(WithLp.equiv 1 (Unitization 𝕜 A)).symm x‖₊ = ‖x‖₊

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NonUnitalNormedRing A
inst✝ : NormedSpace 𝕜 A
x : A
⊢ ‖(WithLp.equiv 1 (Unitization 𝕜 A)).symm ↑x‖₊ = ‖x‖₊

Tactic:
simp [unitization_nnnorm_def]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Basic.lean
/--
If `lim` of shape `J` into an abelian category `C` preserves epimorphisms, then `C` has AB* of
shape `J`.
-/
lemma hasExactLimitsOfShape_of_preservesEpi [HasLimitsOfShape J C]
    [PreservesEpimorphisms (lim (J := J) (C := C))] : HasExactLimitsOfShape J C where
  preservesFiniteColimits

Proof state:
case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasLimitsOfShape J C
inst✝ : lim.PreservesEpimorphisms
⊢ lim.Additive

Tactic:
exact additive_of_preservesBinaryBiproducts _

Result:
no goals

Proof state:
case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasLimitsOfShape J C
inst✝ : lim.PreservesEpimorphisms
⊢ lim.PreservesHomology

Tactic:
exact preservesHomology_of_preservesEpis_and_kernels _

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasLimitsOfShape J C
inst✝ : lim.PreservesEpimorphisms
⊢ PreservesFiniteColimits lim

Tactic:
apply (config := { allowSynthFailures := true }) preservesFiniteColimits_of_preservesHomology

Result:
case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasLimitsOfShape J C
inst✝ : lim.PreservesEpimorphisms
⊢ lim.PreservesHomology

case inst
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : HasLimitsOfShape J C
inst✝ : lim.PreservesEpimorphisms
⊢ lim.Additive
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem map_associator (X Y Z : C) :
    F.map (α_ X Y Z).hom =
      δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫
        (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
⊢ F.map (α_ X Y Z).hom =
    δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ F Y Z ≫ μ F X (Y ⊗ Z)

Tactic:
rw [← LaxMonoidal.associativity F, whiskerRight_δ_μ_assoc, δ_μ_assoc]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem equiv_one (hs1 : 1 ∈ S) (ht1 : 1 ∈ T) :
    hST.equiv 1 = (⟨1, hs1⟩, ⟨1, ht1⟩)

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
hs1 : 1 ∈ S
ht1 : 1 ∈ T
⊢ 1 = hST.equiv.symm (⟨1, hs1⟩, ⟨1, ht1⟩)

Tactic:
simp [equiv]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
hs1 : 1 ∈ S
ht1 : 1 ∈ T
⊢ hST.equiv 1 = (⟨1, hs1⟩, ⟨1, ht1⟩)

Tactic:
rw [Equiv.apply_eq_iff_eq_symm_apply]

Result:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
hs1 : 1 ∈ S
ht1 : 1 ∈ T
⊢ 1 = hST.equiv.symm (⟨1, hs1⟩, ⟨1, ht1⟩)
-- Mathlib/MeasureTheory/Measure/AEDisjoint.lean
theorem iUnion_left_iff {ι : Sort*} [Countable ι] {s : ι → Set α} :
    AEDisjoint μ (⋃ i, s i) t ↔ ∀ i, AEDisjoint μ (s i) t

Proof state:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
t : Set α
ι : Sort u_3
inst✝ : Countable ι
s : ι → Set α
⊢ AEDisjoint μ (⋃ i, s i) t ↔ ∀ (i : ι), AEDisjoint μ (s i) t

Tactic:
simp only [AEDisjoint, iUnion_inter, measure_iUnion_null_iff]

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map_map₂_right_comm {f : α → β' → γ} {g : β → β'} {f' : α → β → δ} {g' : δ → γ}
    (h_right_comm : ∀ a b, f a (g b) = g' (f' a b)) :
    map₂ f a (b.map g) = (map₂ f' a b).map g'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
β' : Type u_6
f : α → β' → γ
g : β → β'
f' : α → β → δ
g' : δ → γ
h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)
⊢ map₂ f a (Option.map g b) = Option.map g' (map₂ f' a b)

Tactic:
cases a <;> cases b <;> simp [h_right_comm]

Result:
no goals
-- Mathlib/Order/RelSeries.lean
theorem mem_toList : x ∈ s.toList ↔ x ∈ s

Proof state:
α : Type u_1
r : Rel α α
s : RelSeries r
x : α
⊢ x ∈ s.toList ↔ x ∈ s

Tactic:
rw [RelSeries.toList, List.mem_ofFn', RelSeries.mem_def]

Result:
no goals
-- Mathlib/Algebra/Lie/Rank.lean
lemma isRegular_iff_finrank_engel_eq_rank (x : L) :
    IsRegular K x ↔ finrank K (engel K x) = rank K L

Proof state:
K : Type u_7
L : Type u_8
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
x : L
⊢ IsRegular K x ↔ finrank K ↥(engel K x) = rank K L

Tactic:
rw [isRegular_iff_natTrailingDegree_charpoly_eq_rank, finrank_engel]

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Hom.lean
lemma AddMonoidHom.apply_nat (f : ℕ →+ M) (n : ℕ) : f n = n • f 1

Proof state:
M : Type u_2
inst✝ : AddMonoid M
f : ℕ →+ M
n : ℕ
⊢ f n = n • f 1

Tactic:
rw [← multiplesHom_symm_apply, ← multiplesHom_apply, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Topology/Algebra/Affine.lean
theorem homothety_isOpenMap (x : F) (t : R) (ht : t ≠ 0) : IsOpenMap <| homothety x t

Proof state:
R : Type u_1
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Field R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
ht : t ≠ 0
⊢ IsOpenMap ⇑(homothety x t)

Tactic:
apply IsOpenMap.of_inverse (homothety_continuous x t⁻¹) <;> intro e <;>
  simp [← AffineMap.comp_apply, ← homothety_mul, ht]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_eq' [Fintype σ] (g : R →+* S₁) (X : σ → S₁) (f : MvPolynomial σ R) :
    f.eval₂ g X = ∑ d ∈ f.support, g (f.coeff d) * ∏ i, X i ^ d i

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Fintype σ
g : R →+* S₁
X : σ → S₁
f : MvPolynomial σ R
⊢ ∑ d ∈ f.support, g (coeff d f) * ∏ i ∈ d.support, X i ^ d i =
    ∑ x ∈ f.support, g (coeff x f) * x.prod fun a b => X a ^ b

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Fintype σ
g : R →+* S₁
X : σ → S₁
f : MvPolynomial σ R
⊢ eval₂ g X f = ∑ d ∈ f.support, g (coeff d f) * ∏ i : σ, X i ^ d i

Tactic:
simp only [eval₂_eq, ← Finsupp.prod_pow]

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Fintype σ
g : R →+* S₁
X : σ → S₁
f : MvPolynomial σ R
⊢ ∑ d ∈ f.support, g (coeff d f) * ∏ i ∈ d.support, X i ^ d i =
    ∑ x ∈ f.support, g (coeff x f) * x.prod fun a b => X a ^ b