harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean
theorem tendsto_polynomial_inv_mul_zero (p : ℝ[X]) :
    Tendsto (fun x ↦ p.eval x⁻¹ * expNegInvGlue x) (𝓝 0) (𝓝 0)

Proof state:
p : ℝ[X]
this : Tendsto (fun x => Polynomial.eval x⁻¹ p / rexp x⁻¹) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | 0 < x}) (𝓝 0)

Tactic:
refine this.congr' <| mem_of_superset self_mem_nhdsWithin fun x hx ↦ ?_

Result:
p : ℝ[X]
this : Tendsto (fun x => Polynomial.eval x⁻¹ p / rexp x⁻¹) (𝓝[>] 0) (𝓝 0)
x : ℝ
hx : x ∈ {x | 0 < x}
⊢ x ∈ {x | (fun x => Polynomial.eval x⁻¹ p / rexp x⁻¹ = (fun x => Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) x) x}

Proof state:
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | ¬x ≤ 0}) (𝓝 0)

Tactic:
simp only [not_le]

Result:
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | 0 < x}) (𝓝 0)

Proof state:
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * expNegInvGlue x) (𝓝 0) (𝓝 0)

Tactic:
simp only [expNegInvGlue, mul_ite, mul_zero]

Result:
p : ℝ[X]
⊢ Tendsto (fun x => if x ≤ 0 then 0 else Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0) (𝓝 0)

Proof state:
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | 0 < x}) (𝓝 0)

Tactic:
have : Tendsto (fun x ↦ p.eval x⁻¹ / exp x⁻¹) (𝓝[>] 0) (𝓝 0) :=
  p.tendsto_div_exp_atTop.comp tendsto_inv_nhdsGT_zero

Result:
p : ℝ[X]
this : Tendsto (fun x => Polynomial.eval x⁻¹ p / rexp x⁻¹) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | 0 < x}) (𝓝 0)

Proof state:
p : ℝ[X]
⊢ Tendsto (fun x => if x ≤ 0 then 0 else Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0) (𝓝 0)

Tactic:
refine tendsto_const_nhds.if ?_

Result:
p : ℝ[X]
⊢ Tendsto (fun x => Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x | ¬x ≤ 0}) (𝓝 0)

Proof state:
p : ℝ[X]
this : Tendsto (fun x => Polynomial.eval x⁻¹ p / rexp x⁻¹) (𝓝[>] 0) (𝓝 0)
x : ℝ
hx : x ∈ {x | 0 < x}
⊢ x ∈ {x | (fun x => Polynomial.eval x⁻¹ p / rexp x⁻¹ = (fun x => Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) x) x}

