harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/LocalProperties/IntegrallyClosed.lean
theorem IsIntegrallyClosed.of_localization_maximal {R : Type*} [CommRing R] [IsDomain R]
    (h : ∀ p : Ideal R, p ≠ ⊥ → [p.IsMaximal] → IsIntegrallyClosed (Localization.AtPrime p)) :
    IsIntegrallyClosed R

Proof state:
case neg.mk
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : FractionRing R
x : R × ↥R⁰
hx : IsIntegral R (Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x)
I : Ideal R := span {↑x.2} / span {x.1}
⊢ ∃ y, (algebraMap R (FractionRing R)) y = Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x

Tactic:
have h1 : 1 ∈ I := by
  apply I.eq_top_iff_one.mp
  by_contra hn
  rcases I.exists_le_maximal hn with ⟨p, hpm, hpi⟩
  have hic := h p (Ring.ne_bot_of_isMaximal_of_not_isField hpm hf)
  have hxp : IsIntegral (Localization.AtPrime p) (mk x.1 x.2) := hx.tower_top
  
  rcases (isIntegrallyClosed_iff (FractionRing R)).mp hic hxp with ⟨⟨y⟩, hy⟩
  
  have hyi : y.2.1 ∈ I := by
    intro a ha
    rcases mem_span_singleton'.mp ha with ⟨b, hb⟩
    apply mem_span_singleton'.mpr ⟨b * y.1, _⟩
    rw [← hb, ← mul_assoc, mul_comm y.2.1 b, mul_assoc, mul_assoc]
    exact congrArg (HMul.hMul b) <| (mul_comm y.1 x.2.1).trans <|
      FaithfulSMul.algebraMap_injective R (Localization R⁰) <| mk'_eq_iff_eq.mp <|
        (mk'_eq_algebraMap_mk'_of_submonoid_le _ _ p.primeCompl_le_nonZeroDivisors y.1 y.2).trans
          <| show algebraMap (Localization.AtPrime p) _ (mk' _ y.1 y.2) = mk' _ x.1 x.2
            by simpa only [← mk_eq_mk', ← hy] using by rfl
  exact y.2.2 (hpi hyi)

Result:
case neg.mk
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : FractionRing R
x : R × ↥R⁰
hx : IsIntegral R (Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x)
I : Ideal R := span {↑x.2} / span {x.1}
h1 : 1 ∈ I
⊢ ∃ y, (algebraMap R (FractionRing R)) y = Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : FractionRing R
x : R × ↥R⁰
hx : IsIntegral R (Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x)
I : Ideal R := span {↑x.2} / span {x.1}
⊢ I = ⊤

Tactic:
by_contra hn

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst : p.IsMaximal], IsIntegrallyClosed (Localization.AtPrime p)
hf : ¬IsField R
x✝ : FractionRing R
x : R × ↥R⁰
hx : IsIntegral R (Quot.mk (⇑(OreLocalization.oreEqv R⁰ R)) x)
I : Ideal R := span {↑x.2} / span {x.1}
hn : ¬I = ⊤
⊢ False
-- Mathlib/MeasureTheory/SetAlgebra.lean
theorem countable_generateSetAlgebra (h : 𝒜.Countable) :
    (generateSetAlgebra 𝒜).Countable

Proof state:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
⊢ (generateSetAlgebra 𝒜).Countable

Tactic:
let f : Set (Set (Set α)) → Set α := fun A ↦ ⋃ a ∈ A, ⋂ t ∈ a, t

Result:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun A => ⋃ a ∈ A, ⋂ t ∈ a, t
⊢ (generateSetAlgebra 𝒜).Countable

Proof state:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun A => ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a | a.Finite ∧ a ⊆ ℬ}
count_𝒞 : 𝒞.Countable
𝒟 : Set (Set (Set (Set α))) := {A | A.Finite ∧ A ⊆ 𝒞}
count_𝒟 : 𝒟.Countable
this : generateSetAlgebra 𝒜 ⊆ f '' 𝒟
⊢ (generateSetAlgebra 𝒜).Countable

Tactic:
exact (count_𝒟.image f).mono this

Result:
no goals

Proof state:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}
⊢ compl '' 𝒜 = {s | sᶜ ∈ 𝒜}

