harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Complex/Periodic.lean
theorem differentiableAt_cuspFunction (hh : h ≠ 0) (hf : Periodic f h)
    {z : ℂ} (hol_z : DifferentiableAt ℂ f z) :
    DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Proof state:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * ↑π * I / ↑h)) z
diff_ne : q * (2 * ↑π * I / ↑h) ≠ 0
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * ↑π * I / ↑h)) z qdiff diff_ne
diff_L : DifferentiableAt ℂ L q
hL : 𝕢 h ∘ L =ᶠ[𝓝 q] id
hF : f ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
this : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Tactic:
rw [← EventuallyEq.eq_of_nhds (qdiff.hasStrictFDerivAt_equiv diff_ne).eventually_left_inverse]
  at hol_z

Result:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * ↑π * I / ↑h)) z
diff_ne : q * (2 * ↑π * I / ↑h) ≠ 0
hol_z :
  DifferentiableAt ℂ f
    (HasStrictFDerivAt.localInverse (𝕢 h)
      ((ContinuousLinearEquiv.unitsEquivAut ℂ) (Units.mk0 (q * (2 * ↑π * I / ↑h)) diff_ne)) z ⋯ (𝕢 h z))
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * ↑π * I / ↑h)) z qdiff diff_ne
diff_L : DifferentiableAt ℂ L q
hL : 𝕢 h ∘ L =ᶠ[𝓝 q] id
hF : f ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
this : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)
-- Mathlib/Analysis/Convex/Slope.lean
theorem StrictConvexOn.secant_strict_mono_aux2 (hf : StrictConvexOn 𝕜 s f) {x y z : 𝕜} (hx : x ∈ s)
    (hz : z ∈ s) (hxy : x < y) (hyz : y < z) : (f y - f x) / (y - x) < (f z - f x) / (z - x)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ 0 < y - x

Tactic:
linarith

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) < (f z - f x) / (z - x)

Tactic:
have hxy' : 0 < y - x := by linarith

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ (f y - f x) / (y - x) < (f z - f x) / (z - x)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
⊢ (f y - f x) * (z - x) < (f z - f x) * (y - x)

Tactic:
linarith only [hf.secant_strict_mono_aux1 hx hz hxy hyz]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
⊢ (f y - f x) / (y - x) < (f z - f x) / (z - x)

Tactic:
rw [div_lt_div_iff₀ hxy' hxz']

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
⊢ (f y - f x) * (z - x) < (f z - f x) * (y - x)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ 0 < z - x

Tactic:
linarith

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
⊢ (f y - f x) / (y - x) < (f z - f x) / (z - x)

Tactic:
have hxz' : 0 < z - x := by linarith

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hxz' : 0 < z - x
⊢ (f y - f x) / (y - x) < (f z - f x) / (z - x)
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.id_pre (F : J ⥤ C) : limit.pre F (𝟭 _) = lim.map (Functor.leftUnitor F).inv

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasLimitsOfShape J C
F : J ⥤ C
⊢ pre F (𝟭 J) = lim.map F.leftUnitor.inv

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_fintype [Fintype β] (f : β → α) : ∏' b, f b = ∏ b, f b

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : Fintype β
f : β → α
⊢ ∏' (b : β), f b = ∏ b : β, f b

Tactic:
apply tprod_eq_prod

Result:
case hf
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : Fintype β
f : β → α
⊢ ∀ b ∉ univ, f b = 1

Proof state:
case hf
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : Fintype β
f : β → α
⊢ ∀ b ∉ univ, f b = 1

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem sup_direction_lt_of_nonempty_of_inter_empty {s₁ s₂ : AffineSubspace k P}
    (h1 : (s₁ : Set P).Nonempty) (h2 : (s₂ : Set P).Nonempty) (he : (s₁ ∩ s₂ : Set P) = ∅) :
    s₁.direction ⊔ s₂.direction < (s₁ ⊔ s₂).direction

Proof state:
case right.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ +ᵥ p₁ = -v₂ +ᵥ p₂
⊢ False

Tactic:
refine Set.Nonempty.ne_empty ?_ he

