harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem Finset.hasProd_compl_iff (s : Finset β) :
    HasProd (fun x : { x // x ∉ s } ↦ f x) a ↔ HasProd f (a * ∏ i ∈ s, f i) :=
  (s.hasProd f).hasProd_compl_iff.trans <| by rw [mul_comm]

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a : α
s : Finset β
⊢ HasProd f ((∏ b ∈ s, f b) * a) ↔ HasProd f (a * ∏ i ∈ s, f i)

Tactic:
rw [mul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
lemma HasRightDerivedFunctor.mk' [RF.IsRightDerivedFunctor α W] :
    HasRightDerivedFunctor F W

Proof state:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
inst✝² : Category.{u_6, u_3} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
⊢ F.HasRightDerivedFunctor W

Tactic:
have := IsRightDerivedFunctor.isLeftKanExtension RF α W

Result:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
inst✝² : Category.{u_6, u_3} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
this : RF.IsLeftKanExtension α
⊢ F.HasRightDerivedFunctor W

Proof state:
C : Type u_1
D : Type u_2
H : Type u_3
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
inst✝² : Category.{u_6, u_3} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
this : RF.IsLeftKanExtension α
⊢ F.HasRightDerivedFunctor W

Tactic:
simpa only [hasRightDerivedFunctor_iff F L W] using HasLeftKanExtension.mk RF α

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma restrict_spanning_iff' : (M ↾ R).Spanning S ↔ R ∩ M.E ⊆ M.closure S ∧ S ⊆ R

Proof state:
α : Type u_2
M : Matroid α
R S : Set α
⊢ (M ↾ R).Spanning S ↔ R ∩ M.E ⊆ M.closure S ∧ S ⊆ R

Tactic:
rw [spanning_iff, restrict_closure_eq', restrict_ground_eq, and_congr_left_iff,
  diff_eq_compl_inter, ← union_inter_distrib_right, inter_eq_right, union_comm,
  ← diff_subset_iff, diff_compl]

Result:
α : Type u_2
M : Matroid α
R S : Set α
⊢ S ⊆ R → (R ∩ M.E ⊆ M.closure (S ∩ R) ↔ R ∩ M.E ⊆ M.closure S)

Proof state:
α : Type u_2
M : Matroid α
R S : Set α
⊢ S ⊆ R → (R ∩ M.E ⊆ M.closure (S ∩ R) ↔ R ∩ M.E ⊆ M.closure S)

Tactic:
intro hSR

Result:
α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
⊢ R ∩ M.E ⊆ M.closure (S ∩ R) ↔ R ∩ M.E ⊆ M.closure S

Proof state:
α : Type u_2
M : Matroid α
R S : Set α
hSR : S ⊆ R
⊢ R ∩ M.E ⊆ M.closure (S ∩ R) ↔ R ∩ M.E ⊆ M.closure S

Tactic:
rw [inter_eq_self_of_subset_left hSR]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_deriv_mul_eq_sub_of_hasDeriv_right {u v u' v' : ℝ → A}
    (hu : ContinuousOn u [[a, b]])
    (hv : ContinuousOn v [[a, b]])
    (huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x)
    (hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x)
    (hu' : IntervalIntegrable u' volume a b)
    (hv' : IntervalIntegrable v' volume a b) :
    ∫ x in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

Proof state:
A : Type u_4
a b : ℝ
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

Tactic:
apply integral_eq_sub_of_hasDeriv_right (hu.mul hv) fun x hx ↦ (huu' x hx).mul (hvv' x hx)

Result:
A : Type u_4
a b : ℝ
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable (fun x => u' x * v x + u x * v' x) volume a b

Proof state:
A : Type u_4
a b : ℝ
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (a ⊓ b) (a ⊔ b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable (fun x => u' x * v x + u x * v' x) volume a b

Tactic:
exact (hu'.mul_continuousOn hv).add (hv'.continuousOn_mul hu)

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_eval_cast (n : ℕ) (k : ℤ) :
    (((descPochhammer ℤ n).eval k : ℤ) : R) = ((descPochhammer R n).eval k : R)

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
k : ℤ
⊢ ↑(eval k (descPochhammer ℤ n)) = eval (↑k) (descPochhammer R n)

Tactic:
rw [← descPochhammer_map (algebraMap ℤ R), eval_map, ← eq_intCast (algebraMap ℤ R)]

Result:
R : Type u
inst✝ : Ring R
n : ℕ
k : ℤ
⊢ (algebraMap ℤ R) (eval k (descPochhammer ℤ n)) = eval₂ (algebraMap ℤ R) (↑k) (descPochhammer ℤ n)

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
k : ℤ
⊢ (algebraMap ℤ R) (eval k (descPochhammer ℤ n)) = eval₂ (algebraMap ℤ R) (↑k) (descPochhammer ℤ n)

Tactic:
simp only [algebraMap_int_eq, eq_intCast, eval₂_at_intCast, Nat.cast_id, eq_natCast, Int.cast_id]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem fromGlued_isOpenEmbedding : IsOpenEmbedding 𝒰.fromGlued.base :=
  .of_continuous_injective_isOpenMap (by fun_prop) 𝒰.fromGlued_injective 𝒰.fromGlued_open_map

Proof state:
X : Scheme
𝒰 : X.OpenCover
⊢ Continuous ⇑(ConcreteCategory.hom (fromGlued 𝒰).base)

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem inf_sdiff_self_right : x ⊓ y \ x = ⊥ :=
  calc
    x ⊓ y \ x = (x ⊓ y ⊔ x \ y) ⊓ y \ x

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊓ y ⊔ x \ y) ⊓ y \ x = x ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x

Tactic:
rw [inf_sup_right]

Result:
no goals

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y \ x = (x ⊓ y ⊔ x \ y) ⊓ y \ x

Tactic:
rw [sup_inf_sdiff]

Result:
no goals

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x = ⊥

Tactic:
rw [inf_comm x y, inf_inf_sdiff, sdiff_inf_sdiff, bot_sup_eq]

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
lemma doubleDualEmb_bijective : Bijective (doubleDualEmb : α → AddChar (AddChar α ℂ) ℂ)

Proof state:
case intro
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Finite α
val✝ : Fintype α
⊢ Bijective ⇑doubleDualEmb

Tactic:
exact (Fintype.bijective_iff_injective_and_card _).2
  ⟨doubleDualEmb_injective, card_eq.symm.trans card_eq.symm⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Finite α
⊢ Bijective ⇑doubleDualEmb

Tactic:
cases nonempty_fintype α

Result:
case intro
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Finite α
val✝ : Fintype α
⊢ Bijective ⇑doubleDualEmb
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem multiplicity_sub_multiplicity {q : ℚ} (hp : p ≠ 1) (hq : q ≠ 0) :
    padicValRat p q = multiplicity (p : ℤ) q.num - multiplicity p q.den

Proof state:
p : ℕ
q : ℚ
hp : p ≠ 1
hq : q ≠ 0
⊢ padicValRat p q = ↑(multiplicity (↑p) q.num) - ↑(multiplicity p q.den)

Tactic:
rw [padicValRat, padicValInt.of_ne_one_ne_zero hp (Rat.num_ne_zero.2 hq),
  padicValNat_def' hp q.pos]

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Ico : (some : α → WithTop α) '' Ico a b = Ico (a : WithTop α) b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Ico a b = Ico ↑a ↑b

Tactic:
rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ico_subset_Iio_self <| Iio_subset_Iio le_top)]

Result:
no goals
-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem hasseDeriv_apply :
    hasseDeriv k f = f.sum fun i r => monomial (i - k) (↑(i.choose k) * r)

Proof state:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (hasseDeriv k) f = f.sum fun i r => (monomial (i - k)) (↑(i.choose k) * r)

Tactic:
dsimp [hasseDeriv]

Result:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (f.sum fun x1 x2 => (monomial (x1 - k)) (x1.choose k • x2)) = f.sum fun i r => (monomial (i - k)) (↑(i.choose k) * r)

Proof state:
case e_f.h.h.a.e_a.h.e_6.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
x✝¹ : ℕ
x✝ : R
n✝ : ℕ
⊢ x✝¹.choose k • x✝ = ↑(x✝¹.choose k) * x✝

Tactic:
apply nsmul_eq_mul

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (f.sum fun x1 x2 => (monomial (x1 - k)) (x1.choose k • x2)) = f.sum fun i r => (monomial (i - k)) (↑(i.choose k) * r)

Tactic:
congr

Result:
case e_f
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (fun x1 x2 => (monomial (x1 - k)) (x1.choose k • x2)) = fun i r => (monomial (i - k)) (↑(i.choose k) * r)

Proof state:
case e_f
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
⊢ (fun x1 x2 => (monomial (x1 - k)) (x1.choose k • x2)) = fun i r => (monomial (i - k)) (↑(i.choose k) * r)

Tactic:
ext

Result:
case e_f.h.h.a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
x✝¹ : ℕ
x✝ : R
n✝ : ℕ
⊢ ((monomial (x✝¹ - k)) (x✝¹.choose k • x✝)).coeff n✝ = ((monomial (x✝¹ - k)) (↑(x✝¹.choose k) * x✝)).coeff n✝

Proof state:
case e_f.h.h.a
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
x✝¹ : ℕ
x✝ : R
n✝ : ℕ
⊢ ((monomial (x✝¹ - k)) (x✝¹.choose k • x✝)).coeff n✝ = ((monomial (x✝¹ - k)) (↑(x✝¹.choose k) * x✝)).coeff n✝

Tactic:
congr

Result:
case e_f.h.h.a.e_a.h.e_6.h
R : Type u_1
inst✝ : Semiring R
k : ℕ
f : R[X]
x✝¹ : ℕ
x✝ : R
n✝ : ℕ
⊢ x✝¹.choose k • x✝ = ↑(x✝¹.choose k) * x✝
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem setIntegral_dirac [MeasurableSpace α] [MeasurableSingletonClass α] (f : α → E) (a : α)
    (s : Set α) [Decidable (a ∈ s)] :
    ∫ x in s, f x ∂Measure.dirac a = if a ∈ s then f a else 0

Proof state:
case pos
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst✝ : Decidable (a ∈ s)
h✝ : a ∈ s
⊢ ∫ (x : α), f x ∂Measure.dirac a = f a

Tactic:
exact integral_dirac _ _

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst✝ : Decidable (a ∈ s)
h✝ : a ∉ s
⊢ ∫ (x : α), f x ∂0 = 0

Tactic:
exact integral_zero_measure _

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst✝ : Decidable (a ∈ s)
⊢ ∫ (x : α) in s, f x ∂Measure.dirac a = if a ∈ s then f a else 0

Tactic:
rw [restrict_dirac]

Result:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst✝ : Decidable (a ∈ s)
⊢ (∫ (x : α), f x ∂if a ∈ s then Measure.dirac a else 0) = if a ∈ s then f a else 0

Proof state:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst✝ : Decidable (a ∈ s)
⊢ (∫ (x : α), f x ∂if a ∈ s then Measure.dirac a else 0) = if a ∈ s then f a else 0

Tactic:
split_ifs

Result:
case pos
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst✝ : Decidable (a ∈ s)
h✝ : a ∈ s
⊢ ∫ (x : α), f x ∂Measure.dirac a = f a

case neg
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst✝ : Decidable (a ∈ s)
h✝ : a ∉ s
⊢ ∫ (x : α), f x ∂0 = 0
-- Mathlib/Order/SymmDiff.lean
theorem bot_bihimp : ⊥ ⇔ a = aᶜ

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ ⊥ ⇔ a = aᶜ

Tactic:
simp [bihimp]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem extract : ∀ {s}, Valid s → Valid ⟨s.toString, b, e⟩ → Valid (s.extract b e)
  | _, h₁, h₂ => by
    let ⟨l, m, r, h₁⟩ := h₁.validFor
    rw [h₁.toString] at h₂
    let ⟨ml, mm, mr, h₂⟩ := h₂.validFor
    have ⟨l', r', h₃⟩ := h₁.extract h₂
    exact h₃.valid

Proof state:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
h₂ : { str := x✝.toString, startPos := b, stopPos := e }.Valid
l m r : List Char
h₁ : ValidFor l m r x✝
⊢ (x✝.extract b e).Valid

Tactic:
rw [h₁.toString] at h₂

Result:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
l m : List Char
h₂ : { str := { data := m }, startPos := b, stopPos := e }.Valid
r : List Char
h₁ : ValidFor l m r x✝
⊢ (x✝.extract b e).Valid

Proof state:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
l m : List Char
h₂✝ : { str := { data := m }, startPos := b, stopPos := e }.Valid
r : List Char
h₁ : ValidFor l m r x✝
ml mm mr : List Char
h₂ : ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }
l' r' : List Char
h₃ : ValidFor l' mm r' (x✝.extract b e)
⊢ (x✝.extract b e).Valid

Tactic:
exact h₃.valid

Result:
no goals

Proof state:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
l m : List Char
h₂✝ : { str := { data := m }, startPos := b, stopPos := e }.Valid
r : List Char
h₁ : ValidFor l m r x✝
ml mm mr : List Char
h₂ : ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }
⊢ (x✝.extract b e).Valid