Tactic:
simp [expNegInvGlue, hx.out.not_le, exp_neg, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_eq_Ioc_same_iff : Icc a b = Ioc a b ↔ ¬a ≤ b where
  mp h

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h : ¬a ≤ b
⊢ Icc a b = Ioc a b

Tactic:
rw [Icc_eq_empty h, Ioc_eq_empty (mt le_of_lt h)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h : Icc a b = Ioc a b
⊢ ¬a ≤ b

Tactic:
simpa using Set.ext_iff.mp h a

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_filter_of_pairwise_eq_one [CommMonoid β] {f : ι → α} {g : α → β} {n : ι} {I : Finset ι}
    (hn : n ∈ I) (hf : (I : Set ι).Pairwise fun i j ↦ f i = f j → g (f i) = 1) :
    ∏ j ∈ filter (fun j ↦ f j = f n) I, g (f j) = g (f n)

Proof state:
α : Type u_6
β : Type u_7
ι : Type u_8
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
f : ι → α
g : α → β
n : ι
I : Finset ι
hn : n ∈ I
hf : (↑I).Pairwise fun i j => f i = f j → g (f i) = 1
j : ι
hj : j ≠ n ∧ j ∈ I ∧ f j = f n
⊢ g (f j) = 1

Tactic:
exact hf hj.2.1 hn hj.1 hj.2.2

Result:
no goals

Proof state:
α : Type u_6
β : Type u_7
ι : Type u_8
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
f : ι → α
g : α → β
n : ι
I : Finset ι
hn : n ∈ I
hf : (↑I).Pairwise fun i j => f i = f j → g (f i) = 1
h : ∀ j ∈ (filter (fun i => f i = f n) I).erase n, g (f j) = 1
⊢ f n = f n

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_6
β : Type u_7
ι : Type u_8
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
f : ι → α
g : α → β
n : ι
I : Finset ι
hn : n ∈ I
hf : (↑I).Pairwise fun i j => f i = f j → g (f i) = 1
⊢ ∏ j ∈ filter (fun j => f j = f n) I, g (f j) = g (f n)

Tactic:
have h j (hj : j ∈ (filter (fun i ↦ f i = f n) I).erase n) : g (f j) = 1 := by
  simp only [mem_erase, mem_filter] at hj
  exact hf hj.2.1 hn hj.1 hj.2.2

Result:
α : Type u_6
β : Type u_7
ι : Type u_8
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
f : ι → α
g : α → β
n : ι
I : Finset ι
hn : n ∈ I
hf : (↑I).Pairwise fun i j => f i = f j → g (f i) = 1
h : ∀ j ∈ (filter (fun i => f i = f n) I).erase n, g (f j) = 1
⊢ ∏ j ∈ filter (fun j => f j = f n) I, g (f j) = g (f n)

Proof state:
α : Type u_6
β : Type u_7
ι : Type u_8
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
f : ι → α
g : α → β
n : ι
I : Finset ι
hn : n ∈ I
hf : (↑I).Pairwise fun i j => f i = f j → g (f i) = 1
j : ι
hj : j ∈ (filter (fun i => f i = f n) I).erase n
⊢ g (f j) = 1

Tactic:
simp only [mem_erase, mem_filter] at hj

Result:
α : Type u_6
β : Type u_7
ι : Type u_8
inst✝¹ : DecidableEq α
inst✝ : CommMonoid β
f : ι → α
g : α → β
n : ι
I : Finset ι
hn : n ∈ I
hf : (↑I).Pairwise fun i j => f i = f j → g (f i) = 1
j : ι
hj : j ≠ n ∧ j ∈ I ∧ f j = f n
⊢ g (f j) = 1
-- Mathlib/Data/PNat/Xgcd.lean
theorem reduce_isReduced : ∀ u : XgcdType, u.reduce.IsReduced
  | u =>
    dite (u.r = 0)
      (fun h => by
        rw [reduce_a h]
        exact u.finish_isReduced)
      fun h => by
      have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
      rw [reduce_b h, flip_isReduced]
      apply reduce_isReduced

Proof state:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ x✝.reduce.IsReduced

Tactic:
rw [reduce_b h, flip_isReduced]

Result:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ u.step.reduce.IsReduced

Proof state:
x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
⊢ x✝.reduce.IsReduced

Tactic:
rw [reduce_a h]

Result:
x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
⊢ u.finish.IsReduced

Proof state:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
⊢ x✝.reduce.IsReduced

Tactic:
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h

Result:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ x✝.reduce.IsReduced

Proof state:
x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
⊢ u.finish.IsReduced

Tactic:
exact u.finish_isReduced

Result:
no goals

Proof state:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
this : sizeOf u.step < sizeOf u
⊢ u.step.reduce.IsReduced

Tactic:
apply reduce_isReduced

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_neg {A : M} (h : IsUnit A.det) : ∀ n : ℤ, A ^ (-n) = (A ^ n)⁻¹
  | (n : ℕ) => zpow_neg_natCast _ _
  | -[n+1] => by
    rw [zpow_negSucc, neg_negSucc, zpow_natCast, nonsing_inv_nonsing_inv]
    rw [det_pow]
    exact h.pow _

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ A ^ (- -[n+1]) = (A ^ -[n+1])⁻¹

Tactic:
rw [zpow_negSucc, neg_negSucc, zpow_natCast, nonsing_inv_nonsing_inv]

Result:
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A ^ (n + 1)).det

Proof state:
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A.det ^ (n + 1))

Tactic:
exact h.pow _

Result:
no goals

Proof state:
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A ^ (n + 1)).det

Tactic:
rw [det_pow]

Result:
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
n : ℕ
⊢ IsUnit (A.det ^ (n + 1))
-- Mathlib/Algebra/Group/Hom/Defs.lean
theorem map_pow [Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) (a : G) :
    ∀ n : ℕ, f (a ^ n) = f a ^ n
  | 0 => by rw [pow_zero, pow_zero, map_one]
  | n + 1 => by rw [pow_succ, pow_succ, map_mul, map_pow f a n]

