harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem HasProd.nat_mul_neg {f : ℤ → M} (hf : HasProd f m) :
    HasProd (fun n : ℕ ↦ f n * f (-n)) (m * f 0)

Proof state:
case e_a.refine_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x => ↑x) v'
u2 : Finset ℤ := image (fun x => -↑x) v'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : (∃ a ∈ v', ↑a = x) ∧ ∃ a ∈ v', -↑a = x
⊢ f x = if x = 0 then f 0 else 1

Tactic:
suffices x = 0 by simp only [this, eq_self_iff_true, if_true]

Result:
case e_a.refine_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x => ↑x) v'
u2 : Finset ℤ := image (fun x => -↑x) v'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : (∃ a ∈ v', ↑a = x) ∧ ∃ a ∈ v', -↑a = x
⊢ x = 0

Proof state:
case inl
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x => ↑x) v'
u2 : Finset ℤ := image (fun x => -↑x) v'
x : ℤ
hx : x ∈ u
h'x : 0 ≤ x
⊢ ↑x.natAbs = x

Tactic:
simp only [Int.natCast_natAbs, abs_eq_self, h'x]

Result:
no goals

Proof state:
case inr
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x => ↑x) v'
u2 : Finset ℤ := image (fun x => -↑x) v'
x : ℤ
hx : x ∈ u
h'x : x ≤ 0
⊢ (∃ a ∈ v', ↑a = x) ∨ ∃ a ∈ v', -↑a = x

Tactic:
refine Or.inr ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩

Result:
case inr
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x => ↑x) v'
u2 : Finset ℤ := image (fun x => -↑x) v'
x : ℤ
hx : x ∈ u
h'x : x ≤ 0
⊢ -↑x.natAbs = x

Proof state:
case e_a.refine_1
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x => ↑x) v'
u2 : Finset ℤ := image (fun x => -↑x) v'
A : u ⊆ u1 ∪ u2
hx : 0 ∈ (u1 ∪ u2) \ (u1 ∩ u2)
⊢ False

Tactic:
simp only [mem_sdiff, mem_union, mem_image, Nat.cast_eq_zero, exists_eq_right, neg_eq_zero,
  or_self, mem_inter, and_self, and_not_self, u1, u2] at hx

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem ext_elem_iff {x y : M} : x = y ↔ ∀ i, b.repr x i = b.repr y i

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x y : M
⊢ x = y ↔ ∀ (i : ι), (b.repr x) i = (b.repr y) i

Tactic:
simp only [← DFunLike.ext_iff, EmbeddingLike.apply_eq_iff_eq]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Multiset.lean
@[simp]
lemma mem_nsmul {a : α} {s : Multiset α} {n : ℕ} : a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s

Proof state:
case refine_1
α : Type u_1
a : α
s : Multiset α
n : ℕ
ha : a ∈ n • s
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
case refine_1
α : Type u_1
a : α
s : Multiset α
ha : a ∈ 0 • s
⊢ False

Proof state:
case refine_1
α : Type u_1
a : α
s : Multiset α
ha : a ∈ 0 • s
⊢ False

Tactic:
simp [zero_nsmul] at ha

Result:
no goals

Proof state:
case refine_2.intro
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s ∨ a ∈ s

Tactic:
exact Or.inr h.2

Result:
no goals

Proof state:
case refine_2.intro
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n.succ • s

Tactic:
rw [succ_nsmul, mem_add]

Result:
case refine_2.intro
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s ∨ a ∈ s

Proof state:
case refine_2
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s

Tactic:
obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero h.1

Result:
case refine_2.intro
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n.succ • s

Proof state:
α : Type u_1
a : α
s : Multiset α
n : ℕ
⊢ a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s

Tactic:
refine ⟨fun ha ↦ ⟨?_, mem_of_mem_nsmul ha⟩, fun h ↦ ?_⟩

Result:
case refine_1
α : Type u_1
a : α
s : Multiset α
n : ℕ
ha : a ∈ n • s
⊢ n ≠ 0