Tactic:
have ⟨l', r', h₃⟩ := h₁.extract h₂

Result:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
l m : List Char
h₂✝ : { str := { data := m }, startPos := b, stopPos := e }.Valid
r : List Char
h₁ : ValidFor l m r x✝
ml mm mr : List Char
h₂ : ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }
l' r' : List Char
h₃ : ValidFor l' mm r' (x✝.extract b e)
⊢ (x✝.extract b e).Valid

Proof state:
b e : Pos
x✝ : Substring
h₁ : x✝.Valid
h₂ : { str := x✝.toString, startPos := b, stopPos := e }.Valid
⊢ (x✝.extract b e).Valid

Tactic:
let ⟨l, m, r, h₁⟩ := h₁.validFor

Result:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
h₂ : { str := x✝.toString, startPos := b, stopPos := e }.Valid
l m r : List Char
h₁ : ValidFor l m r x✝
⊢ (x✝.extract b e).Valid

Proof state:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
l m : List Char
h₂ : { str := { data := m }, startPos := b, stopPos := e }.Valid
r : List Char
h₁ : ValidFor l m r x✝
⊢ (x✝.extract b e).Valid

Tactic:
let ⟨ml, mm, mr, h₂⟩ := h₂.validFor

Result:
b e : Pos
x✝ : Substring
h₁✝ : x✝.Valid
l m : List Char
h₂✝ : { str := { data := m }, startPos := b, stopPos := e }.Valid
r : List Char
h₁ : ValidFor l m r x✝
ml mm mr : List Char
h₂ : ValidFor ml mm mr { str := { data := m }, startPos := b, stopPos := e }
⊢ (x✝.extract b e).Valid
-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem isClosed_image_of_isClosed {s : Set M} (hsc : IsClosed s) (hs : s ⊆ support f) :
    IsClosed (extChartAt I c '' s)

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
s : Set M
hsc : IsClosed s
hs : s ⊆ support ↑f
⊢ IsClosed (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s)