Proof state:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
⊢ f (a ^ 0) = f a ^ 0

Tactic:
rw [pow_zero, pow_zero, map_one]

Result:
no goals

Proof state:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Monoid G
inst✝¹ : Monoid H
inst✝ : MonoidHomClass F G H
f : F
a : G
n : ℕ
⊢ f (a ^ (n + 1)) = f a ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ, map_mul, map_pow f a n]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem veblenWith_lt_veblenWith_iff :
    veblenWith f o₁ a < veblenWith f o₂ b ↔
      o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a < b

Proof state:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ (match cmp o₁ o₂ with
      | Ordering.eq => cmp a b
      | Ordering.lt => cmp a (veblenWith f o₂ b)
      | Ordering.gt => cmp (veblenWith f o₁ a) b) =
      Ordering.lt ↔
    o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a < b

Tactic:
aesop (add simp lt_asymm)

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o₁ a < veblenWith f o₂ b ↔
    o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a < b

Tactic:
rw [← cmp_eq_lt_iff, cmp_veblenWith hf]

Result:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ (match cmp o₁ o₂ with
      | Ordering.eq => cmp a b
      | Ordering.lt => cmp a (veblenWith f o₂ b)
      | Ordering.gt => cmp (veblenWith f o₁ a) b) =
      Ordering.lt ↔
    o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a < b
-- Mathlib/RingTheory/Ideal/Colon.lean
theorem _root_.Ideal.mem_colon_singleton {I : Ideal R} {x r : R} :
    r ∈ I.colon (Ideal.span {x}) ↔ r * x ∈ I

Proof state:
R : Type u_6
inst✝ : CommRing R
I : Ideal R
x r : R
⊢ r ∈ colon I (Ideal.span {x}) ↔ r * x ∈ I

Tactic:
simp only [← Ideal.submodule_span_eq, Submodule.mem_colon_singleton, smul_eq_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
/-- If `f : X → Y` is continuous and `Y` is equipped with the Borel sigma algebra, then
the push-forward of probability measures `f* : ProbabilityMeasure X → ProbabilityMeasure Y`
is continuous (in the topologies of convergence in distribution). -/
lemma continuous_map {f : Ω → Ω'} (f_cont : Continuous f) :
    Continuous (fun ν ↦ ProbabilityMeasure.map ν f_cont.measurable.aemeasurable)

Proof state:
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous f
⊢ Continuous fun ν => ν.map ⋯

Tactic:
rw [continuous_iff_continuousAt]

Result:
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous f
⊢ ∀ (x : ProbabilityMeasure Ω), ContinuousAt (fun ν => ν.map ⋯) x

Proof state:
Ω : Type u_1
Ω' : Type u_2
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : MeasurableSpace Ω'
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω'
inst✝ : BorelSpace Ω'
f : Ω → Ω'
f_cont : Continuous f
⊢ ∀ (x : ProbabilityMeasure Ω), ContinuousAt (fun ν => ν.map ⋯) x

Tactic:
exact fun _ ↦ tendsto_map_of_tendsto_of_continuous _ _ continuous_id.continuousAt f_cont

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_pi_div_six : sin (π / 6) = 1 / 2

Proof state:
⊢ cos (π / 2 - π / 6) = cos (π / 3)

Tactic:
congr

Result:
case e_x

⊢ π / 2 - π / 6 = π / 3

Proof state:
⊢ sin (π / 6) = 1 / 2

Tactic:
rw [← cos_pi_div_two_sub, ← cos_pi_div_three]

Result:
⊢ cos (π / 2 - π / 6) = cos (π / 3)

Proof state:
case e_x

⊢ π / 2 - π / 6 = π / 3

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma isoHomologyπ₀_inv_naturality [L.HasHomology 0] :
    HomologicalComplex.homologyMap φ 0 ≫ L.isoHomologyπ₀.inv =
      K.isoHomologyπ₀.inv ≫ HomologicalComplex.cyclesMap φ 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
K L : CochainComplex C ℕ
φ : K ⟶ L
inst✝¹ : HomologicalComplex.HasHomology K 0
inst✝ : HomologicalComplex.HasHomology L 0
⊢ HomologicalComplex.homologyMap φ 0 ≫ L.isoHomologyπ₀.inv = K.isoHomologyπ₀.inv ≫ HomologicalComplex.cyclesMap φ 0

Tactic:
simp only [← cancel_epi (K.homologyπ 0), HomologicalComplex.homologyπ_naturality_assoc,
  HomologicalComplex.isoHomologyπ_hom_inv_id, comp_id,
  HomologicalComplex.isoHomologyπ_hom_inv_id_assoc]

Result:
no goals
-- Mathlib/Analysis/Convex/Body.lean
theorem hausdorffEdist_coe : EMetric.hausdorffEdist (K : Set V) L = edist K L

Proof state:
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NormedSpace ℝ V
K L : ConvexBody V
⊢ EMetric.hausdorffEdist ↑K ↑L = ENNReal.ofReal (dist K L)

Tactic:
exact (ENNReal.ofReal_toReal hausdorffEdist_ne_top).symm

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NormedSpace ℝ V
K L : ConvexBody V
⊢ EMetric.hausdorffEdist ↑K ↑L = edist K L

Tactic:
rw [edist_dist]

Result:
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NormedSpace ℝ V
K L : ConvexBody V
⊢ EMetric.hausdorffEdist ↑K ↑L = ENNReal.ofReal (dist K L)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem push_beq_push [BEq α] {a b : α} {n : Nat} {v : Vector α n} {w : Vector α n} :
    (v.push a == w.push b) = (v == w && a == b)

Proof state:
case mk.mk
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.push a ==
      { toArray := toArray✝, size_toArray := size_toArray✝ }.push b) =
    ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ==
        { toArray := toArray✝, size_toArray := size_toArray✝ } &&
      a == b)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