Tactic:
ext s

Result:
case h
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}
s : Set α
⊢ s ∈ compl '' 𝒜 ↔ s ∈ {s | sᶜ ∈ 𝒜}

Proof state:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun A => ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a | a.Finite ∧ a ⊆ ℬ}
⊢ (generateSetAlgebra 𝒜).Countable

Tactic:
have count_𝒞 : 𝒞.Countable := countable_setOf_finite_subset (countable_coe_iff.1 count_ℬ)

Result:
α : Type u_1
𝒜 : Set (Set α)
h : 𝒜.Countable
ℬ : Set (Set α) := {s | s ∈ 𝒜} ∪ {s | sᶜ ∈ 𝒜}
count_ℬ : ℬ.Countable
f : Set (Set (Set α)) → Set α := fun A => ⋃ a ∈ A, ⋂ t ∈ a, t
𝒞 : Set (Set (Set α)) := {a | a.Finite ∧ a ⊆ ℬ}
count_𝒞 : 𝒞.Countable
⊢ (generateSetAlgebra 𝒜).Countable
-- Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
theorem balancedCoreAux_maximal (h : t ⊆ s) (ht : Balanced 𝕜 t) : t ⊆ balancedCoreAux 𝕜 s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ x ∈ r • s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ (norm_pos_iff.mp <| zero_lt_one.trans_le hr)]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ r⁻¹ • x ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ ‖r⁻¹‖ ≤ 1

Tactic:
rw [norm_inv]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ ‖r‖⁻¹ ≤ 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
⊢ t ⊆ balancedCoreAux 𝕜 s

Tactic:
refine fun x hx => mem_balancedCoreAux_iff.2 fun r hr => ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ x ∈ r • s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ ‖r‖⁻¹ ≤ 1

Tactic:
exact inv_le_one_of_one_le₀ hr

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ r⁻¹ • x ∈ s

Tactic:
refine h (ht.smul_mem ?_ hx)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ ‖r⁻¹‖ ≤ 1
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem MonoidHom.map_cyclic [h : IsCyclic G] (σ : G →* G) :
    ∃ m : ℤ, ∀ g : G, σ g = g ^ m

Proof state:
case intro.intro.intro
G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x => h ^ x) m = σ h
n : ℤ
⊢ σ ((fun x => h ^ x) n) = (fun x => h ^ x) n ^ m

Tactic:
rw [MonoidHom.map_zpow, ← hm, ← zpow_mul, ← zpow_mul']

Result:
no goals

Proof state:
case intro
G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
⊢ ∃ m, ∀ (g : G), σ g = g ^ m

Tactic:
obtain ⟨m, hm⟩ := hG (σ h)

Result:
case intro.intro
G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x => h ^ x) m = σ h
⊢ ∃ m, ∀ (g : G), σ g = g ^ m

Proof state:
case intro.intro
G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x => h ^ x) m = σ h
g : G
⊢ σ g = g ^ m

Tactic:
obtain ⟨n, rfl⟩ := hG g

Result:
case intro.intro.intro
G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x => h ^ x) m = σ h
n : ℤ
⊢ σ ((fun x => h ^ x) n) = (fun x => h ^ x) n ^ m

Proof state:
G : Type u_2
inst✝ : Group G
h : IsCyclic G
σ : G →* G
⊢ ∃ m, ∀ (g : G), σ g = g ^ m

Tactic:
obtain ⟨h, hG⟩ := IsCyclic.exists_generator (α := G)

Result:
case intro
G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
⊢ ∃ m, ∀ (g : G), σ g = g ^ m

Proof state:
case intro.intro
G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x => h ^ x) m = σ h
⊢ ∃ m, ∀ (g : G), σ g = g ^ m

Tactic:
refine ⟨m, fun g => ?_⟩

Result:
case intro.intro
G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x => h ^ x) m = σ h
g : G
⊢ σ g = g ^ m
-- Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
theorem IsLocalDiffeomorph.isLocalHomeomorph (hf : IsLocalDiffeomorph I J n f) :
    IsLocalHomeomorph f

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
hf : IsLocalDiffeomorphOn I J n f univ
⊢ IsLocalHomeomorphOn f univ