Tactic:
refine ContinuousOn.preimage_isClosed_of_isClosed
  ((continuousOn_extChartAt_symm _).mono f.closedBall_subset) ?_ hsc

Result:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
s : Set M
hsc : IsClosed s
hs : s ⊆ support ↑f
⊢ IsClosed (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
s : Set M
hsc : IsClosed s
hs : s ⊆ support ↑f
⊢ IsClosed (↑(extChartAt I c) '' s)

Tactic:
rw [f.image_eq_inter_preimage_of_subset_support hs]

Result:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
s : Set M
hsc : IsClosed s
hs : s ⊆ support ↑f
⊢ IsClosed (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I ∩ ↑(extChartAt I c).symm ⁻¹' s)

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
s : Set M
hsc : IsClosed s
hs : s ⊆ support ↑f
⊢ IsClosed (closedBall (↑(extChartAt I c) c) f.rOut ∩ range ↑I)

Tactic:
exact IsClosed.inter isClosed_closedBall I.isClosed_range

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma add_of_Y_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hx : P x * Q z = Q x * P z) (hy : P y * Q z = Q y * P z) (hy' : P y * Q z = W.negY Q * P z) :
    W.add P Q = W.dblU P • ![0, 1, 0]

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.add P Q = W.dblU P • ![0, 1, 0]

Tactic:
rw [add, if_pos <| equiv_of_X_eq_of_Y_eq hPz hQz hx hy, dblXYZ_of_Y_eq hP hPz hQz hx hy hy']

Result:
no goals
-- Mathlib/Logic/Hydra.lean
lemma cutExpand_double {a a₁ a₂} (h₁ : r a₁ a) (h₂ : r a₂ a) : CutExpand r {a₁, a₂} {a} :=
  cutExpand_singleton <| by
    simp only [insert_eq_cons, mem_cons, mem_singleton, forall_eq_or_imp, forall_eq]
    tauto

Proof state:
α : Type u_1
r : α → α → Prop
a a₁ a₂ : α
h₁ : r a₁ a
h₂ : r a₂ a
⊢ ∀ x' ∈ {a₁, a₂}, r x' a

Tactic:
simp only [insert_eq_cons, mem_cons, mem_singleton, forall_eq_or_imp, forall_eq]

Result:
α : Type u_1
r : α → α → Prop
a a₁ a₂ : α
h₁ : r a₁ a
h₂ : r a₂ a
⊢ r a₁ a ∧ r a₂ a

Proof state:
α : Type u_1
r : α → α → Prop
a a₁ a₂ : α
h₁ : r a₁ a
h₂ : r a₂ a
⊢ r a₁ a ∧ r a₂ a

Tactic:
tauto

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_one (a : Ordinal) : a ⨳ 1 = a

Proof state:
a : Ordinal.{u_1}
⊢ sInf {c | ∀ a' < a, ∀ b' < 1, a' ⨳ 1 ♯ a ⨳ b' < c ♯ a' ⨳ b'} = a

Tactic:
convert csInf_Ici

Result:
case h.e'_2.h.e'_3
a : Ordinal.{u_1}
⊢ {c | ∀ a' < a, ∀ b' < 1, a' ⨳ 1 ♯ a ⨳ b' < c ♯ a' ⨳ b'} = Ici a

Proof state:
a : Ordinal.{u_1}
⊢ a ⨳ 1 = a

Tactic:
rw [nmul]

Result:
a : Ordinal.{u_1}
⊢ sInf {c | ∀ a' < a, ∀ b' < 1, a' ⨳ 1 ♯ a ⨳ b' < c ♯ a' ⨳ b'} = a

Proof state:
case h.e'_2.h.e'_3.h.refine_2
a b : Ordinal.{u_1}
ha : b ∈ Ici a
c : Ordinal.{u_1}
hc : c < a
⊢ ∀ b' < 1, c ⨳ 1 ♯ a ⨳ b' < b ♯ c ⨳ b'

Tactic:
simpa [nmul_one c] using hc.trans_le ha

Result:
no goals

Proof state:
case h.e'_2.h.e'_3.h.refine_1
a b : Ordinal.{u_1}
H : b ∈ {c | ∀ a' < a, ∀ b' < 1, a' ⨳ 1 ♯ a ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < a
⊢ c < b

Tactic:
simpa [nmul_one c] using H c hc

Result:
no goals

Proof state:
case h.e'_2.h.e'_3
a : Ordinal.{u_1}
⊢ {c | ∀ a' < a, ∀ b' < 1, a' ⨳ 1 ♯ a ⨳ b' < c ♯ a' ⨳ b'} = Ici a

Tactic:
ext b

Result:
case h.e'_2.h.e'_3.h
a b : Ordinal.{u_1}
⊢ b ∈ {c | ∀ a' < a, ∀ b' < 1, a' ⨳ 1 ♯ a ⨳ b' < c ♯ a' ⨳ b'} ↔ b ∈ Ici a

Proof state:
case h.e'_2.h.e'_3.h
a b : Ordinal.{u_1}
⊢ b ∈ {c | ∀ a' < a, ∀ b' < 1, a' ⨳ 1 ♯ a ⨳ b' < c ♯ a' ⨳ b'} ↔ b ∈ Ici a

Tactic:
refine ⟨fun H ↦ le_of_forall_lt (a := a) fun c hc ↦ ?_, fun ha c hc ↦ ?_⟩

Result:
case h.e'_2.h.e'_3.h.refine_1
a b : Ordinal.{u_1}
H : b ∈ {c | ∀ a' < a, ∀ b' < 1, a' ⨳ 1 ♯ a ⨳ b' < c ♯ a' ⨳ b'}
c : Ordinal.{u_1}
hc : c < a
⊢ c < b

case h.e'_2.h.e'_3.h.refine_2
a b : Ordinal.{u_1}
ha : b ∈ Ici a
c : Ordinal.{u_1}
hc : c < a
⊢ ∀ b' < 1, c ⨳ 1 ♯ a ⨳ b' < b ♯ c ⨳ b'
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_smul_setAverage (f : α → E) {s : Set α} (h : μ s ≠ ∞) :
    (μ s).toReal • ⨍ x in s, f x ∂μ = ∫ x in s, f x ∂μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s : Set α
h : μ s ≠ ⊤
this : Fact (μ s < ⊤)
⊢ (μ s).toReal • ⨍ (x : α) in s, f x ∂μ = ∫ (x : α) in s, f x ∂μ

Tactic:
rw [← measure_smul_average, restrict_apply_univ]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s : Set α
h : μ s ≠ ⊤
⊢ (μ s).toReal • ⨍ (x : α) in s, f x ∂μ = ∫ (x : α) in s, f x ∂μ

Tactic:
haveI := Fact.mk h.lt_top

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s : Set α
h : μ s ≠ ⊤
this : Fact (μ s < ⊤)
⊢ (μ s).toReal • ⨍ (x : α) in s, f x ∂μ = ∫ (x : α) in s, f x ∂μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_add_emod' (a b : Int) : a / b * b + a % b = a

Proof state:
a b : Int
⊢ b * (a / b) + a % b = a

Tactic:
exact ediv_add_emod ..

Result:
no goals

Proof state:
a b : Int
⊢ a / b * b + a % b = a

Tactic:
rw [Int.mul_comm]

Result:
a b : Int
⊢ b * (a / b) + a % b = a
-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem convs'_succ :
    (of v).convs' (n + 1) = ⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n

Proof state:
case inl.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
a : ℤ
h : fract ↑a = 0
⊢ (of ↑a).convs' (n + 1) = ↑⌊↑a⌋ + 1 / (of (fract ↑a)⁻¹).convs' n

Tactic:
rw [convs'_of_int, fract_intCast, inv_zero, ← cast_zero, convs'_of_int, cast_zero,
  div_zero, add_zero, floor_intCast]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
⊢ (of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n

Tactic:
rcases eq_or_ne (fract v) 0 with h | h

Result:
case inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v = 0
⊢ (of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n

case inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ (of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n

Proof state:
case inl
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v = 0
⊢ (of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n

Tactic:
obtain ⟨a, rfl⟩ : ∃ a : ℤ, v = a := ⟨⌊v⌋, eq_of_sub_eq_zero h⟩

Result:
case inl.intro
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
a : ℤ
h : fract ↑a = 0
⊢ (of ↑a).convs' (n + 1) = ↑⌊↑a⌋ + 1 / (of (fract ↑a)⁻¹).convs' n

Proof state:
case inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ (of v).convs' (n + 1) = ↑⌊v⌋ + 1 / (of (fract v)⁻¹).convs' n

Tactic:
rw [convs', of_h_eq_floor, add_right_inj, convs'Aux_succ_some (of_s_head h)]

Result:
case inr
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.a / ({ a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convs'Aux (of v).s.tail n) =
    1 / (of (fract v)⁻¹).convs' n

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
h : fract v ≠ 0
⊢ { a := 1, b := ↑⌊(fract v)⁻¹⌋ }.b + convs'Aux (of v).s.tail n = (of (fract v)⁻¹).convs' n

Tactic:
rw [convs', of_h_eq_floor, add_right_inj, of_s_tail]

Result:
no goals