Result:
case right.intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
he : ↑s₁ ∩ ↑s₂ = ∅
p₁ : P
hp₁ : p₁ ∈ ↑s₁
p₂ : P
hp₂ : p₂ ∈ ↑s₂
v₁ : V
hv₁ : v₁ ∈ s₁.direction
v₂ : V
hv₂ : v₂ ∈ s₂.direction
hv₁v₂ : v₁ +ᵥ p₁ = -v₂ +ᵥ p₂
⊢ (↑s₁ ∩ ↑s₂).Nonempty
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma zeroLocus_map {U V : X.Opens} (i : U ≤ V) (s : Set Γ(X, V)) :
    X.zeroLocus ((X.presheaf.map (homOfLE i).op).hom '' s) = X.zeroLocus s ∪ Uᶜ

Proof state:
case h
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
x : ↑↑X.toPresheafedSpace
⊢ (∀ (i : ↑Γ(X, V)), x ∈ U → i ∈ s → x ∉ X.basicOpen i) ↔ x ∈ U → ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
rw [forall_comm (β := x ∈ U)]

Result:
no goals

Proof state:
case h
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
x : ↑↑X.toPresheafedSpace
⊢ (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
conv_lhs => enter [i]; rw [forall_comm (β := x ∈ U)]

Result:
case h
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
x : ↑↑X.toPresheafedSpace
⊢ (∀ (i : ↑Γ(X, V)), x ∈ U → i ∈ s → x ∉ X.basicOpen i) ↔ x ∈ U → ∀ f ∈ s, x ∉ X.basicOpen f

Proof state:
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
x : ↑↑X.toPresheafedSpace
this : (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → ∀ f ∈ s, x ∉ X.basicOpen f
⊢ x ∈ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) '' s) ↔ x ∈ X.zeroLocus s ∪ (↑U)ᶜ

Tactic:
simpa [or_iff_not_imp_right]

Result:
no goals

Proof state:
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
⊢ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) '' s) = X.zeroLocus s ∪ (↑U)ᶜ

Tactic:
ext x

Result:
case h
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) '' s) ↔ x ∈ X.zeroLocus s ∪ (↑U)ᶜ

Proof state:
case h
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) '' s) ↔ x ∈ X.zeroLocus s ∪ (↑U)ᶜ