v w : Vector α n
⊢ (v.push a == w.push b) = (v == w && a == b)

Tactic:
cases v

Result:
case mk
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
w : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.push a == w.push b) =
    ({ toArray := toArray✝, size_toArray := size_toArray✝ } == w && a == b)

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
w : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.push a == w.push b) =
    ({ toArray := toArray✝, size_toArray := size_toArray✝ } == w && a == b)

Tactic:
cases w

Result:
case mk.mk
α : Type u_1
inst✝ : BEq α
a b : α
n : Nat
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ }.push a ==
      { toArray := toArray✝, size_toArray := size_toArray✝ }.push b) =
    ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ==
        { toArray := toArray✝, size_toArray := size_toArray✝ } &&
      a == b)
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem localization_away_isOpenEmbedding (S : Type v) [CommSemiring S] [Algebra R S] (r : R)
    [IsLocalization.Away r S] : IsOpenEmbedding (comap (algebraMap R S)) where
  toIsEmbedding := localization_comap_isEmbedding S (Submonoid.powers r)
  isOpen_range

Proof state:
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ IsOpen (Set.range ⇑(comap (algebraMap R S)))

Tactic:
rw [localization_away_comap_range S r]

Result:
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ IsOpen ↑(basicOpen r)

Proof state:
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ IsOpen ↑(basicOpen r)

Tactic:
exact isOpen_basicOpen

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem powerSeriesPart_zero : powerSeriesPart (0 : R⸨X⸩) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ powerSeriesPart 0 = 0

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : Semiring R
n✝ : ℕ
⊢ (PowerSeries.coeff R n✝) (powerSeriesPart 0) = (PowerSeries.coeff R n✝) 0

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
n✝ : ℕ
⊢ (PowerSeries.coeff R n✝) (powerSeriesPart 0) = (PowerSeries.coeff R n✝) 0

Tactic:
simp [(PowerSeries.coeff _ _).map_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem pentagon_inv_inv_hom_inv_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i =
      f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv :=
  eq_of_inv_eq_inv (by simp)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv ≫ (α_ f g h).hom ▷ i) =
    inv (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
lemma freeLocus_eq_univ_iff [Module.FinitePresentation R M] :
    freeLocus R M = Set.univ ↔ Module.Projective R M

Proof state:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
⊢ freeLocus R M = Set.univ ↔ Projective R M

Tactic:
simp_rw [Set.eq_univ_iff_forall, mem_freeLocus]

Result:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
⊢ (∀ (x : PrimeSpectrum R), Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)) ↔
    Projective R M

