harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
@[simp]
lemma evenKernel_neg (a : UnitAddCircle) (x : ℝ) : evenKernel (-a) x = evenKernel a x

Proof state:
a : UnitAddCircle
x : ℝ
⊢ evenKernel (-a) x = evenKernel a x

Tactic:
induction a using QuotientAddGroup.induction_on with
| H => simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, evenKernel_def, jacobiTheta₂_neg_left]

Result:
no goals

Proof state:
case H
x z✝ : ℝ
⊢ evenKernel (-↑z✝) x = evenKernel (↑z✝) x

Tactic:
simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, evenKernel_def, jacobiTheta₂_neg_left]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem isNormal_preOmega : IsNormal preOmega

Proof state:
o : Ordinal.{u_1}
ho : o.IsLimit
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ (preOmega b).card < a.card

Tactic:
apply lt_of_lt_of_le _ (card_le_card <| ha _ (ho.succ_lt hb))

Result:
o : Ordinal.{u_1}
ho : o.IsLimit
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ (preOmega b).card < (preOmega (succ b)).card

Proof state:
⊢ IsNormal ⇑preOmega

Tactic:
rw [isNormal_iff_strictMono_limit]

Result:
⊢ StrictMono ⇑preOmega ∧
    ∀ (o : Ordinal.{u_1}), o.IsLimit → ∀ (a : Ordinal.{u_1}), (∀ b < o, preOmega b ≤ a) → preOmega o ≤ a

Proof state:
o : Ordinal.{u_1}
ho : o.IsLimit
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ (preOmega b).card < (preOmega (succ b)).card

Tactic:
rw [(isInitial_preOmega _).card_lt_card, preOmega_lt_preOmega]

Result:
o : Ordinal.{u_1}
ho : o.IsLimit
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ b < succ b

Proof state:
⊢ StrictMono ⇑preOmega ∧
    ∀ (o : Ordinal.{u_1}), o.IsLimit → ∀ (a : Ordinal.{u_1}), (∀ b < o, preOmega b ≤ a) → preOmega o ≤ a

Tactic:
refine ⟨preOmega_strictMono, fun o ho a ha ↦
  (preOmega_le_of_forall_lt (isInitial_ord _) fun b hb ↦ ?_).trans (ord_card_le a)⟩

Result:
o : Ordinal.{u_1}
ho : o.IsLimit
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ preOmega b < a.card.ord

Proof state:
o : Ordinal.{u_1}
ho : o.IsLimit
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ preOmega b < a.card.ord

Tactic:
rw [← (isInitial_ord _).card_lt_card, card_ord]

Result:
o : Ordinal.{u_1}
ho : o.IsLimit
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ (preOmega b).card < a.card

Proof state:
o : Ordinal.{u_1}
ho : o.IsLimit
a : Ordinal.{u_1}
ha : ∀ b < o, preOmega b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ b < succ b

Tactic:
exact lt_succ b

Result:
no goals
-- Mathlib/Algebra/Order/Ring/WithTop.lean
lemma mul_def (a b : WithTop α) :
    a * b = if a = 0 ∨ b = 0 then 0 else WithTop.map₂ (· * ·) a b

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
⊢ a * b = if a = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 => x1 * x2) a b

Tactic:
cases a <;> cases b <;> aesop

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem Set.Finite.closure_biUnion {ι : Type*} {s : Set ι} (hs : s.Finite) (f : ι → Set X) :
    closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
ι : Type u_3
s : Set ι
hs : s.Finite
f : ι → Set X
⊢ closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i)

Tactic:
simp [closure_eq_compl_interior_compl, hs.interior_biInter]

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem nextCoeff_eq_zero_of_eraseLead_eq_zero (h : f.eraseLead = 0) : f.nextCoeff = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
h₂ : ¬f.nextCoeff = 0
⊢ False

Tactic:
exact leadingCoeff_ne_zero.mp (leadingCoeff_eraseLead_eq_nextCoeff h₂ ▸ h₂) h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
⊢ f.nextCoeff = 0