Tactic:
exact hf.isLocalHomeomorphOn

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
hf : IsLocalDiffeomorph I J n f
⊢ IsLocalHomeomorph f

Tactic:
rw [isLocalHomeomorph_iff_isLocalHomeomorphOn_univ]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
hf : IsLocalDiffeomorph I J n f
⊢ IsLocalHomeomorphOn f univ

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
hf : IsLocalDiffeomorph I J n f
⊢ IsLocalHomeomorphOn f univ

Tactic:
rw [isLocalDiffeomorph_iff_isLocalDiffeomorphOn_univ] at hf

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
hf : IsLocalDiffeomorphOn I J n f univ
⊢ IsLocalHomeomorphOn f univ
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- Functional equation for the even Hurwitz zeta function. -/
lemma completedHurwitzZetaEven_one_sub (a : UnitAddCircle) (s : ℂ) :
    completedHurwitzZetaEven a (1 - s) = completedCosZeta a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven a (1 - s) = completedCosZeta a s

Tactic:
rw [completedHurwitzZetaEven, completedCosZeta, sub_div,
  (by norm_num : (1 / 2 : ℂ) = ↑(1 / 2 : ℝ)),
  (by rfl : (1 / 2 : ℝ) = (hurwitzEvenFEPair a).k),
  (hurwitzEvenFEPair a).functional_equation (s / 2),
  (by rfl : (hurwitzEvenFEPair a).ε = 1),
  one_smul]

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
⊢ 1 / 2 = ↑(1 / 2)

Tactic:
norm_num

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).ε = 1

Tactic:
rfl

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
⊢ 1 / 2 = (hurwitzEvenFEPair a).k

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem split_of_not_mem_Ioo (h : x ∉ Ioo (I.lower i) (I.upper i)) : split I i x = ⊤

Proof state:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split J i x).boxes

Tactic:
clear hJ

Result:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
⊢ J ∈ (split J i x).boxes

Proof state:
case inl.h
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ J.lower i
⊢ ↑J = J.splitUpper i x

Tactic:
rwa [eq_comm, Box.splitUpper_eq_self]

Result:
no goals

Proof state:
case inr.h
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : J.upper i ≤ x
⊢ ↑J = J.splitLower i x

Tactic:
rwa [eq_comm, Box.splitLower_eq_self]

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ∉ Ioo (I.lower i) (I.upper i)
⊢ split I i x = ⊤

Tactic:
refine ((isPartitionTop I).eq_of_boxes_subset fun J hJ => ?_).symm

Result:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ∉ Ioo (I.lower i) (I.upper i)
J : Box ι
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split I i x).boxes

Proof state:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ≤ J.lower i ∨ J.upper i ≤ x
⊢ ↑J = J.splitLower i x ∨ ↑J = J.splitUpper i x

Tactic:
cases h <;> [right; left]

Result:
case inl.h
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ J.lower i
⊢ ↑J = J.splitUpper i x

case inr.h
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h✝ : J.upper i ≤ x
⊢ ↑J = J.splitLower i x

Proof state:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
⊢ ↑J = J.splitLower i x ∨ ↑J = J.splitUpper i x

Tactic:
rw [mem_Ioo, not_and_or, not_lt, not_lt] at h

Result:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ≤ J.lower i ∨ J.upper i ≤ x
⊢ ↑J = J.splitLower i x ∨ ↑J = J.splitUpper i x

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
h : x ∉ Ioo (I.lower i) (I.upper i)
J : Box ι
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split I i x).boxes

Tactic:
rcases mem_top.1 hJ with rfl

Result:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split J i x).boxes

Proof state:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
⊢ J ∈ (split J i x).boxes

Tactic:
rw [mem_boxes, mem_split_iff]

Result:
ι : Type u_1
i : ι
x : ℝ
J : Box ι
h : x ∉ Ioo (J.lower i) (J.upper i)
⊢ ↑J = J.splitLower i x ∨ ↑J = J.splitUpper i x
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma compls_infs (s t : Finset α) : (s ⊼ t)ᶜˢ = sᶜˢ ⊻ tᶜˢ

Proof state:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ image compl (s ⊼ t) = image compl s ⊻ image compl t