Proof state:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
⊢ (∀ (x : PrimeSpectrum R), Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)) ↔
    Projective R M

Tactic:
exact ⟨fun H ↦ Module.projective_of_localization_maximal fun I hI ↦
  have := H ⟨I, hI.isPrime⟩; .of_free, fun H x ↦ Module.free_of_flat_of_isLocalRing⟩

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem zero_of_map_zero {P Q : C} (f : P ⟶ Q) : Function.Injective f → ∀ a, f a = 0 → a = 0 :=
  fun h a ha => by
  rw [← apply_zero f] at ha
  exact h ha

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

Tactic:
rw [← apply_zero f] at ha

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Injective (pseudoApply f)
a : Pseudoelement P
ha : pseudoApply f a = pseudoApply f 0
⊢ a = 0

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

Tactic:
exact h ha

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma integral_densityProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν]
    (n : ℕ) (a : α) {s : Set β} (hs : MeasurableSet s) :
    ∫ x, densityProcess κ ν n a x s ∂(ν a) = (κ a (univ ×ˢ s)).toReal

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫ (x : γ), κ.densityProcess ν n a x s ∂ν a = ((κ a) (univ ×ˢ s)).toReal

Tactic:
rw [← setIntegral_univ, setIntegral_densityProcess hκν _ _ hs MeasurableSet.univ]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem mk_finrank_eq_card_basis [Module.Finite R M] {ι : Type w} (h : Basis ι R M) :
    (finrank R M : Cardinal.{w}) = #ι

Proof state:
case intro
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
ι : Type w
h : Basis ι R M
val✝ : Fintype ι
⊢ ↑(finrank R M) = #ι

Tactic:
rw [Cardinal.mk_fintype, finrank_eq_card_basis h]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
ι : Type w
h : Basis ι R M
⊢ ↑(finrank R M) = #ι

Tactic:
cases @nonempty_fintype _ (Module.Finite.finite_basis h)

Result:
case intro
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
ι : Type w
h : Basis ι R M
val✝ : Fintype ι
⊢ ↑(finrank R M) = #ι
-- Mathlib/Logic/Function/DependsOn.lean
lemma dependsOn_iff_factorsThrough {f : (Π i, α i) → β} {s : Set ι} :
    DependsOn f s ↔ FactorsThrough f s.restrict

Proof state:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s : Set ι
⊢ DependsOn f s ↔ FactorsThrough f s.restrict

Tactic:
rw [DependsOn, FactorsThrough]

Result:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s : Set ι
⊢ (∀ ⦃x y : (i : ι) → α i⦄, (∀ i ∈ s, x i = y i) → f x = f y) ↔
    ∀ ⦃a b : (i : ι) → α i⦄, s.restrict a = s.restrict b → f a = f b

Proof state:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s : Set ι
⊢ (∀ ⦃x y : (i : ι) → α i⦄, (∀ i ∈ s, x i = y i) → f x = f y) ↔
    ∀ ⦃a b : (i : ι) → α i⦄, s.restrict a = s.restrict b → f a = f b

Tactic:
simp [funext_iff]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma snd_swapRight (κ : Kernel α (β × γ)) : snd (swapRight κ) = fst κ

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ a) {p | p.swap ∈ {p | p.2 ∈ s}} = (κ a) {p | p.1 ∈ s}

Tactic:
rfl

Result:
no goals

Proof state:
case h.h.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet {p | p.2 ∈ s}

Tactic:
exact measurable_snd hs

Result:
no goals

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ.swapRight.snd a) s = (κ.fst a) s

Tactic:
rw [snd_apply' _ _ hs, swapRight_apply', fst_apply' _ _ hs]

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ a) {p | p.swap ∈ {p | p.2 ∈ s}} = (κ a) {p | p.1 ∈ s}

case h.h.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet {p | p.2 ∈ s}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
⊢ κ.swapRight.snd = κ.fst

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ.swapRight.snd a) s = (κ.fst a) s
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.smul_mem_of_zero_mem (hs : Convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s) (hx : x ∈ s)
    {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) : t • x ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ t • x ∈ s

Tactic:
simpa using hs.add_smul_mem zero_mem (by simpa using hx) ht

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ 0 + x ∈ s

Tactic:
simpa using hx

Result:
no goals