harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Compactness/Compact.lean
theorem Set.Finite.isCompact_biUnion {s : Set ι} {f : ι → Set X} (hs : s.Finite)
    (hf : ∀ i ∈ s, IsCompact (f i)) : IsCompact (⋃ i ∈ s, f i) :=
  isCompact_iff_ultrafilter_le_nhds'.2 fun l hl => by
    rw [Ultrafilter.finite_biUnion_mem_iff hs] at hl
    rcases hl with ⟨i, his, hi⟩
    rcases (hf i his).ultrafilter_le_nhds _ (le_principal_iff.2 hi) with ⟨x, hxi, hlx⟩
    exact ⟨x, mem_iUnion₂.2 ⟨i, his, hxi⟩, hlx⟩

Proof state:
case intro.intro.intro.intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
i : ι
his : i ∈ s
hi : f i ∈ l
x : X
hxi : x ∈ f i
hlx : ↑l ≤ 𝓝 x
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x

Tactic:
exact ⟨x, mem_iUnion₂.2 ⟨i, his, hxi⟩, hlx⟩

Result:
no goals

Proof state:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
hl : ⋃ i ∈ s, f i ∈ l
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x

Tactic:
rw [Ultrafilter.finite_biUnion_mem_iff hs] at hl

Result:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
hl : ∃ i ∈ s, f i ∈ l
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x

Proof state:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
hl : ∃ i ∈ s, f i ∈ l
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x

Tactic:
rcases hl with ⟨i, his, hi⟩

Result:
case intro.intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
i : ι
his : i ∈ s
hi : f i ∈ l
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x

Proof state:
case intro.intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
i : ι
his : i ∈ s
hi : f i ∈ l
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x

Tactic:
rcases (hf i his).ultrafilter_le_nhds _ (le_principal_iff.2 hi) with ⟨x, hxi, hlx⟩

Result:
case intro.intro.intro.intro
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
i : ι
his : i ∈ s
hi : f i ∈ l
x : X
hxi : x ∈ f i
hlx : ↑l ≤ 𝓝 x
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x
-- Mathlib/FieldTheory/RatFunc/Degree.lean
theorem intDegree_add_le {x y : RatFunc K} (hy : y ≠ 0) (hxy : x + y ≠ 0) :
    intDegree (x + y) ≤ max (intDegree x) (intDegree y)

Proof state:
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ (x + y).intDegree ≤ x.intDegree ⊔ y.intDegree

Tactic:
rw [intDegree_add hxy, ←
  natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree hx y.denom_ne_zero,
  mul_comm y.denom, ←
  natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree hy x.denom_ne_zero,
  le_max_iff, sub_le_sub_iff_right, Int.ofNat_le, sub_le_sub_iff_right, Int.ofNat_le, ←
  le_max_iff, mul_comm y.num]

Result:
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ (x.num * y.denom + x.denom * y.num).natDegree ≤ (x.num * y.denom).natDegree ⊔ (x.denom * y.num).natDegree

Proof state:
case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ (x.num * y.denom + x.denom * y.num).natDegree ≤ (x.num * y.denom).natDegree ⊔ (x.denom * y.num).natDegree

Tactic:
exact natDegree_add_le _ _

Result:
no goals

Proof state:
case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hxy : x + y ≠ 0
hx : x = 0
⊢ (x + y).intDegree ≤ x.intDegree ⊔ y.intDegree

Tactic:
simp only [hx, zero_add, ne_eq] at hxy

Result:
case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hx : x = 0
hxy : ¬y = 0
⊢ (x + y).intDegree ≤ x.intDegree ⊔ y.intDegree

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ (x + y).intDegree ≤ x.intDegree ⊔ y.intDegree

Tactic:
by_cases hx : x = 0

Result:
case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hxy : x + y ≠ 0
hx : x = 0
⊢ (x + y).intDegree ≤ x.intDegree ⊔ y.intDegree

case neg
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ (x + y).intDegree ≤ x.intDegree ⊔ y.intDegree

Proof state:
case pos
K : Type u
inst✝ : Field K
x y : RatFunc K
hy : y ≠ 0
hx : x = 0
hxy : ¬y = 0
⊢ (x + y).intDegree ≤ x.intDegree ⊔ y.intDegree

Tactic:
simp [hx, hxy]

