harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
lemma contMDiff_of_contMDiff_inr {g : M' → N'}
    (h : ContMDiff I J n ((@Sum.inr N N') ∘ g)) : ContMDiff I J n g

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst✝⁸ : TopologicalSpace M'
inst✝⁷ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝⁴ : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J n (Sum.inr ∘ g)
⊢ ContMDiff I J n g

Tactic:
nontriviality N'

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst✝⁸ : TopologicalSpace M'
inst✝⁷ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝⁴ : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
g : M' → N'
h : ContMDiff I J n (Sum.inr ∘ g)
a✝ : Nontrivial N'
⊢ ContMDiff I J n g

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst✝⁸ : TopologicalSpace M'
inst✝⁷ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝⁴ : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
g : M' → N'
h : ContMDiffOn I J n (Sum.inr ∘ g) univ
a✝ : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun x => default) id
this : aux ∘ Sum.inr ∘ g = g
⊢ univ ⊆ Sum.inr ∘ g ⁻¹' (Sum.inr '' univ)

Tactic:
intro x _hx

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M' : Type u_16
inst✝⁸ : TopologicalSpace M'
inst✝⁷ : ChartedSpace H M'
n : WithTop ℕ∞
E' : Type u_17
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_18
inst✝⁴ : TopologicalSpace H'
J : ModelWithCorners 𝕜 E' H'
N : Type u_20
N' : Type u_21
inst✝³ : TopologicalSpace N
inst✝² : TopologicalSpace N'
inst✝¹ : ChartedSpace H' N
inst✝ : ChartedSpace H' N'
g : M' → N'
h : ContMDiffOn I J n (Sum.inr ∘ g) univ
a✝ : Nontrivial N'
inhabited_h : Inhabited N'
aux : N ⊕ N' → N' := Sum.elim (fun x => default) id
this : aux ∘ Sum.inr ∘ g = g
x : M'
_hx : x ∈ univ
⊢ x ∈ Sum.inr ∘ g ⁻¹' (Sum.inr '' univ)
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem one_eq_closure : (1 : AddSubmonoid R) = closure {1}

Proof state:
R : Type u_4
inst✝ : AddMonoidWithOne R
⊢ AddMonoidHom.mrange (Nat.castAddMonoidHom R) = AddMonoidHom.mrange ((multiplesHom R) 1)

Tactic:
congr 1

Result:
case e_f
R : Type u_4
inst✝ : AddMonoidWithOne R
⊢ Nat.castAddMonoidHom R = (multiplesHom R) 1

Proof state:
case e_f
R : Type u_4
inst✝ : AddMonoidWithOne R
⊢ Nat.castAddMonoidHom R = (multiplesHom R) 1

Tactic:
ext

Result:
case e_f.a
R : Type u_4
inst✝ : AddMonoidWithOne R
⊢ (Nat.castAddMonoidHom R) 1 = ((multiplesHom R) 1) 1

Proof state:
R : Type u_4
inst✝ : AddMonoidWithOne R
⊢ 1 = closure {1}

Tactic:
rw [closure_singleton_eq, one_eq_mrange]

Result:
R : Type u_4
inst✝ : AddMonoidWithOne R
⊢ AddMonoidHom.mrange (Nat.castAddMonoidHom R) = AddMonoidHom.mrange ((multiplesHom R) 1)

Proof state:
case e_f.a
R : Type u_4
inst✝ : AddMonoidWithOne R
⊢ (Nat.castAddMonoidHom R) 1 = ((multiplesHom R) 1) 1

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
@[simp] lemma doubleDualEmb_eq_zero : (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ) = 0 ↔ a = 0

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
a : α
inst✝ : Finite α
⊢ doubleDualEmb a = 0 ↔ a = 0

Tactic:
rw [← map_zero doubleDualEmb, doubleDualEmb_inj]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/CompatibleSheafification.lean
theorem sheafificationWhiskerLeftIso_inv_app (P : Cᵒᵖ ⥤ D) (F : D ⥤ E)
    [∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
    [∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D),
        PreservesLimit (W.index P).multicospan F] :
    (sheafificationWhiskerLeftIso J P).inv.app F = (J.sheafifyCompIso F P).inv

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
P : Cᵒᵖ ⥤ D
F : D ⥤ E
inst✝¹ : ∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
⊢ (𝟙 (J.plusObj (J.plusObj (P ⋙ F))) ≫ J.plusMap (J.plusCompIso F P).inv) ≫ (J.plusCompIso F (J.plusObj P)).inv =
    J.plusMap (J.plusCompIso F P).inv ≫ (J.plusCompIso F (J.plusObj P)).inv

Tactic:
erw [Category.id_comp]

Result:
no goals

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
P : Cᵒᵖ ⥤ D
F : D ⥤ E
inst✝¹ : ∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
⊢ (J.sheafificationWhiskerLeftIso P).inv.app F = (J.sheafifyCompIso F P).inv

Tactic:
dsimp [sheafificationWhiskerLeftIso, sheafifyCompIso]

Result:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w₁
inst✝⁷ : Category.{max v u, w₁} D
E : Type w₂
inst✝⁶ : Category.{max v u, w₂} E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
P : Cᵒᵖ ⥤ D
F : D ⥤ E
inst✝¹ : ∀ (F : D ⥤ E) (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝ : ∀ (F : D ⥤ E) (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
⊢ (𝟙 (J.plusObj (J.plusObj (P ⋙ F))) ≫ J.plusMap (J.plusCompIso F P).inv) ≫ (J.plusCompIso F (J.plusObj P)).inv =
    J.plusMap (J.plusCompIso F P).inv ≫ (J.plusCompIso F (J.plusObj P)).inv
-- Mathlib/Data/ENNReal/Holder.lean
/-- assumes `q ≠ 0` instead of `r ≠ 0`. -/
lemma inv_sub_inv_eq_inv' (hq : q ≠ 0) : r⁻¹ - q⁻¹ = p⁻¹

Proof state:
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
hp : p ≠ 0
⊢ ⊤ + ⊤ = ⊤

Tactic:
simp

Result:
no goals

Proof state:
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
hq : q ≠ 0
⊢ r⁻¹ - q⁻¹ = p⁻¹

Tactic:
obtain (rfl | hr) := eq_zero_or_pos r

Result:
case inl
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
⊢ 0⁻¹ - q⁻¹ = p⁻¹

case inr
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
hq : q ≠ 0
hr : 0 < r
⊢ r⁻¹ - q⁻¹ = p⁻¹

Proof state:
case inl
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
hp : p ≠ 0
⊢ False

Tactic:
have := calc
  0⁻¹ = p⁻¹ + q⁻¹ := inv_eq p q 0
  _ < ⊤ + ⊤ := by simp [hp, hq, pos_iff_ne_zero]
  _ = ⊤ := by simp

Result:
case inl
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
hp : p ≠ 0
this : 0⁻¹ < ⊤
⊢ False

Proof state:
case inl
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
⊢ p = 0

Tactic:
by_contra! hp

Result:
case inl
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
hp : p ≠ 0
⊢ False

Proof state:
case inl
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
hp : p ≠ 0
this : 0⁻¹ < ⊤
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
case inr
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
hq : q ≠ 0
hr : 0 < r
⊢ r⁻¹ - q⁻¹ = p⁻¹

Tactic:
exact inv_sub_inv_eq_inv p q hr.ne'

Result:
no goals

Proof state:
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
this : p = 0
⊢ 0⁻¹ - q⁻¹ = p⁻¹

Tactic:
simpa [this]

Result:
no goals

Proof state:
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
hp : p ≠ 0
⊢ p⁻¹ + q⁻¹ < ⊤ + ⊤

Tactic:
simp [hp, hq, pos_iff_ne_zero]

Result:
no goals

Proof state:
case inl
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
⊢ 0⁻¹ - q⁻¹ = p⁻¹

Tactic:
suffices p = 0 by simpa [this]

Result:
case inl
p q : ℝ≥0∞
hq : q ≠ 0
inst✝ : p.HolderTriple q 0
⊢ p = 0
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsNormal.blsub_eq {f : Ordinal.{u} → Ordinal.{max u v}} (H : IsNormal f) {o : Ordinal.{u}}
    (h : IsLimit o) : (blsub.{_, v} o fun x _ => f x) = f o

Proof state:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : o.IsLimit
⊢ (o.blsub fun x x_1 => f x) = f o

Tactic:
rw [← IsNormal.bsup_eq.{u, v} H h, bsup_eq_blsub_of_lt_succ_limit h]

Result:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : o.IsLimit
⊢ ∀ a < o, f a < f (succ a)

Proof state:
f : Ordinal.{u} → Ordinal.{max u v}
H : IsNormal f
o : Ordinal.{u}
h : o.IsLimit
⊢ ∀ a < o, f a < f (succ a)

Tactic:
exact fun a _ => H.1 a

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem neg_convexOn_iff : ConvexOn 𝕜 s (-f) ↔ ConcaveOn 𝕜 s f

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommGroup β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ ConcaveOn 𝕜 s f → ConvexOn 𝕜 s (-f)

Tactic:
rintro ⟨hconv, h⟩

Result:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommGroup β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
hconv : Convex 𝕜 s
h : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)
⊢ ConvexOn 𝕜 s (-f)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommGroup β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ ConvexOn 𝕜 s (-f) ↔ ConcaveOn 𝕜 s f

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommGroup β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ ConvexOn 𝕜 s (-f) → ConcaveOn 𝕜 s f

case mpr
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommGroup β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ ConcaveOn 𝕜 s f → ConvexOn 𝕜 s (-f)
-- Mathlib/RingTheory/Etale/Kaehler.lean
lemma tensorH1CotangentOfIsLocalization_toLinearMap
    (M : Submonoid S) [IsLocalization M T] :
    (tensorH1CotangentOfIsLocalization R T M).toLinearMap =
      (Algebra.H1Cotangent.map R R S T).liftBaseChange T

Proof state:
R S T : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
⊢ Function.Surjective ⇑fQ

Tactic:
intro x

Result:
R S T : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x✝ : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
x : T
⊢ ∃ a, fQ a = x

Proof state:
R S T : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
⊢ ↑(tensorH1CotangentOfIsLocalization R T M) = LinearMap.liftBaseChange T (H1Cotangent.map R R S T)

Tactic:
ext x : 3

Result:
case a.h.h
R S T : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
⊢ ((AlgebraTensorModule.curry ↑(tensorH1CotangentOfIsLocalization R T M)) 1) x =
    ((AlgebraTensorModule.curry (LinearMap.liftBaseChange T (H1Cotangent.map R R S T))) 1) x
-- Mathlib/Topology/LocallyClosed.lean
/--
A set `s` is locally closed if one of the equivalent conditions below hold
1. It is the intersection of some open set and some closed set.
2. The coborder `(closure s \ s)ᶜ` is open.
3. `s` is closed in some neighborhood of `x` for all `x ∈ s`.
4. Every `x ∈ s` has some open neighborhood `U` such that `U ∩ closure s ⊆ s`.
5. `s` is open in the closure of `s`.
-/
lemma isLocallyClosed_tfae (s : Set X) :
    List.TFAE
    [ IsLocallyClosed s,
      IsOpen (coborder s),
      ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s,
      IsOpen (closure s ↓∩ s)]

Proof state:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen (coborder s)
tfae_2_to_3 : IsOpen (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
tfae_3_to_4 : (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)) → ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s
x✝ : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure s ⊆ s
x : { x // x ∈ closure s }
⊢ x ∈ Subtype.val ⁻¹' ⋃ x, ⋃ (h : x ∈ s), U x h → x ∈ closure s ↓∩ s

Tactic:
rintro ⟨_, ⟨⟨y, rfl⟩, ⟨_, ⟨hy, rfl⟩, hxU⟩⟩⟩

Result:
case refine_1.intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen (coborder s)
tfae_2_to_3 : IsOpen (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
tfae_3_to_4 : (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)) → ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s
x✝ : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU✝ : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure s ⊆ s
x : { x // x ∈ closure s }
y : X
hy : y ∈ s
hxU : ↑x ∈ (fun h => U y h) hy
⊢ x ∈ closure s ↓∩ s
-- Mathlib/Algebra/Group/AddChar.lean
@[simp, norm_cast]
lemma coe_sum (s : Finset ι) (ψ : ι → AddChar A M) : ∑ i ∈ s, ψ i = ∏ i ∈ s, ⇑(ψ i)

Proof state:
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
⊢ ⇑(∑ i ∈ s, ψ i) = ∏ i ∈ s, ⇑(ψ i)

Tactic:
induction s using Finset.cons_induction <;> simp [*]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem measurableSet_region_between_co (hf : Measurable f) (hg : Measurable g)
    (hs : MeasurableSet s) :
    MeasurableSet { p : α × ℝ | p.fst ∈ s ∧ p.snd ∈ Ico (f p.fst) (g p.fst) }

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {a | a.1 ∈ s}

Tactic:
exact measurable_fst hs

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet ({a | a.1 ∈ s} ∩ {a | a.2 ∈ {a_1 | f a.1 ≤ a_1} ∩ {a_1 | a_1 < g a.1}})

Tactic:
refine
  MeasurableSet.inter ?_
    ((measurableSet_le (hf.comp measurable_fst) measurable_snd).inter
      (measurableSet_lt measurable_snd (hg.comp measurable_fst)))

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {a | a.1 ∈ s}

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ico (f p.1) (g p.1)}

Tactic:
dsimp only [regionBetween, Ico, mem_setOf_eq, setOf_and]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet ({a | a.1 ∈ s} ∩ {a | a.2 ∈ {a_1 | f a.1 ≤ a_1} ∩ {a_1 | a_1 < g a.1}})
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
theorem denote_blastArithShiftRight (aig : AIG α) (target : ArbitraryShiftTarget aig w0)
    (lhs : BitVec w0) (rhs : BitVec target.n) (assign : α → Bool)
    (hleft : ∀ (idx : Nat) (hidx : idx < w0), ⟦aig, target.target.get idx hidx, assign⟧ = lhs.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.distance.get idx hidx, assign⟧ = rhs.getLsbD idx) :
    ∀ (idx : Nat) (hidx : idx < w0),
        ⟦
          (blastArithShiftRight aig target).aig,
          (blastArithShiftRight aig target).vec.get idx hidx,
          assign
        ⟧
          =
        (BitVec.sshiftRight' lhs rhs).getLsbD idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w0 : Nat
aig : AIG α
target : aig.ArbitraryShiftTarget w0
lhs : BitVec w0
rhs : BitVec target.n
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w0), ⟦assign, { aig := aig, ref := target.target.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < target.n), ⟦assign, { aig := aig, ref := target.distance.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w0
res : RefVecEntry α w0
hres : blastArithShiftRight aig target = res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs.sshiftRightRec rhs (target.n - 1)).getLsbD idx

Tactic:
rcases target with ⟨n, target, distance⟩

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w0 : Nat
aig : AIG α
lhs : BitVec w0
assign : α → Bool
idx : Nat
hidx : idx < w0
res : RefVecEntry α w0
n : Nat
target : aig.RefVec w0
distance : aig.RefVec n
rhs : BitVec { n := n, target := target, distance := distance }.n
hleft :
  ∀ (idx : Nat) (hidx : idx < w0),
    ⟦assign, { aig := aig, ref := { n := n, target := target, distance := distance }.target.get idx hidx }⟧ =
      lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < { n := n, target := target, distance := distance }.n),
    ⟦assign, { aig := aig, ref := { n := n, target := target, distance := distance }.distance.get idx hidx }⟧ =
      rhs.getLsbD idx
hres : blastArithShiftRight aig { n := n, target := target, distance := distance } = res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    (lhs.sshiftRightRec rhs ({ n := n, target := target, distance := distance }.n - 1)).getLsbD idx
-- Mathlib/Algebra/Group/EvenFunction.lean
/--
If `f` is both even and odd, and its target is a torsion-free commutative additive group,
then `f = 0`.
-/
lemma zero_of_even_and_odd [Neg α] (he : f.Even) (ho : f.Odd) : f = 0

Proof state:
α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : NoZeroSMulDivisors ℕ β
f : α → β
inst✝ : Neg α
he : Function.Even f
ho : Function.Odd f
⊢ f = 0

Tactic:
ext r

Result:
case h
α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : NoZeroSMulDivisors ℕ β
f : α → β
inst✝ : Neg α
he : Function.Even f
ho : Function.Odd f
r : α
⊢ f r = 0 r

Proof state:
case h
α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : NoZeroSMulDivisors ℕ β
f : α → β
inst✝ : Neg α
he : Function.Even f
ho : Function.Odd f
r : α
⊢ f r = 0 r

Tactic:
rw [Pi.zero_apply, ← neg_eq_self ℕ, ← ho, he]

Result:
no goals
-- Mathlib/Analysis/Complex/Schwarz.lean
theorem norm_le_norm_of_mapsTo_ball_self (hd : DifferentiableOn ℂ f (ball 0 R))
    (h_maps : MapsTo f (ball 0 R) (ball 0 R)) (h₀ : f 0 = 0) (hz : ‖z‖ < R) :
    ‖f z‖ ≤ ‖z‖

Proof state:
f : ℂ → ℂ
z : ℂ
R : ℝ
hd : DifferentiableOn ℂ f (ball 0 R)
h_maps : MapsTo f (ball 0 R) (ball 0 R)
h₀ : f 0 = 0
hz : z ∈ ball 0 R
⊢ ‖f z‖ ≤ ‖z‖

Tactic:
simpa only [dist_zero_right] using dist_le_dist_of_mapsTo_ball_self hd h_maps h₀ hz

Result:
no goals

Proof state:
f : ℂ → ℂ
z : ℂ
R : ℝ
hd : DifferentiableOn ℂ f (ball 0 R)
h_maps : MapsTo f (ball 0 R) (ball 0 R)
h₀ : f 0 = 0
hz : ‖z‖ < R
⊢ ‖f z‖ ≤ ‖z‖

Tactic:
replace hz : z ∈ ball (0 : ℂ) R := mem_ball_zero_iff.2 hz

Result:
f : ℂ → ℂ
z : ℂ
R : ℝ
hd : DifferentiableOn ℂ f (ball 0 R)
h_maps : MapsTo f (ball 0 R) (ball 0 R)
h₀ : f 0 = 0
hz : z ∈ ball 0 R
⊢ ‖f z‖ ≤ ‖z‖
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_neg {x : α} (hx : fract x ≠ 0) : fract (-x) = 1 - fract x

Proof state:
case right
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ 1 - fract x < 1 ∧ ∃ z, -x - (1 - fract x) = ↑z

Tactic:
refine ⟨sub_lt_self _ (lt_of_le_of_ne' (fract_nonneg x) hx), -⌊x⌋ - 1, ?_⟩

Result:
case right
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ -x - (1 - fract x) = ↑(-⌊x⌋ - 1)

Proof state:
case right
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ -x + fract x = -↑⌊x⌋

Tactic:
conv in -x => rw [← floor_add_fract x]

Result:
case right
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ -(↑⌊x⌋ + fract x) + fract x = -↑⌊x⌋

Proof state:
case right
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ -x - (1 - fract x) = ↑(-⌊x⌋ - 1)

Tactic:
simp only [sub_sub_eq_add_sub, cast_sub, cast_neg, cast_one, sub_left_inj]

Result:
case right
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ -x + fract x = -↑⌊x⌋

Proof state:
case right
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ -(↑⌊x⌋ + fract x) + fract x = -↑⌊x⌋

Tactic:
simp [-floor_add_fract]

Result:
no goals

Proof state:
case left
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ 0 ≤ 1 - fract x

Tactic:
rw [le_sub_iff_add_le, zero_add]

Result:
case left
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ fract x ≤ 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ 0 ≤ 1 - fract x ∧ 1 - fract x < 1 ∧ ∃ z, -x - (1 - fract x) = ↑z

Tactic:
constructor

Result:
case left
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ 0 ≤ 1 - fract x

case right
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ 1 - fract x < 1 ∧ ∃ z, -x - (1 - fract x) = ↑z

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ fract (-x) = 1 - fract x

Tactic:
rw [fract_eq_iff]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ 0 ≤ 1 - fract x ∧ 1 - fract x < 1 ∧ ∃ z, -x - (1 - fract x) = ↑z

Proof state:
case left
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
x : α
hx : fract x ≠ 0
⊢ fract x ≤ 1

Tactic:
exact (fract_lt_one x).le

Result:
no goals