Tactic:
suffices (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → (∀ f ∈ s, x ∉ X.basicOpen f) by
  simpa [or_iff_not_imp_right]

Result:
case h
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
x : ↑↑X.toPresheafedSpace
⊢ (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → ∀ f ∈ s, x ∉ X.basicOpen f
-- Mathlib/SetTheory/Game/Nim.lean
theorem le_grundyValue_of_Iio_subset_moveRight {G : PGame} [G.Impartial] {o : Nimber}
    (h : Set.Iio o ⊆ Set.range (grundyValue ∘ G.moveRight)) : o ≤ grundyValue G

Proof state:
case intro
G : PGame
inst✝ : G.Impartial
o : Nimber
h : Set.Iio o ⊆ Set.range (grundyValue ∘ G.moveRight)
ho : G.grundyValue < o
i : G.RightMoves
hi : (grundyValue ∘ G.moveRight) i = G.grundyValue
⊢ False

Tactic:
exact grundyValue_ne_moveRight i hi

Result:
no goals

Proof state:
G : PGame
inst✝ : G.Impartial
o : Nimber
h : Set.Iio o ⊆ Set.range (grundyValue ∘ G.moveRight)
ho : G.grundyValue < o
⊢ False

Tactic:
obtain ⟨i, hi⟩ := h ho

Result:
case intro
G : PGame
inst✝ : G.Impartial
o : Nimber
h : Set.Iio o ⊆ Set.range (grundyValue ∘ G.moveRight)
ho : G.grundyValue < o
i : G.RightMoves
hi : (grundyValue ∘ G.moveRight) i = G.grundyValue
⊢ False

Proof state:
G : PGame
inst✝ : G.Impartial
o : Nimber
h : Set.Iio o ⊆ Set.range (grundyValue ∘ G.moveRight)
⊢ o ≤ G.grundyValue

Tactic:
by_contra! ho

Result:
G : PGame
inst✝ : G.Impartial
o : Nimber
h : Set.Iio o ⊆ Set.range (grundyValue ∘ G.moveRight)
ho : G.grundyValue < o
⊢ False
-- Mathlib/Analysis/Complex/AbelLimit.lean
private lemma stolzCone_subset_stolzSet_aux' (s : ℝ) :
    ∃ M ε, 0 < M ∧ 0 < ε ∧ ∀ x y, 0 < x → x < ε → |y| < s * x →
      sqrt (x ^ 2 + y ^ 2) < M * (1 - sqrt ((1 - x) ^ 2 + y ^ 2))

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ (1 - x) ^ 2 + y ^ 2 ≤ (1 - x) ^ 2 + (s * x) ^ 2

Tactic:
rw [← sq_abs y]

Result:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ (1 - x) ^ 2 + |y| ^ 2 ≤ (1 - x) ^ 2 + (s * x) ^ 2

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ (1 - x) ^ 2 + |y| ^ 2 ≤ (1 - x) ^ 2 + (s * x) ^ 2

Tactic:
gcongr

Result:
no goals

Proof state:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ √(x ^ 2 + (s * x) ^ 2) = √((1 + s ^ 2) * x ^ 2)

Tactic:
congr

Result:
case e_x
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ x ^ 2 + (s * x) ^ 2 = (1 + s ^ 2) * x ^ 2
-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
private lemma summable_F'' : Summable F''

Proof state:
case refine_1
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ Summable fun y => (↑↑p)⁻¹ ^ y * (↑↑p)⁻¹ ^ (3 / 2)

Tactic:
exact Summable.mul_right _ <| summable_geometric_of_lt_one (hp₀ p).le (hp₁ p)

Result:
no goals

Proof state:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
this : Summable fun pk => (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)
pk : Nat.Primes × ℕ
⊢ 0 ≤ (if Nat.Prime (↑pk.1 ^ (pk.2 + 1 + 1)) then 0 else Λ (↑pk.1 ^ (pk.2 + 1 + 1))) / ↑↑pk.1 ^ (pk.2 + 1 + 1)

Tactic:
have := vonMangoldt_nonneg (n := (pk.1 : ℕ) ^ (pk.2 + 2))

Result:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
this✝ : Summable fun pk => (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)
pk : Nat.Primes × ℕ
this : 0 ≤ Λ (↑pk.1 ^ (pk.2 + 2))
⊢ 0 ≤ (if Nat.Prime (↑pk.1 ^ (pk.2 + 1 + 1)) then 0 else Λ (↑pk.1 ^ (pk.2 + 1 + 1))) / ↑↑pk.1 ^ (pk.2 + 1 + 1)

Proof state:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
x✝ : Nat.Primes × ℕ
⊢ 0 x✝ ≤ (↑↑x✝.1)⁻¹ ^ x✝.2 * (↑↑x✝.1)⁻¹ ^ (3 / 2)

Tactic:
positivity

Result:
no goals

Proof state:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ 1 - 2⁻¹ = 2⁻¹

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem not_of_lt_findIdx {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.findIdx p) :
    p (xs[i]'(Nat.le_trans h (findIdx_le_length p))) = false

Proof state:
case cons.inr
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ ho : i < findIdx p (x :: xs)
npx : p x = false
h : i < findIdx p xs + 1
e : i > 0
ipm : i.pred.succ = i
⊢ p xs[i.pred] = false

Tactic:
rw [← ipm, Nat.succ_lt_succ_iff] at h

Result:
case cons.inr
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ ho : i < findIdx p (x :: xs)
npx : p x = false
h : i.pred < findIdx p xs
e : i > 0
ipm : i.pred.succ = i
⊢ p xs[i.pred] = false

Proof state:
α : Type u_1
p : α → Bool
xs : List α
⊢ ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false

Tactic:
induction xs with
| nil => intro i h; rw [findIdx_nil] at h; simp at h
| cons x xs ih =>
  intro i h
  have ho := h
  rw [findIdx_cons] at h
  have npx : p x = false := by
    apply eq_false_of_ne_true
    intro y
    rw [y, cond_true] at h
    simp at h
  simp [npx, cond_false] at h
  cases i.eq_zero_or_pos with
  | inl e => simpa [e, Fin.zero_eta, get_cons_zero]
  | inr e =>
    have ipm := Nat.succ_pred_eq_of_pos e
    simp +singlePass only [← ipm, getElem_cons_succ]
    rw [← ipm, Nat.succ_lt_succ_iff] at h
    simpa using ih h

Result:
no goals
-- Mathlib/Order/Filter/CountablyGenerated.lean
theorem antitone_seq_of_seq (s : ℕ → Set α) :
    ∃ t : ℕ → Set α, Antitone t ∧ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (t i)

Proof state:
case h
α : Type u_1
s : ℕ → Set α
⊢ (Antitone fun n => ⋂ m, ⋂ (_ : m ≤ n), s m) ∧ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 ((fun n => ⋂ m, ⋂ (_ : m ≤ n), s m) i)

Tactic:
constructor

Result:
case h.left
α : Type u_1
s : ℕ → Set α
⊢ Antitone fun n => ⋂ m, ⋂ (_ : m ≤ n), s m

case h.right
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

Proof state:
case h.left
α : Type u_1
s : ℕ → Set α
⊢ Antitone fun n => ⋂ m, ⋂ (_ : m ≤ n), s m

Tactic:
exact fun i j hij => biInter_mono (Iic_subset_Iic.2 hij) fun n _ => Subset.rfl

Result:
no goals

Proof state:
case h.right
α : Type u_1
s : ℕ → Set α
⊢ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

Tactic:
apply le_antisymm <;> rw [le_iInf_iff] <;> intro i

Result:
case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ i, 𝓟 (s i) ≤ 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)

Proof state:
case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ i, 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m) ≤ 𝓟 (s i)

Tactic:
refine iInf_le_of_le i (principal_mono.2 <| iInter₂_subset i ?_)

Result:
case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ i ≤ i

Proof state:
case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ i ≤ i

Tactic:
rfl

Result:
no goals

Proof state:
case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⨅ i, 𝓟 (s i) ≤ 𝓟 (⋂ m, ⋂ (_ : m ≤ i), s m)

Tactic:
rw [le_principal_iff]

Result:
case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⋂ m, ⋂ (_ : m ≤ i), s m ∈ ⨅ i, 𝓟 (s i)

Proof state:
α : Type u_1
s : ℕ → Set α
⊢ ∃ t, Antitone t ∧ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (t i)

Tactic:
use fun n => ⋂ m ≤ n, s m

Result:
case h
α : Type u_1
s : ℕ → Set α
⊢ (Antitone fun n => ⋂ m, ⋂ (_ : m ≤ n), s m) ∧ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 ((fun n => ⋂ m, ⋂ (_ : m ≤ n), s m) i)

Proof state:
case h.right.a
α : Type u_1
s : ℕ → Set α
i j : ℕ
x✝ : j ∈ {i_1 | i_1 ≤ i}
⊢ s j ∈ ⨅ i, 𝓟 (s i)

Tactic:
exact mem_iInf_of_mem j (mem_principal_self _)

Result:
no goals

Proof state:
case h.right.a
α : Type u_1
s : ℕ → Set α
i : ℕ
⊢ ⋂ m, ⋂ (_ : m ≤ i), s m ∈ ⨅ i, 𝓟 (s i)

Tactic:
refine (biInter_mem (finite_le_nat _)).2 fun j _ => ?_

Result:
case h.right.a
α : Type u_1
s : ℕ → Set α
i j : ℕ
x✝ : j ∈ {i_1 | i_1 ≤ i}
⊢ s j ∈ ⨅ i, 𝓟 (s i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_nonpos_of_nonneg_of_nonpos {a b : Int}
  (ha : 0 ≤ a) (hb : b ≤ 0) : a * b ≤ 0

Proof state:
a b : Int
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b ≤ 0

Tactic:
have h : a * b ≤ a * 0 := Int.mul_le_mul_of_nonneg_left hb ha

Result:
a b : Int
ha : 0 ≤ a
hb : b ≤ 0
h : a * b ≤ a * 0
⊢ a * b ≤ 0

Proof state:
a b : Int
ha : 0 ≤ a
hb : b ≤ 0
h : a * b ≤ a * 0
⊢ a * b ≤ 0

Tactic:
rwa [Int.mul_zero] at h

Result:
no goals
-- Mathlib/Algebra/CharP/Algebra.lean
/-- If `R →+* A` is injective, and `A` is of exponential characteristic `p`, then `R` is also of
exponential characteristic `p`. Similar to `RingHom.charZero`. -/
lemma RingHom.expChar {R A : Type*} [Semiring R] [Semiring A] (f : R →+* A)
    (H : Function.Injective f) (p : ℕ) [ExpChar A p] : ExpChar R p

Proof state:
case zero
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring A
f : R →+* A
H : Function.Injective ⇑f
inst✝ : CharZero A
this : CharZero R
⊢ ExpChar R 1

Tactic:
exact .zero

Result:
no goals

Proof state:
case prime
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring A
f : R →+* A
H : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
hchar✝ : CharP A p
⊢ ExpChar R p

Tactic:
haveI := f.charP H p

Result:
case prime
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring A
f : R →+* A
H : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
hchar✝ : CharP A p
this : CharP R p
⊢ ExpChar R p

Proof state:
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring A
f : R →+* A
H : Function.Injective ⇑f
p : ℕ
inst✝ : ExpChar A p
⊢ ExpChar R p

Tactic:
cases ‹ExpChar A p› with
| zero => haveI := f.charZero; exact .zero
| prime hp => haveI := f.charP H p; exact .prime hp

Result:
no goals

Proof state:
case zero
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring A
f : R →+* A
H : Function.Injective ⇑f
inst✝ : CharZero A
⊢ ExpChar R 1

Tactic:
haveI := f.charZero

Result:
case zero
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring A
f : R →+* A
H : Function.Injective ⇑f
inst✝ : CharZero A
this : CharZero R
⊢ ExpChar R 1

Proof state:
case prime
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring A
f : R →+* A
H : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
hchar✝ : CharP A p
this : CharP R p
⊢ ExpChar R p

Tactic:
exact .prime hp

Result:
no goals
-- Mathlib/LinearAlgebra/Orientation.lean
theorem abs_det_adjustToOrientation [Nonempty ι] (e : Basis ι R M)
    (x : Orientation R M ι) (v : ι → M) : |(e.adjustToOrientation x).det v| = |e.det v|

Proof state:
R : Type u_1
inst✝⁵ : LinearOrderedCommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
v : ι → M
⊢ |(e.adjustToOrientation x).det v| = |e.det v|

Tactic:
rcases e.det_adjustToOrientation x with h | h <;> simp [h]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem dual_lc (l : ι →₀ R) (i : ι) : ε i (DualBases.lc e l) = l i

Proof state:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (ε i) (lc e l) = l i

Tactic:
rw [lc, _root_.map_finsupp_sum, Finsupp.sum_eq_single i (g := fun a b ↦ (ε i) (b • e a))]

Result:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (ε i) (l i • e i) = l i

case h₀
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ ∀ (b : ι), l b ≠ 0 → b ≠ i → (ε i) (l b • e b) = 0

case h₁
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ l i = 0 → (ε i) (0 • e i) = 0

Proof state:
case h₀
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i q : ι
a✝ : l q ≠ 0
q_ne : q ≠ i
⊢ (ε i) (l q • e q) = 0

Tactic:
simp [h.eval_of_ne q_ne.symm, smul_eq_mul]

Result:
no goals

Proof state:
case h₁
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ l i = 0 → (ε i) (0 • e i) = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (ε i) (l i • e i) = l i

Tactic:
simp [h.eval_same, smul_eq_mul]

Result:
no goals

Proof state:
case h₀
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ ∀ (b : ι), l b ≠ 0 → b ≠ i → (ε i) (l b • e b) = 0

Tactic:
intro q _ q_ne

Result:
case h₀
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i q : ι
a✝ : l q ≠ 0
q_ne : q ≠ i
⊢ (ε i) (l q • e q) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem choice_eq {α : Type _} [Subsingleton α] (a : α) : choice α = some a

Proof state:
α : Type u_1
inst✝ : Subsingleton α
a : α
⊢ Classical.choice ⋯ = a

Tactic:
apply Subsingleton.elim

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Subsingleton α
a : α
⊢ (if h : Nonempty α then some (Classical.choice h) else none) = some a

Tactic:
rw [dif_pos (⟨a⟩ : Nonempty α)]

Result:
α : Type u_1
inst✝ : Subsingleton α
a : α
⊢ some (Classical.choice ⋯) = some a

Proof state:
α : Type u_1
inst✝ : Subsingleton α
a : α
⊢ choice α = some a

Tactic:
simp [choice]

Result:
α : Type u_1
inst✝ : Subsingleton α
a : α
⊢ (if h : Nonempty α then some (Classical.choice h) else none) = some a

Proof state:
α : Type u_1
inst✝ : Subsingleton α
a : α
⊢ some (Classical.choice ⋯) = some a

Tactic:
simp

Result:
α : Type u_1
inst✝ : Subsingleton α
a : α
⊢ Classical.choice ⋯ = a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_setWidth_of_le (x : BitVec w) (h : k ≤ l) :
    (x.setWidth l).setWidth k = x.setWidth k

Proof state:
case pred
w k l : Nat
x : BitVec w
h : k ≤ l
i : Nat
a✝ : i < k
⊢ (setWidth k (setWidth l x)).getLsbD i = (setWidth k x).getLsbD i

Tactic:
simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and]

Result:
case pred
w k l : Nat
x : BitVec w
h : k ≤ l
i : Nat
a✝ : i < k
⊢ (decide (i < k) && (decide (i < l) && x.getLsbD i)) = (decide (i < k) && x.getLsbD i)

Proof state:
case pred.true
w k l : Nat
x : BitVec w
h : k ≤ l
i : Nat
a✝ : i < k
⊢ i < w → i < k → i < l

Tactic:
omega

Result:
no goals

Proof state:
case pred
w k l : Nat
x : BitVec w
h : k ≤ l
i : Nat
a✝ : i < k
⊢ (x.getLsbD i = true → i < w) → (decide (i < k) && (decide (i < l) && x.getLsbD i)) = (decide (i < k) && x.getLsbD i)

Tactic:
cases getLsbD x i <;> simp

Result:
case pred.true
w k l : Nat
x : BitVec w
h : k ≤ l
i : Nat
a✝ : i < k
⊢ i < w → i < k → i < l

Proof state:
case pred
w k l : Nat
x : BitVec w
h : k ≤ l
i : Nat
a✝ : i < k
⊢ (decide (i < k) && (decide (i < l) && x.getLsbD i)) = (decide (i < k) && x.getLsbD i)

Tactic:
have p := lt_of_getLsbD (x := x) (i := i)

Result:
case pred
w k l : Nat
x : BitVec w
h : k ≤ l
i : Nat
a✝ : i < k
p : x.getLsbD i = true → i < w
⊢ (decide (i < k) && (decide (i < l) && x.getLsbD i)) = (decide (i < k) && x.getLsbD i)

Proof state:
w k l : Nat
x : BitVec w
h : k ≤ l
⊢ setWidth k (setWidth l x) = setWidth k x

Tactic:
ext i

Result:
case pred
w k l : Nat
x : BitVec w
h : k ≤ l
i : Nat
a✝ : i < k
⊢ (setWidth k (setWidth l x)).getLsbD i = (setWidth k x).getLsbD i

Proof state:
case pred
w k l : Nat
x : BitVec w
h : k ≤ l
i : Nat
a✝ : i < k
p : x.getLsbD i = true → i < w
⊢ (decide (i < k) && (decide (i < l) && x.getLsbD i)) = (decide (i < k) && x.getLsbD i)

Tactic:
revert p

Result:
case pred
w k l : Nat
x : BitVec w
h : k ≤ l
i : Nat
a✝ : i < k
⊢ (x.getLsbD i = true → i < w) → (decide (i < k) && (decide (i < l) && x.getLsbD i)) = (decide (i < k) && x.getLsbD i)
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem padic_norm_e_of_padicInt (z : ℤ_[p]) : ‖(z : ℚ_[p])‖ = ‖z‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ‖↑z‖ = ‖z‖

Tactic:
simp [norm_def]

Result:
no goals