Tactic:
by_contra h₂

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
h₂ : ¬f.nextCoeff = 0
⊢ False
-- Mathlib/RingTheory/IsTensorProduct.lean
/-- If `N` is the base change of `M` to `A`, then `N ⊗[R] P` is the base change
of `M ⊗[R] P` to `A`. This is simply the isomorphism
`A ⊗[S] (M ⊗[R] P) ≃ₗ[A] (A ⊗[S] M) ⊗[R] P`. -/
lemma isBaseChange_tensorProduct_map {f : M →ₗ[S] N} (hf : IsBaseChange A f) :
    IsBaseChange A (AlgebraTensorModule.map f (LinearMap.id (R := R) (M := P)))

Proof state:
case tmul
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
P : Type u_2
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
A : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra S A
inst✝⁵ : IsScalarTower R S A
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module A N
inst✝¹ : IsScalarTower S A N
inst✝ : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] M ⊗[R] P ≃ₗ[A] N ⊗[R] P :=
  (AlgebraTensorModule.assoc R S A A M P).symm ≪≫ₗ AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P)
m : M
p : P
⊢ e (1 ⊗ₜ[S] m ⊗ₜ[R] p) = (AlgebraTensorModule.map f LinearMap.id) (m ⊗ₜ[R] p)

Tactic:
simp [e, IsBaseChange.equiv_tmul]

Result:
no goals

Proof state:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
P : Type u_2
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
A : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra S A
inst✝⁵ : IsScalarTower R S A
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module A N
inst✝¹ : IsScalarTower S A N
inst✝ : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
⊢ IsBaseChange A (AlgebraTensorModule.map f LinearMap.id)

Tactic:
let e : A ⊗[S] M ⊗[R] P ≃ₗ[A] N ⊗[R] P := (AlgebraTensorModule.assoc R S A A M P).symm.trans
  (AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P))

Result:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : Module R M
inst✝¹³ : Module R N
inst✝¹² : Module S N
inst✝¹¹ : IsScalarTower R S N
P : Type u_2
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
A : Type u_4
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra S A
inst✝⁵ : IsScalarTower R S A
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
inst✝² : Module A N
inst✝¹ : IsScalarTower S A N
inst✝ : IsScalarTower R A N
f : M →ₗ[S] N
hf : IsBaseChange A f
e : A ⊗[S] M ⊗[R] P ≃ₗ[A] N ⊗[R] P :=
  (AlgebraTensorModule.assoc R S A A M P).symm ≪≫ₗ AlgebraTensorModule.congr hf.equiv (LinearEquiv.refl R P)
⊢ IsBaseChange A (AlgebraTensorModule.map f LinearMap.id)
-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLogExp.lean
@[simp] lemma EReal.log_exp (x : EReal) : log (exp x) = x

Proof state:
case h_real
a✝ : ℝ
⊢ (↑a✝).exp.log = ↑a✝

Tactic:
rw [exp_coe, log_ofReal, if_neg (not_le.mpr (Real.exp_pos _)), Real.log_exp]

Result:
no goals

Proof state:
case h_bot

⊢ ⊥.exp.log = ⊥

Tactic:
simp

Result:
no goals

Proof state:
x : EReal
⊢ x.exp.log = x

Tactic:
induction x

Result:
case h_bot

⊢ ⊥.exp.log = ⊥

case h_real
a✝ : ℝ
⊢ (↑a✝).exp.log = ↑a✝

case h_top

⊢ ⊤.exp.log = ⊤

Proof state:
case h_top

⊢ ⊤.exp.log = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Nilpotent.lean
lemma isNilpotent_aeval_sub_of_isNilpotent_sub (h : IsNilpotent (a - b)) :
    IsNilpotent (aeval a P - aeval b P)

Proof state:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
h : IsNilpotent (a - b)
⊢ IsNilpotent ((aeval a) P - (aeval b) P)

Tactic:
simp only [← eval_map_algebraMap]

Result:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
h : IsNilpotent (a - b)
⊢ IsNilpotent (eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P))

Proof state:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
h : IsNilpotent (a - b)
⊢ IsNilpotent (eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P))

Tactic:
have ⟨c, hc⟩ := evalSubFactor (map (algebraMap R S) P) a b

Result:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
h : IsNilpotent (a - b)
c : S
hc : eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P) = c * (a - b)
⊢ IsNilpotent (eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P))