Tactic:
exact image_image₂_distrib fun _ _ ↦ compl_inf

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ⊼ t)ᶜˢ = sᶜˢ ⊻ tᶜˢ

Tactic:
simp_rw [← image_compl]

Result:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ image compl (s ⊼ t) = image compl s ⊻ image compl t
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
protected lemma GrowsPolynomially.inv {f : ℝ → ℝ} (hf : GrowsPolynomially f) :
    GrowsPolynomially fun x => (f x)⁻¹

Proof state:
f : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf✝ : GrowsPolynomially fun x => |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x|) u ∈ Set.Icc (c₁ * (fun x => |f x|) x) (c₂ * (fun x => |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
⊢ f u ≠ 0

Tactic:
exact hx'' u hu.1

Result:
no goals

Proof state:
case hba
f : ℝ → ℝ
hf✝¹ : GrowsPolynomially f
hf_pos_or_neg : (∀ᶠ (x : ℝ) in atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in atTop, f x < 0
hf' : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
hf✝ : GrowsPolynomially fun x => |f x|
b : ℝ
hb : b ∈ Set.Ioo 0 1
hb_pos : 0 < b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hf :
  ∀ᶠ (x : ℝ) in atTop,
    ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x|) u ∈ Set.Icc (c₁ * (fun x => |f x|) x) (c₂ * (fun x => |f x|) x)
x : ℝ
hx : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)
hx' : f x ≠ 0
hx'' : ∀ (y : ℝ), b * id x ≤ y → f y ≠ 0
u : ℝ
hu : u ∈ Set.Icc (b * x) x
h₁ : 0 < |f u|
⊢ |f u| ≤ c₂ * |f x|

Tactic:
exact (hx u hu).2

Result:
no goals
-- Mathlib/ModelTheory/Order.lean
lemma monotone [Preorder M] [L.OrderedStructure M] [Preorder N] [L.OrderedStructure N] (f : F) :
    Monotone f := fun a b => by
  have h := HomClass.map_rel f leSymb ![a,b]
  simp only [relMap_leSymb, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
    Matrix.head_cons, Function.comp_apply] at h
  exact h

Proof state:
L : Language
M : Type w'
inst✝⁸ : L.IsOrdered
inst✝⁷ : L.Structure M
N : Type u_1
inst✝⁶ : L.Structure N
F : Type u_2
inst✝⁵ : FunLike F M N
inst✝⁴ : L.HomClass F M N
inst✝³ : Preorder M
inst✝² : L.OrderedStructure M
inst✝¹ : Preorder N
inst✝ : L.OrderedStructure N
f : F
a b : M
h : RelMap leSymb ![a, b] → RelMap leSymb (⇑f ∘ ![a, b])
⊢ a ≤ b → f a ≤ f b

Tactic:
simp only [relMap_leSymb, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
  Matrix.head_cons, Function.comp_apply] at h

Result:
L : Language
M : Type w'
inst✝⁸ : L.IsOrdered
inst✝⁷ : L.Structure M
N : Type u_1
inst✝⁶ : L.Structure N
F : Type u_2
inst✝⁵ : FunLike F M N
inst✝⁴ : L.HomClass F M N
inst✝³ : Preorder M
inst✝² : L.OrderedStructure M
inst✝¹ : Preorder N
inst✝ : L.OrderedStructure N
f : F
a b : M
h : a ≤ b → f a ≤ f b
⊢ a ≤ b → f a ≤ f b

Proof state:
L : Language
M : Type w'
inst✝⁸ : L.IsOrdered
inst✝⁷ : L.Structure M
N : Type u_1
inst✝⁶ : L.Structure N
F : Type u_2
inst✝⁵ : FunLike F M N
inst✝⁴ : L.HomClass F M N
inst✝³ : Preorder M
inst✝² : L.OrderedStructure M
inst✝¹ : Preorder N
inst✝ : L.OrderedStructure N
f : F
a b : M
h : a ≤ b → f a ≤ f b
⊢ a ≤ b → f a ≤ f b

Tactic:
exact h

Result:
no goals

Proof state:
L : Language
M : Type w'
inst✝⁸ : L.IsOrdered
inst✝⁷ : L.Structure M
N : Type u_1
inst✝⁶ : L.Structure N
F : Type u_2
inst✝⁵ : FunLike F M N
inst✝⁴ : L.HomClass F M N
inst✝³ : Preorder M
inst✝² : L.OrderedStructure M
inst✝¹ : Preorder N
inst✝ : L.OrderedStructure N
f : F
a b : M
⊢ a ≤ b → f a ≤ f b

Tactic:
have h := HomClass.map_rel f leSymb ![a,b]

Result:
L : Language
M : Type w'
inst✝⁸ : L.IsOrdered
inst✝⁷ : L.Structure M
N : Type u_1
inst✝⁶ : L.Structure N
F : Type u_2
inst✝⁵ : FunLike F M N
inst✝⁴ : L.HomClass F M N
inst✝³ : Preorder M
inst✝² : L.OrderedStructure M
inst✝¹ : Preorder N
inst✝ : L.OrderedStructure N
f : F
a b : M
h : RelMap leSymb ![a, b] → RelMap leSymb (⇑f ∘ ![a, b])
⊢ a ≤ b → f a ≤ f b
-- Mathlib/RingTheory/Ideal/Maps.lean
lemma ker_comp_of_injective [Semiring T] (g : T →+* R) {f : R →+* S} (hf : Function.Injective f) :
    ker (f.comp g) = RingHom.ker g

Proof state:
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : Semiring T
g : T →+* R
f : R →+* S
hf : Function.Injective ⇑f
⊢ ker (f.comp g) = ker g

Tactic:
rw [← RingHom.comap_ker, (injective_iff_ker_eq_bot f).mp hf, RingHom.ker]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Basic.lean
theorem flip_flip_aux (A : BilinForm R M) :
    flipHomAux (M := M) (flipHomAux (M := M) A) = A

Proof state:
case H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A✝ : BilinForm R M
A y✝ : M
⊢ ((flipHomAux (flipHomAux A✝)) A) y✝ = (A✝ A) y✝

Tactic:
simp [flipHomAux]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : BilinForm R M
⊢ flipHomAux (flipHomAux A) = A

Tactic:
ext A

Result:
case H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A✝ : BilinForm R M
A y✝ : M
⊢ ((flipHomAux (flipHomAux A✝)) A) y✝ = (A✝ A) y✝
-- Mathlib/Data/Nat/ModEq.lean
theorem mul_left' (c : ℕ) (h : a ≡ b [MOD n]) : c * a ≡ c * b [MOD c * n]

Proof state:
n a b c : ℕ
h : a ≡ b [MOD n]
⊢ c * a ≡ c * b [MOD c * n]

Tactic:
unfold ModEq at *

Result:
n a b c : ℕ
h : a % n = b % n
⊢ c * a % (c * n) = c * b % (c * n)

Proof state:
n a b c : ℕ
h : a % n = b % n
⊢ c * a % (c * n) = c * b % (c * n)

Tactic:
rw [mul_mod_mul_left, mul_mod_mul_left, h]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem summable_of_sum_range_le {f : ℕ → ℝ≥0} {c : ℝ≥0}
    (h : ∀ n, ∑ i ∈ Finset.range n, f i ≤ c) : Summable f

Proof state:
f : ℕ → ℝ≥0
c : ℝ≥0
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c
⊢ Summable f

Tactic:
refine summable_iff_not_tendsto_nat_atTop.2 fun H => ?_

Result:
f : ℕ → ℝ≥0
c : ℝ≥0
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c
H : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop
⊢ False

Proof state:
f : ℕ → ℝ≥0
c : ℝ≥0
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c
H : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop
⊢ False

Tactic:
rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩

Result:
case intro.intro
f : ℕ → ℝ≥0
c : ℝ≥0
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c
H : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop
n : ℕ
hn : c < ∑ i ∈ Finset.range n, f i
⊢ False

Proof state:
case intro.intro
f : ℕ → ℝ≥0
c : ℝ≥0
h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c
H : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop
n : ℕ
hn : c < ∑ i ∈ Finset.range n, f i
⊢ False

Tactic:
exact lt_irrefl _ (hn.trans_le (h n))

Result:
no goals