case refine_2
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s
-- Mathlib/CategoryTheory/Idempotents/Basic.lean
theorem Equivalence.isIdempotentComplete {D : Type*} [Category D] (ε : C ≌ D)
    (h : IsIdempotentComplete C) : IsIdempotentComplete D

Proof state:
case intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom

Tactic:
use ε.functor.obj Y, ε.functor.map i, ε.functor.map e

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y) ∧ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom

Proof state:
case h.right
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.counit.app X' ≫ p ≫ ε.counitInv.app X' = φ.inv ≫ p ≫ φ.hom

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem cocycle (i j k : 𝒰.J) : t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j = 𝟙 _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j = 𝟙 (pullback (fV 𝒰 f g i j) (fV 𝒰 f g i k))

Tactic:
apply pullback.hom_ext <;> rw [Category.id_comp]

Result:
case h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ (t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)

case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ (t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)

Proof state:
case h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ ((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
      pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)

Tactic:
apply pullback.hom_ext

Result:
case h₀.h₀.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) ≫
      pullback.fst (𝒰.map i ≫ f) g =
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) ≫
      pullback.fst (𝒰.map i ≫ f) g

case h₀.h₀.h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ (((t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫
        pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) ≫
      pullback.snd (𝒰.map i ≫ f) g =
    (pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)) ≫
      pullback.snd (𝒰.map i ≫ f) g
-- Mathlib/RingTheory/Nilpotent/Basic.lean
theorem isReduced_iff_pow_one_lt [MonoidWithZero R] (k : ℕ) (hk : 1 < k) :
    IsReduced R ↔ ∀ x : R, x ^ k = 0 → x = 0

Proof state:
R : Type u_1
inst✝ : MonoidWithZero R
k : ℕ
hk : 1 < k
⊢ IsReduced R ↔ ∀ (x : R), x ^ k = 0 → x = 0

Tactic:
simp_rw [← zero_isRadical_iff, isRadical_iff_pow_one_lt k hk, zero_dvd_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem tsub_le_iff_tsub_le : a - b ≤ c ↔ a - c ≤ b

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - b ≤ c ↔ a - c ≤ b

Tactic:
rw [tsub_le_iff_left, tsub_le_iff_right]

Result:
no goals
-- Mathlib/FieldTheory/CardinalEmb.lean
theorem succEquiv_coherence (i : ι) (f) : (succEquiv i f).1 =
    f.comp (Subalgebra.inclusion <| strictMono_filtration.monotone <| le_succ i)

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.toType
f : ↥(adjoin F (⇑b ∘ φ '' Iio (i⁺))) →ₐ[F] Ē
⊢ ((succEquiv i) f).1 = f.comp (Subalgebra.inclusion ⋯)

Tactic:
ext

Result:
case H
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.toType
f : ↥(adjoin F (⇑b ∘ φ '' Iio (i⁺))) →ₐ[F] Ē
x✝ : ↥(adjoin F (⇑b ∘ φ '' Iio i))
⊢ ((succEquiv i) f).1 x✝ = (f.comp (Subalgebra.inclusion ⋯)) x✝

Proof state:
case H
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.toType
f : ↥(adjoin F (⇑b ∘ φ '' Iio (i⁺))) →ₐ[F] Ē
x✝ : ↥(adjoin F (⇑b ∘ φ '' Iio i))
⊢ ((Equiv.sigmaEquivProdOfEquiv fun x =>
            (embEquivOfIsAlgClosed ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯ Ē).symm)
          (algHomEquivSigma (f.comp ↑(equivOfEq ⋯)))).1
      x✝ =
    f ((Subalgebra.inclusion ⋯) x✝)

Tactic:
rfl

Result:
no goals

Proof state:
case H
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.toType
f : ↥(adjoin F (⇑b ∘ φ '' Iio (i⁺))) →ₐ[F] Ē
x✝ : ↥(adjoin F (⇑b ∘ φ '' Iio i))
⊢ ((succEquiv i) f).1 x✝ = (f.comp (Subalgebra.inclusion ⋯)) x✝

Tactic:
simp [succEquiv]

Result:
case H
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.toType
f : ↥(adjoin F (⇑b ∘ φ '' Iio (i⁺))) →ₐ[F] Ē
x✝ : ↥(adjoin F (⇑b ∘ φ '' Iio i))
⊢ ((Equiv.sigmaEquivProdOfEquiv fun x =>
            (embEquivOfIsAlgClosed ↥(adjoin F (⇑b ∘ φ '' Iio i)) ↥(↥(adjoin F (⇑b ∘ φ '' Iio i)))⟮b (φ i)⟯ Ē).symm)
          (algHomEquivSigma (f.comp ↑(equivOfEq ⋯)))).1
      x✝ =
    f ((Subalgebra.inclusion ⋯) x✝)
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem descFactorial_le_pow (n : ℕ) : ∀ k : ℕ, n.descFactorial k ≤ n ^ k
  | 0 => by rw [descFactorial_zero, Nat.pow_zero]
  | k + 1 => by
    rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm _ n]
    exact Nat.mul_le_mul (Nat.sub_le _ _) (descFactorial_le_pow _ k)

Proof state:
n k : ℕ
⊢ n.descFactorial (k + 1) ≤ n ^ (k + 1)

Tactic:
rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm _ n]