Proof state:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
h : IsNilpotent (a - b)
c : S
hc : eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P) = c * (a - b)
⊢ IsNilpotent (eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P))

Tactic:
exact hc ▸ (Commute.all _ _).isNilpotent_mul_right h

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem add {β} [AddMonoid β] {f g : α →ₛ β} (hf : f.FinMeasSupp μ)
    (hg : g.FinMeasSupp μ) : (f + g).FinMeasSupp μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : AddMonoid β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (map (fun p => p.1 + p.2) (f.pair g)).FinMeasSupp μ

Tactic:
exact hf.map₂ hg (zero_add 0)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : AddMonoid β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (f + g).FinMeasSupp μ

Tactic:
rw [add_eq_map₂]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : AddMonoid β
f g : α →ₛ β
hf : f.FinMeasSupp μ
hg : g.FinMeasSupp μ
⊢ (map (fun p => p.1 + p.2) (f.pair g)).FinMeasSupp μ
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_integrand_deriv_integrable_A {s : ℂ} (hs : 0 < s.re) {X : ℝ} (hX : 0 ≤ X) :
    IntervalIntegrable (fun x => -((-x).exp * x ^ s) : ℝ → ℂ) volume 0 X

Proof state:
case h.e'_3.h
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x✝ : ℝ
⊢ -(↑(rexp (-x✝)) * ↑x✝ ^ s) = (-fun x => ↑(rexp (-x)) * ↑x ^ (s + 1 - 1)) x✝

Tactic:
simp only [ofReal_exp, ofReal_neg, add_sub_cancel_right]

Result:
case h.e'_3.h
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x✝ : ℝ
⊢ -(cexp (-↑x✝) * ↑x✝ ^ s) = (-fun x => cexp (-↑x) * ↑x ^ s) x✝

Proof state:
case h.e'_3.h
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x✝ : ℝ
⊢ -(cexp (-↑x✝) * ↑x✝ ^ s) = (-fun x => cexp (-↑x) * ↑x ^ s) x✝

Tactic:
rfl

Result:
no goals

Proof state:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s)) volume 0 X

Tactic:
convert (Gamma_integrand_intervalIntegrable (s + 1) _ hX).neg

Result:
case h.e'_3.h
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
x✝ : ℝ
⊢ -(↑(rexp (-x✝)) * ↑x✝ ^ s) = (-fun x => ↑(rexp (-x)) * ↑x ^ (s + 1 - 1)) x✝

s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ 0 < (s + 1).re

Proof state:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ 0 < s.re + 1

Tactic:
linarith

Result:
no goals

Proof state:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ 0 < (s + 1).re

Tactic:
simp only [add_re, one_re]

Result:
s : ℂ
hs : 0 < s.re
X : ℝ
hX : 0 ≤ X
⊢ 0 < s.re + 1
-- Mathlib/Algebra/Order/Field/Power.lean
theorem Even.zpow_pos_iff (hn : Even n) (h : n ≠ 0) : 0 < a ^ n ↔ a ≠ 0

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
k : ℤ
h : k + k ≠ 0
⊢ k ≠ 0

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
n : ℤ
hn : Even n
h : n ≠ 0
⊢ 0 < a ^ n ↔ a ≠ 0

Tactic:
obtain ⟨k, rfl⟩ := hn

Result:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a : α
k : ℤ
h : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrderedField α
a : α
k : ℤ
h : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0

Tactic:
rw [zpow_add' (by simp [em']), mul_self_pos, zpow_ne_zero_iff (by simpa using h)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
k : ℤ
h : k + k ≠ 0
⊢ a ≠ 0 ∨ k + k ≠ 0 ∨ k = 0 ∧ k = 0