Result:
no goals
-- Mathlib/Analysis/Analytic/Order.lean
/-- The order of an analytic function `f` at `z₀` is zero iff `f` does not vanish at `z₀`. -/
lemma order_eq_zero_iff (hf : AnalyticAt 𝕜 f z₀) :
    hf.order = 0 ↔ f z₀ ≠ 0

Proof state:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • g z) → f z₀ ≠ 0

Tactic:
intro ⟨g, _, _, hg⟩

Result:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
g : 𝕜 → E
left✝¹ : AnalyticAt 𝕜 g z₀
left✝ : g z₀ ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • g z
⊢ f z₀ ≠ 0

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hz : f z₀ ≠ 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • f z

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ hf.order = 0 ↔ f z₀ ≠ 0

Tactic:
rw [← ENat.coe_zero, order_eq_nat_iff hf 0]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • g z) ↔ f z₀ ≠ 0

Proof state:
case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ f z₀ ≠ 0 → ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • g z

Tactic:
exact fun hz ↦ ⟨f, hf, hz, by simp⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • g z) ↔ f z₀ ≠ 0

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • g z) → f z₀ ≠ 0

case mpr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ f z₀ ≠ 0 → ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • g z

Proof state:
case mp
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
g : 𝕜 → E
left✝¹ : AnalyticAt 𝕜 g z₀
left✝ : g z₀ ≠ 0
hg : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ 0 • g z
⊢ f z₀ ≠ 0

Tactic:
simpa [hg.self_of_nhds]