Result:
n k : ℕ
⊢ (n - k) * n.descFactorial k ≤ n * n ^ k

Proof state:
n : ℕ
⊢ n.descFactorial 0 ≤ n ^ 0

Tactic:
rw [descFactorial_zero, Nat.pow_zero]

Result:
no goals

Proof state:
n k : ℕ
⊢ (n - k) * n.descFactorial k ≤ n * n ^ k

Tactic:
exact Nat.mul_le_mul (Nat.sub_le _ _) (descFactorial_le_pow _ k)

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_of_mem_sInter {x y z : ZFSet} (hy : y ∈ ⋂₀ x) (hz : z ∈ x) : y ∈ z

Proof state:
x y z : ZFSet.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
⊢ y ∈ z

Tactic:
rcases eq_empty_or_nonempty x with (rfl | hx)

Result:
case inl
y z : ZFSet.{u_1}
hy : y ∈ ⋂₀ ∅
hz : z ∈ ∅
⊢ y ∈ z

case inr
x y z : ZFSet.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
hx : x.Nonempty
⊢ y ∈ z

Proof state:
case inl
y z : ZFSet.{u_1}
hy : y ∈ ⋂₀ ∅
hz : z ∈ ∅
⊢ y ∈ z

Tactic:
exact (not_mem_empty z hz).elim

Result:
no goals

Proof state:
case inr
x y z : ZFSet.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
hx : x.Nonempty
⊢ y ∈ z

Tactic:
exact (mem_sInter hx).1 hy z hz

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem add_ciSup (hf : BddAbove (range f)) (c : Cardinal.{v}) :
    c + (⨆ i, f i) = ⨆ i, c + f i

Proof state:
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ c + ⨆ i, f i = ⨆ i, c + f i

Tactic:
rw [add_comm, Cardinal.ciSup_add f hf]

Result:
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ ⨆ i, f i + c = ⨆ i, c + f i

Proof state:
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ ⨆ i, f i + c = ⨆ i, c + f i

Tactic:
simp_rw [add_comm]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem mk_cardinal : #Cardinal = univ.{u, u + 1}

Proof state:
⊢ #Cardinal.{u} = univ.{u, u + 1}

Tactic:
simpa only [card_type, card_univ] using congr_arg card type_cardinal

Result:
no goals
-- Mathlib/Probability/StrongLaw.lean
theorem truncation_eq_self {f : α → ℝ} {A : ℝ} {x : α} (h : |f x| < A) :
    truncation f A x = f x

Proof state:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
H : f x ∉ Set.Ioc (-A) A
⊢ 0 = f x

Tactic:
apply H.elim

Result:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
H : f x ∉ Set.Ioc (-A) A
⊢ f x ∈ Set.Ioc (-A) A

Proof state:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
⊢ f x ∉ Set.Ioc (-A) A → 0 = f x