Tactic:
simp [em']

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
protected lemma pos_iff_ne_zero : 0 < p ↔ p ≠ 0

Proof state:
p : DyckWord
⊢ 0 < p ↔ p ≠ 0

Tactic:
rw [ne_comm, iff_comm, ne_iff_lt_iff_le]

Result:
p : DyckWord
⊢ 0 ≤ p

Proof state:
p : DyckWord
⊢ 0 ≤ p

Tactic:
exact DyckWord.zero_le p

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mdifferentiable_prod_module_iff (f : M → F₁ × F₂) :
    MDifferentiable I 𝓘(𝕜, F₁ × F₂) f ↔
      MDifferentiable I 𝓘(𝕜, F₁) (Prod.fst ∘ f) ∧ MDifferentiable I 𝓘(𝕜, F₂) (Prod.snd ∘ f)

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
f : M → F₁ × F₂
⊢ MDifferentiable I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) f ↔
    MDifferentiable I 𝓘(𝕜, F₁) (Prod.fst ∘ f) ∧ MDifferentiable I 𝓘(𝕜, F₂) (Prod.snd ∘ f)

Tactic:
exact mdifferentiable_prod_iff f

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
f : M → F₁ × F₂
⊢ MDifferentiable I 𝓘(𝕜, F₁ × F₂) f ↔
    MDifferentiable I 𝓘(𝕜, F₁) (Prod.fst ∘ f) ∧ MDifferentiable I 𝓘(𝕜, F₂) (Prod.snd ∘ f)

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

Result:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
f : M → F₁ × F₂
⊢ MDifferentiable I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) f ↔
    MDifferentiable I 𝓘(𝕜, F₁) (Prod.fst ∘ f) ∧ MDifferentiable I 𝓘(𝕜, F₂) (Prod.snd ∘ f)
-- Mathlib/Data/Set/Lattice.lean
theorem iInter₂_eq_empty_iff {s : ∀ i, κ i → Set α} :
    ⋂ (i) (j), s i j = ∅ ↔ ∀ a, ∃ i j, a ∉ s i j

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ ⋂ i, ⋂ j, s i j = ∅ ↔ ∀ (a : α), ∃ i j, a ∉ s i j

Tactic:
simp only [eq_empty_iff_forall_not_mem, mem_iInter, not_forall]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_addX : (W'.map f).toAffine.addX (f x₁) (f x₂) (f ℓ) = f (W'.addX x₁ x₂ ℓ)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x₁ x₂ ℓ : R
⊢ (map W' f).toAffine.addX (f x₁) (f x₂) (f ℓ) = f (W'.addX x₁ x₂ ℓ)

Tactic:
simp only [addX]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x₁ x₂ ℓ : R
⊢ f ℓ ^ 2 + (map W' f).toAffine.a₁ * f ℓ - (map W' f).toAffine.a₂ - f x₁ - f x₂ =
    f (ℓ ^ 2 + W'.a₁ * ℓ - W'.a₂ - x₁ - x₂)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x₁ x₂ ℓ : R
⊢ f ℓ ^ 2 + (map W' f).toAffine.a₁ * f ℓ - (map W' f).toAffine.a₂ - f x₁ - f x₂ =
    f (ℓ ^ 2 + W'.a₁ * ℓ - W'.a₂ - x₁ - x₂)

Tactic:
map_simp

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem psumPart_indiscrete {n : ℕ} (npos : n ≠ 0) :
    psumPart σ R (.indiscrete n) = psum σ R n

Proof state:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
n : ℕ
npos : n ≠ 0
⊢ psumPart σ R (Nat.Partition.indiscrete n) = psum σ R n