Result:
no goals
-- Mathlib/RingTheory/Extension.lean
@[simp]
lemma Hom.comp_id (f : Hom P P') : f.comp (Hom.id P) = f

Proof state:
case toRingHom.a
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Extension R S
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Extension R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
x✝ : P.Ring
⊢ (f.comp (Hom.id P)).toRingHom x✝ = f.toRingHom x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Extension R S
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Extension R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
⊢ f.comp (Hom.id P) = f

Tactic:
ext

Result:
case toRingHom.a
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Extension R S
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Extension R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
x✝ : P.Ring
⊢ (f.comp (Hom.id P)).toRingHom x✝ = f.toRingHom x✝
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem isIso_of_source_target_iso_zero {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) (j : Y ≅ 0) :
    IsIso f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
i : X ≅ 0
j : Y ≅ 0
⊢ IsIso 0

Tactic:
exact (isIsoZeroEquivIsoZero _ _).invFun ⟨i, j⟩

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
i : X ≅ 0
j : Y ≅ 0
⊢ IsIso f

Tactic:
rw [zero_of_source_iso_zero f i]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
i : X ≅ 0
j : Y ≅ 0
⊢ IsIso 0
-- Mathlib/Order/Filter/Map.lean
theorem le_comap_top (f : α → β) (l : Filter α) : l ≤ comap f ⊤

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Filter α
⊢ l ≤ comap f ⊤

Tactic:
rw [comap_top]

Result:
α : Type u_1
β : Type u_2
f : α → β
l : Filter α
⊢ l ≤ ⊤

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Filter α
⊢ l ≤ ⊤

Tactic:
exact le_top

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffAt.eventually (h : ContDiffAt 𝕜 n f x) (h' : n ≠ ∞) :
    ∀ᶠ y in 𝓝 x, ContDiffAt 𝕜 n f y

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : WithTop ℕ∞
h : ContDiffAt 𝕜 n f x
h' : n ≠ ∞
⊢ ∀ᶠ (y : E) in 𝓝 x, ContDiffAt 𝕜 n f y

Tactic:
simpa [nhdsWithin_univ] using ContDiffWithinAt.eventually h h'

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Exp.lean
theorem exp_of_nilpotent_is_unit {a : A} (h : IsNilpotent a) : IsUnit (exp a)

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
h : IsNilpotent a
h₁ : Commute a (-a)
h₂ : IsNilpotent (-a)
h₃ : 1 = exp a * exp (-a)
⊢ ∃ b, exp a * b = 1 ∧ b * exp a = 1

Tactic:
refine ⟨exp (-a), h₃.symm, ?_⟩

Result:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
h : IsNilpotent a
h₁ : Commute a (-a)
h₂ : IsNilpotent (-a)
h₃ : 1 = exp a * exp (-a)
⊢ exp (-a) * exp a = 1

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
h : IsNilpotent a
⊢ IsUnit (exp a)

Tactic:
have h₁ : Commute a (-a) := Commute.neg_right rfl

Result:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
h : IsNilpotent a
h₁ : Commute a (-a)
⊢ IsUnit (exp a)

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
h : IsNilpotent a
h₁ : Commute a (-a)
h₂ : IsNilpotent (-a)
h₃ : 1 = exp a * exp (-a)
⊢ IsUnit (exp a)

Tactic:
apply isUnit_iff_exists.2

Result:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
h : IsNilpotent a
h₁ : Commute a (-a)
h₂ : IsNilpotent (-a)
h₃ : 1 = exp a * exp (-a)
⊢ ∃ b, exp a * b = 1 ∧ b * exp a = 1

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
h : IsNilpotent a
h₁ : Commute a (-a)
h₂ : IsNilpotent (-a)
h₃ : exp (a + -a) = exp a * exp (-a)
⊢ IsUnit (exp a)

Tactic:
rw [add_neg_cancel a, exp_zero_eq_one] at h₃

Result:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
h : IsNilpotent a
h₁ : Commute a (-a)
h₂ : IsNilpotent (-a)
h₃ : 1 = exp a * exp (-a)
⊢ IsUnit (exp a)

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
h : IsNilpotent a
h₁ : Commute a (-a)
h₂ : IsNilpotent (-a)
⊢ IsUnit (exp a)

Tactic:
have h₃ := exp_add_of_commute h₁ h h₂

Result:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
h : IsNilpotent a
h₁ : Commute a (-a)
h₂ : IsNilpotent (-a)
h₃ : exp (a + -a) = exp a * exp (-a)
⊢ IsUnit (exp a)

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
h : IsNilpotent a
h₁ : Commute a (-a)
⊢ IsUnit (exp a)

Tactic:
have h₂ : IsNilpotent (-a) := IsNilpotent.neg h

Result:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
h : IsNilpotent a
h₁ : Commute a (-a)
h₂ : IsNilpotent (-a)
⊢ IsUnit (exp a)

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
a : A
h : IsNilpotent a
h₁ : Commute a (-a)
h₂ : IsNilpotent (-a)
h₃ : 1 = exp a * exp (-a)
⊢ exp (-a) * exp a = 1

Tactic:
rw [← exp_add_of_commute h₁.symm h₂ h, neg_add_cancel a, exp_zero_eq_one]

Result:
no goals
-- Mathlib/Analysis/Complex/Isometry.lean
theorem linearEquiv_det_rotation (a : Circle) : LinearEquiv.det (rotation a).toLinearEquiv = 1

Proof state:
a : Circle
⊢ LinearEquiv.det (rotation a).toLinearEquiv = 1

Tactic:
rw [← Units.eq_iff, LinearEquiv.coe_det, det_rotation, Units.val_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_zero : Int.bmod 0 m = 0

Proof state:
m✝ m : Nat
h : ↑m / 2 + 2 / 2 ≤ 0
⊢ 2 ≠ 0

m✝ m : Nat
h : (↑m + (1 + 1)) / 2 ≤ 0
⊢ 2 ∣ 1 + 1

Tactic:
all_goals decide

Result:
no goals

Proof state:
m✝ m : Nat
h : ↑m / 2 + 2 / 2 ≤ 0
⊢ False

m✝ m : Nat
h : (↑m + (1 + 1)) / 2 ≤ 0
⊢ 2 ∣ 1 + 1

Tactic:
rw [Int.ediv_self, ← ofNat_two, ← ofNat_ediv, add_one_le_iff, ← @Int.not_le] at h

Result:
m✝ m : Nat
h : ¬0 ≤ ↑(m / 2)
⊢ False

m✝ m : Nat
h : ↑m / 2 + 2 / 2 ≤ 0
⊢ 2 ≠ 0

m✝ m : Nat
h : (↑m + (1 + 1)) / 2 ≤ 0
⊢ 2 ∣ 1 + 1

Proof state:
m : Nat
h : (↑0 + 1) / 2 ≤ 0
⊢ ↑0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
m✝ m : Nat
h : ↑m / 2 + (1 + 1) / 2 ≤ 0
⊢ False

m✝ m : Nat
h : (↑m + (1 + 1)) / 2 ≤ 0
⊢ 2 ∣ 1 + 1

Tactic:
change _ + 2 / 2 ≤ 0 at h

Result:
m✝ m : Nat
h : ↑m / 2 + 2 / 2 ≤ 0
⊢ False

m✝ m : Nat
h : (↑m + (1 + 1)) / 2 ≤ 0
⊢ 2 ∣ 1 + 1

Proof state:
m✝ m : Nat
h : (↑(m + 1) + 1) / 2 ≤ 0
⊢ ↑(m + 1) = 0

Tactic:
exfalso

Result:
m✝ m : Nat
h : (↑(m + 1) + 1) / 2 ≤ 0
⊢ False

Proof state:
m✝ m : Nat
h : (↑(m + 1) + 1) / 2 ≤ 0
⊢ False

Tactic:
rw [natCast_add, ofNat_one, Int.add_assoc, add_ediv_of_dvd_right] at h

Result:
m✝ m : Nat
h : ↑m / 2 + (1 + 1) / 2 ≤ 0
⊢ False

m✝ m : Nat
h : (↑m + (1 + 1)) / 2 ≤ 0
⊢ 2 ∣ 1 + 1

Proof state:
m : Nat
h : ¬0 < (↑m + 1) / 2
⊢ ↑m = 0

Tactic:
rw [@Int.not_lt] at h

Result:
m : Nat
h : (↑m + 1) / 2 ≤ 0
⊢ ↑m = 0

Proof state:
m : Nat
h : (↑m + 1) / 2 ≤ 0
⊢ ↑m = 0

Tactic:
match m with
| 0 => rfl
| (m+1) =>
  exfalso
  rw [natCast_add, ofNat_one, Int.add_assoc, add_ediv_of_dvd_right] at h
  change _ + 2 / 2 ≤ 0 at h
  rw [Int.ediv_self, ← ofNat_two, ← ofNat_ediv, add_one_le_iff, ← @Int.not_le] at h
  exact h (ofNat_nonneg _)
  all_goals decide

Result:
no goals

Proof state:
m✝ m : Nat
h : (↑m + (1 + 1)) / 2 ≤ 0
⊢ 2 ∣ 1 + 1

Tactic:
decide

Result:
no goals

Proof state:
m : Nat
⊢ bmod 0 m = 0

Tactic:
dsimp [bmod]

Result:
m : Nat
⊢ (if 0 < (↑m + 1) / 2 then 0 else 0 - ↑m) = 0

Proof state:
m : Nat
⊢ ¬0 < (↑m + 1) / 2 → ↑m = 0

Tactic:
intro h

Result:
m : Nat
h : ¬0 < (↑m + 1) / 2
⊢ ↑m = 0

Proof state:
m✝ m : Nat
h : ¬0 ≤ ↑(m / 2)
⊢ False

m✝ m : Nat
h : ↑m / 2 + 2 / 2 ≤ 0
⊢ 2 ≠ 0

m✝ m : Nat
h : (↑m + (1 + 1)) / 2 ≤ 0
⊢ 2 ∣ 1 + 1

Tactic:
exact h (ofNat_nonneg _)

Result:
m✝ m : Nat
h : ↑m / 2 + 2 / 2 ≤ 0
⊢ 2 ≠ 0

m✝ m : Nat
h : (↑m + (1 + 1)) / 2 ≤ 0
⊢ 2 ∣ 1 + 1

Proof state:
m : Nat
⊢ (if 0 < (↑m + 1) / 2 then 0 else 0 - ↑m) = 0

Tactic:
simp only [Int.zero_sub, ite_eq_left_iff, Int.neg_eq_zero]

Result:
m : Nat
⊢ ¬0 < (↑m + 1) / 2 → ↑m = 0
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem closure_eq_iInter_cthickening (E : Set α) :
    closure E = ⋂ (δ : ℝ) (_ : 0 < δ), cthickening δ E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
⊢ cthickening 0 E = ⋂ δ, ⋂ (_ : 0 < δ), cthickening δ E

Tactic:
exact cthickening_eq_iInter_cthickening E

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
⊢ closure E = ⋂ δ, ⋂ (_ : 0 < δ), cthickening δ E

Tactic:
rw [← cthickening_zero]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
⊢ cthickening 0 E = ⋂ δ, ⋂ (_ : 0 < δ), cthickening δ E
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_eq_zero (hs : Absorbent ℝ s) (hb : Bornology.IsVonNBounded ℝ s) :
    gauge s x = 0 ↔ x = 0

Proof state:
case intro.intro
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
h₀ : gauge s x = 0
hne : x ≠ 0
this : {x}ᶜ ∈ comap (gauge s) (𝓝 0)
r : ℝ
hr₀ : 0 < r
hr : gauge s ⁻¹' {b | |b| < r} ⊆ {x}ᶜ
⊢ False

Tactic:
exact hr (by simpa [h₀]) rfl

Result:
no goals

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
h₀ : gauge s x = 0
hne : x ≠ 0
this : {x}ᶜ ∈ comap (gauge s) (𝓝 0)
r : ℝ
hr₀ : 0 < r
hr : gauge s ⁻¹' {b | |b| < r} ⊆ {x}ᶜ
⊢ x ∈ gauge s ⁻¹' {b | |b| < r}

Tactic:
simpa [h₀]

Result:
no goals

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
h₀ : gauge s x = 0
hne : x ≠ 0
this : {x}ᶜ ∈ comap (gauge s) (𝓝 0)
⊢ False

Tactic:
rcases ((nhds_basis_zero_abs_sub_lt _).comap _).mem_iff.1 this with ⟨r, hr₀, hr⟩

Result:
case intro.intro
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
h₀ : gauge s x = 0
hne : x ≠ 0
this : {x}ᶜ ∈ comap (gauge s) (𝓝 0)
r : ℝ
hr₀ : 0 < r
hr : gauge s ⁻¹' {b | |b| < r} ⊆ {x}ᶜ
⊢ False

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
⊢ gauge s x = 0 ↔ x = 0

Tactic:
refine ⟨fun h₀ ↦ by_contra fun (hne : x ≠ 0) ↦ ?_, fun h ↦ h.symm ▸ gauge_zero⟩

Result:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
h₀ : gauge s x = 0
hne : x ≠ 0
⊢ False

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
h₀ : gauge s x = 0
hne : x ≠ 0
⊢ False

Tactic:
have : {x}ᶜ ∈ comap (gauge s) (𝓝 0) :=
  comap_gauge_nhds_zero_le hs hb (isOpen_compl_singleton.mem_nhds hne.symm)

Result:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
hs : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
h₀ : gauge s x = 0
hne : x ≠ 0
this : {x}ᶜ ∈ comap (gauge s) (𝓝 0)
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zip_map' (f : α → β) (g : α → γ) :
    ∀ l : List α, zip (l.map f) (l.map g) = l.map fun a => (f a, g a)
  | [] => rfl
  | a :: l => by simp only [map, zip_cons_cons, zip_map']

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
a : α
l : List α
⊢ (map f (a :: l)).zip (map g (a :: l)) = map (fun a => (f a, g a)) (a :: l)

Tactic:
simp only [map, zip_cons_cons, zip_map']

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem map_sum_finset_aux [DecidableEq ι] [Fintype ι] {n : ℕ} (h : (∑ i, #(A i)) = n) :
    (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)

Proof state:
case neg.h
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i => Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i : ι, #(A i) = m → (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), A i ≠ ∅
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC : (fun i => ∑ j ∈ A i, g i j) = update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)
Beq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i => ∑ j ∈ B i, g i j
Ceq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i => ∑ j ∈ C i, g i j
Brec : (f fun i => ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i => g i (r i)
Crec : (f fun i => ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i => g i (r i)
D : Disjoint (piFinset B) (piFinset C)
r : (a : ι) → α a
hr : r ∈ piFinset A
hri₀ : ¬r i₀ = j₂
⊢ r ∈ piFinset B

Tactic:
refine mem_piFinset.2 fun i => ?_

Result:
case neg.h
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i => Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i : ι, #(A i) = m → (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i : ι, #(A i) = n
Ai_empty : ∀ (i : ι), A i ≠ ∅
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC : (fun i => ∑ j ∈ A i, g i j) = update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)
Beq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i => ∑ j ∈ B i, g i j
Ceq : update (fun i => ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i => ∑ j ∈ C i, g i j
Brec : (f fun i => ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i => g i (r i)
Crec : (f fun i => ∑ j ∈ C i, g i j) = ∑ r ∈ piFinset C, f fun i => g i (r i)
D : Disjoint (piFinset B) (piFinset C)
r : (a : ι) → α a
hr : r ∈ piFinset A
hri₀ : ¬r i₀ = j₂
i : ι
⊢ r i ∈ B i