Tactic:
intro H

Result:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
H : f x ∉ Set.Ioc (-A) A
⊢ 0 = f x

Proof state:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
⊢ truncation f A x = f x

Tactic:
simp only [truncation, indicator, Set.mem_Icc, id, Function.comp_apply, ite_eq_left_iff]

Result:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
⊢ f x ∉ Set.Ioc (-A) A → 0 = f x

Proof state:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h : |f x| < A
H : f x ∉ Set.Ioc (-A) A
⊢ f x ∈ Set.Ioc (-A) A

Tactic:
simp [(abs_lt.1 h).1, (abs_lt.1 h).2.le]

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem le_fib_self {n : ℕ} (five_le_n : 5 ≤ n) : n ≤ fib n

Proof state:
n : ℕ
five_le_n : 5 ≤ n
⊢ n ≤ fib n

Tactic:
induction' five_le_n with n five_le_n IH

Result:
case refl
n : ℕ
⊢ 5 ≤ fib 5

case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ n.succ ≤ fib n.succ

Proof state:
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ 2 ≤ 5

Tactic:
decide

Result:
no goals

Proof state:
case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ n.succ ≤ fib n.succ

Tactic:
rw [succ_le_iff]

Result:
case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ n < fib n.succ

Proof state:
case refl
n : ℕ
⊢ 5 ≤ fib 5

Tactic:
rfl

Result:
no goals

Proof state:
case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ n < fib n.succ

Tactic:
calc
  n ≤ fib n := IH
  _ < fib (n + 1) := fib_lt_fib_succ (le_trans (by decide) five_le_n)

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem isAffineOpen_top (X : Scheme) [IsAffine X] : IsAffineOpen (⊤ : X.Opens)

Proof state:
case h.e'_2
X : Scheme
inst✝ : IsAffine X
⊢ ⊤ = Scheme.Hom.opensRange (𝟙 X)

Tactic:
ext1

Result:
case h.e'_2.h
X : Scheme
inst✝ : IsAffine X
⊢ ↑⊤ = ↑(Scheme.Hom.opensRange (𝟙 X))

Proof state:
X : Scheme
inst✝ : IsAffine X
⊢ IsAffineOpen ⊤

Tactic:
convert isAffineOpen_opensRange (𝟙 X)

Result:
case h.e'_2
X : Scheme
inst✝ : IsAffine X
⊢ ⊤ = Scheme.Hom.opensRange (𝟙 X)

Proof state:
case h.e'_2.h
X : Scheme
inst✝ : IsAffine X
⊢ ↑⊤ = ↑(Scheme.Hom.opensRange (𝟙 X))

Tactic:
exact Set.range_id.symm

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
@[simp, norm_cast]
lemma ofReal_nnqsmul (q : ℚ≥0) (r : ℝ) : ofReal (q • r) = q • r

Proof state:
q : ℚ≥0
r : ℝ
⊢ ↑(q • r) = q • ↑r

Tactic:
simp [NNRat.smul_def]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem Continuous.min (hf : Continuous f) (hg : Continuous g) :
    Continuous fun b => min (f b) (g b)

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
⊢ Continuous fun b => f b ⊓ g b

Tactic:
simp only [min_def]

Result:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
⊢ Continuous fun b => if f b ≤ g b then f b else g b

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous f
hg : Continuous g
⊢ Continuous fun b => if f b ≤ g b then f b else g b

Tactic:
exact hf.if_le hg hf hg fun x => id

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem cospanExt_inv_app_one : (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.one = iZ.inv

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).inv.app WalkingCospan.one = iZ.inv

Tactic:
dsimp [cospanExt]

Result:
no goals
-- Mathlib/Dynamics/OmegaLimit.lean
theorem omegaLimit_subset_closure_fw_image {u : Set τ} (hu : u ∈ f) :
    ω f ϕ s ⊆ closure (image2 ϕ u s)

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
⊢ ⋂ u, closure (image2 ϕ (↑u) s) ⊆ closure (image2 ϕ u s)

Tactic:
intro _ hx