Tactic:
simp [psumPart, npos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem getElem_zipWith {f : α → β → γ} {l : List α} {l' : List β}
    {i : Nat} {h : i < (zipWith f l l').length} :
    (zipWith f l l')[i] =
      f (l[i]'(lt_length_left_of_zipWith h))
        (l'[i]'(lt_length_right_of_zipWith h))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
i : Nat
h : i < (zipWith f l l').length
⊢ some l'[i] = some l'[i] ∧ f l[i] l'[i] = f l[i] l'[i]

α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
i : Nat
h : i < (zipWith f l l').length
⊢ i < l'.length

Tactic:
exact ⟨rfl, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
i : Nat
h : i < (zipWith f l l').length
⊢ l[i]? = some l[i]

Tactic:
rw [getElem?_eq_getElem]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
i : Nat
h : i < (zipWith f l l').length
⊢ ∃ x y, l[i]? = some x ∧ l'[i]? = some y ∧ f x y = f l[i] l'[i]

Tactic:
exact
  ⟨l[i]'(lt_length_left_of_zipWith h), l'[i]'(lt_length_right_of_zipWith h),
    by rw [getElem?_eq_getElem], by rw [getElem?_eq_getElem]; exact ⟨rfl, rfl⟩⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
i : Nat
h : i < (zipWith f l l').length
⊢ (zipWith f l l')[i] = f l[i] l'[i]

Tactic:
rw [← Option.some_inj, ← getElem?_eq_getElem, getElem?_zipWith_eq_some]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
i : Nat
h : i < (zipWith f l l').length
⊢ ∃ x y, l[i]? = some x ∧ l'[i]? = some y ∧ f x y = f l[i] l'[i]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
i : Nat
h : i < (zipWith f l l').length
⊢ l'[i]? = some l'[i] ∧ f l[i] l'[i] = f l[i] l'[i]

Tactic:
rw [getElem?_eq_getElem]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
i : Nat
h : i < (zipWith f l l').length
⊢ some l'[i] = some l'[i] ∧ f l[i] l'[i] = f l[i] l'[i]

α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
i : Nat
h : i < (zipWith f l l').length
⊢ i < l'.length
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem mem_span_insert {y} :
    x ∈ span R (insert y s) ↔ ∃ a : R, ∃ z ∈ span R s, x = a • y + z

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
s : Set M
y : M
⊢ x ∈ span R (insert y s) ↔ ∃ a, ∃ z ∈ span R s, x = a • y + z

Tactic:
simp [span_insert, mem_sup, mem_span_singleton, eq_comm (a := x)]

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem IsLindelof.inter_right (hs : IsLindelof s) (ht : IsClosed t) : IsLindelof (s ∩ t)

Proof state:
case intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
x : X
hsx : x ∈ s
hx : ClusterPt x f
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
have hxt : x ∈ t := ht.mem_of_nhdsWithin_neBot <| hx.mono hstf.2

Result:
case intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
x : X
hsx : x ∈ s
hx : ClusterPt x f
hxt : x ∈ t
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
obtain ⟨x, hsx, hx⟩ : ∃ x ∈ s, ClusterPt x f := hs hstf.1

Result:
case intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
x : X
hsx : x ∈ s
hx : ClusterPt x f
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
hstf : f ≤ 𝓟 (s ∩ t)
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
rw [← inf_principal, le_inf_iff] at hstf

Result:
X : Type u
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Proof state:
case intro.intro
X : Type u
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
hstf : f ≤ 𝓟 s ∧ f ≤ 𝓟 t
x : X
hsx : x ∈ s
hx : ClusterPt x f
hxt : x ∈ t
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
exact ⟨x, ⟨hsx, hxt⟩, hx⟩

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed t
⊢ IsLindelof (s ∩ t)

Tactic:
intro f hnf _ hstf

Result:
X : Type u
inst✝¹ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsClosed t
f : Filter X
hnf : f.NeBot
inst✝ : CountableInterFilter f
hstf : f ≤ 𝓟 (s ∩ t)
⊢ ∃ x ∈ s ∩ t, ClusterPt x f
-- Mathlib/Topology/Basic.lean
theorem continuousAt_congr {g : X → Y} (h : f =ᶠ[𝓝 x] g) :
    ContinuousAt f x ↔ ContinuousAt g x

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x : X
g : X → Y
h : f =ᶠ[𝓝 x] g
⊢ ContinuousAt f x ↔ ContinuousAt g x

Tactic:
simp only [ContinuousAt, tendsto_congr' h, h.eq_of_nhds]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
lemma hasSmallLocalizedHom_iff_source {X' : C} (f : X ⟶  X') (hf : W f) (Y : C) :
    HasSmallLocalizedHom.{w} W X Y ↔ HasSmallLocalizedHom.{w} W X' Y

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X X' : C
f : X ⟶ X'
hf : W f
Y : C
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X' Y

Tactic:
simp only [hasSmallLocalizedHom_iff W W.Q]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X X' : C
f : X ⟶ X'
hf : W f
Y : C
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X X' : C
f : X ⟶ X'
hf : W f
Y : C
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y)

Tactic:
exact small_congr (Iso.homCongr (Localization.isoOfHom W.Q W f hf) (Iso.refl _))

Result:
no goals