Result:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : a✝ ∈ ⋂ u, closure (image2 ϕ (↑u) s)
⊢ a✝ ∈ closure (image2 ϕ u s)

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : ∀ (i : ↑f.sets), a✝ ∈ closure (image2 ϕ (↑i) s)
⊢ a✝ ∈ closure (image2 ϕ u s)

Tactic:
exact hx ⟨u, hu⟩

Result:
no goals

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
⊢ ω f ϕ s ⊆ closure (image2 ϕ u s)

Tactic:
rw [omegaLimit_eq_iInter]

Result:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
⊢ ⋂ u, closure (image2 ϕ (↑u) s) ⊆ closure (image2 ϕ u s)

Proof state:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : a✝ ∈ ⋂ u, closure (image2 ϕ (↑u) s)
⊢ a✝ ∈ closure (image2 ϕ u s)

Tactic:
rw [mem_iInter] at hx

Result:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : ∀ (i : ↑f.sets), a✝ ∈ closure (image2 ϕ (↑i) s)
⊢ a✝ ∈ closure (image2 ϕ u s)
-- Mathlib/Analysis/Convex/Gauge.lean
theorem mul_gauge_le_norm (hs : Metric.ball (0 : E) r ⊆ s) : r * gauge s x ≤ ‖x‖

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
⊢ r * gauge s x ≤ ‖x‖

Tactic:
obtain hr | hr := le_or_lt r 0

Result:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : r ≤ 0
⊢ r * gauge s x ≤ ‖x‖

case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : 0 < r
⊢ r * gauge s x ≤ ‖x‖

Proof state:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : 0 < r
⊢ gauge s x ≤ gauge (ball 0 r) x

Tactic:
exact gauge_mono (absorbent_ball_zero hr) hs x

Result:
no goals

Proof state:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : 0 < r
⊢ r * gauge s x ≤ ‖x‖

Tactic:
rw [mul_comm, ← le_div_iff₀ hr, ← gauge_ball hr.le]

Result:
case inr
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : 0 < r
⊢ gauge s x ≤ gauge (ball 0 r) x

Proof state:
case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hs : ball 0 r ⊆ s
hr : r ≤ 0
⊢ r * gauge s x ≤ ‖x‖

Tactic:
exact (mul_nonpos_of_nonpos_of_nonneg hr <| gauge_nonneg _).trans (norm_nonneg _)

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem univ_pi_Iio_ae_eq_Iic {f : ∀ i, α i} :
    (pi univ fun i => Iio (f i)) =ᵐ[Measure.pi μ] Iic f

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f : (i : ι) → α i
⊢ (univ.pi fun i => Iio (f i)) =ᶠ[ae (Measure.pi μ)] univ.pi fun i => Iic (f i)

Tactic:
exact pi_Iio_ae_eq_pi_Iic

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f : (i : ι) → α i
⊢ (univ.pi fun i => Iio (f i)) =ᶠ[ae (Measure.pi μ)] Iic f

Tactic:
rw [← pi_univ_Iic]

Result:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f : (i : ι) → α i
⊢ (univ.pi fun i => Iio (f i)) =ᶠ[ae (Measure.pi μ)] univ.pi fun i => Iic (f i)
-- Mathlib/Data/Sym/Basic.lean
theorem decode_encode [DecidableEq α] (s : Sym (Option α) n.succ) : decode (encode s) = s

Proof state:
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ decode (encode s) = s

Tactic:
simp only [decode, h, not_false_iff, encode_of_not_none_mem, Embedding.some_apply, map_map,
  comp_apply, Option.some_get]

Result:
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ map (fun x => ↑x) s.attach = s

Proof state:
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ map (fun x => ↑x) s.attach = s

Tactic:
convert s.attach_map_coe

Result:
no goals

Proof state:
case pos
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∈ s
⊢ decode (encode s) = s

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
⊢ decode (encode s) = s

Tactic:
by_cases h : none ∈ s

Result:
case pos
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∈ s
⊢ decode (encode s) = s

case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ decode (encode s) = s