harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Nodup.lean
theorem count_eq_of_nodup [DecidableEq α] {a : α} {l : List α} (d : Nodup l) :
    count a l = if a ∈ l then 1 else 0

Proof state:
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
d : l.Nodup
⊢ count a l = if a ∈ l then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
d : l.Nodup
h : a ∈ l
⊢ count a l = 1

case neg
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
d : l.Nodup
h : a ∉ l
⊢ count a l = 0

Proof state:
case neg
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
d : l.Nodup
h : a ∉ l
⊢ count a l = 0

Tactic:
exact count_eq_zero_of_not_mem h

Result:
no goals

Proof state:
case pos
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
d : l.Nodup
h : a ∈ l
⊢ count a l = 1

Tactic:
exact count_eq_one_of_mem d h

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Module.lean
theorem ContinuousLinearEquiv.hasSum {f : ι → M} (e : M ≃SL[σ] M₂) {y : M₂} :
    HasSum (fun b : ι ↦ e (f b)) y ↔ HasSum f (e.symm y) :=
  ⟨fun h ↦ by simpa only [e.symm.coe_coe, e.symm_apply_apply] using h.mapL (e.symm : M₂ →SL[σ'] M),
    fun h ↦ by simpa only [e.coe_coe, e.apply_symm_apply] using (e : M →SL[σ] M₂).hasSum h⟩

Proof state:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum (fun b => e (f b)) y
⊢ HasSum f (e.symm y)

Tactic:
simpa only [e.symm.coe_coe, e.symm_apply_apply] using h.mapL (e.symm : M₂ →SL[σ'] M)

Result:
no goals

Proof state:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R₂ M₂
inst✝³ : TopologicalSpace M
inst✝² : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomInvPair σ' σ
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum f (e.symm y)
⊢ HasSum (fun b => e (f b)) y

Tactic:
simpa only [e.coe_coe, e.apply_symm_apply] using (e : M →SL[σ] M₂).hasSum h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_flatten {L : List (List α)} : (flatten L).head? = L.findSome? fun l => l.head?

Proof state:
α : Type u_1
L : List (List α)
⊢ L.flatten.head? = findSome? (fun l => l.head?) L

Tactic:
induction L with
| nil => rfl
| cons =>
  simp only [findSome?_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
⊢ [].flatten.head? = findSome? (fun l => l.head?) []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : tail✝.flatten.head? = findSome? (fun l => l.head?) tail✝
⊢ (head✝ :: tail✝).flatten.head? = findSome? (fun l => l.head?) (head✝ :: tail✝)

Tactic:
simp only [findSome?_cons]

Result:
case cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : tail✝.flatten.head? = findSome? (fun l => l.head?) tail✝
⊢ (head✝ :: tail✝).flatten.head? =
    match head✝.head? with
    | some b => some b
    | none => findSome? (fun l => l.head?) tail✝

Proof state:
case cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : tail✝.flatten.head? = findSome? (fun l => l.head?) tail✝
⊢ (head✝ :: tail✝).flatten.head? =
    match head✝.head? with
    | some b => some b
    | none => findSome? (fun l => l.head?) tail✝

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
lemma ContDiffWithinAt.analyticWithinAt (h : ContDiffWithinAt 𝕜 ω f s x) :
    AnalyticWithinAt 𝕜 f s x

Proof state:
case intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : AnalyticOn 𝕜 f u
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
have xu : x ∈ u := mem_of_mem_nhdsWithin (by simp) hu

Result:
case intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : AnalyticOn 𝕜 f u
xu : x ∈ u
⊢ AnalyticWithinAt 𝕜 f s x

Proof state:
case intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : AnalyticOn 𝕜 f u
xu : x ∈ u
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
exact (hf x xu).mono_of_mem_nhdsWithin (nhdsWithin_mono _ (subset_insert _ _) hu)

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f s x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
obtain ⟨u, hu, hf⟩ := h.analyticOn

Result:
case intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : AnalyticOn 𝕜 f u
⊢ AnalyticWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
h : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
hf : AnalyticOn 𝕜 f u
⊢ x ∈ insert x s

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem mem_interior : x ∈ interior s ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t

Proof state:
X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
⊢ x ∈ interior s ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t

Tactic:
simp only [interior, mem_sUnion, mem_setOf_eq, and_assoc, and_left_comm]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eqToHom_map_comp (F : C ⥤ D) {X Y Z : C} (p : X = Y) (q : Y = Z) :
    F.map (eqToHom p) ≫ F.map (eqToHom q) = F.map (eqToHom <| p.trans q)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
p : X = Y
q : Y = Z
⊢ F.map (eqToHom p) ≫ F.map (eqToHom q) = F.map (eqToHom ⋯)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem eventually_imp : (∀ᶠ x in f, p x → q x) ↔ (∀ᶠ x in f, p x) → ∀ᶠ x in f, q x

Proof state:
α : Type u
f : Ultrafilter α
p q : α → Prop
⊢ (∀ᶠ (x : α) in ↑f, p x → q x) ↔ (∀ᶠ (x : α) in ↑f, p x) → ∀ᶠ (x : α) in ↑f, q x

Tactic:
simp only [imp_iff_not_or, eventually_or, eventually_not]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/MidpointZero.lean
theorem homothety_one_half {k : Type*} {V P : Type*} [Field k] [CharZero k] [AddCommGroup V]
    [Module k V] [AddTorsor V P] (a b : P) : homothety a (1 / 2 : k) b = midpoint k a b

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Field k
inst✝³ : CharZero k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AddTorsor V P
a b : P
⊢ (homothety a (1 / 2)) b = midpoint k a b

Tactic:
rw [one_div, homothety_inv_two]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem self_mem_range_succ (n : Nat) : n ∈ range (n + 1)

Proof state:
n : Nat
⊢ n ∈ range (n + 1)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENat/Lattice.lean
lemma iSup_add_iSup (h : ∀ i j, ∃ k, f i + g j ≤ f k + g k) : iSup f + iSup g = ⨆ i, f i + g i

Proof state:
case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
i j : ι
⊢ f i + g j ≤ ⨆ i, f i + g i

Tactic:
rcases h i j with ⟨k, hk⟩

Result:
case inr.intro
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
i j k : ι
hk : f i + g j ≤ f k + g k
⊢ f i + g j ≤ ⨆ i, f i + g i

Proof state:
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : IsEmpty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

Proof state:
case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
refine le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))

Result:
case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g ≤ ⨆ i, f i + g i

Proof state:
case inl
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : IsEmpty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
simp only [iSup_of_empty, bot_eq_zero, zero_add]

Result:
no goals

Proof state:
case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g ≤ ⨆ i, f i + g i

Tactic:
refine iSup_add_iSup_le fun i j => ?_

Result:
case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
i j : ι
⊢ f i + g j ≤ ⨆ i, f i + g i

Proof state:
case inr.intro
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
i j k : ι
hk : f i + g j ≤ f k + g k
⊢ f i + g j ≤ ⨆ i, f i + g i

Tactic:
exact le_iSup_of_le k hk

Result:
no goals
-- Mathlib/Topology/Sets/Closeds.lean
theorem iInf_def {ι} (s : ι → Closeds α) :
    ⨅ i, s i = ⟨⋂ i, s i, isClosed_iInter fun i => (s i).2⟩

Proof state:
case h
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
⊢ ↑(⨅ i, s i) = ↑{ carrier := ⋂ i, ↑(s i), closed' := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
⊢ ⨅ i, s i = { carrier := ⋂ i, ↑(s i), closed' := ⋯ }

Tactic:
ext1

Result:
case h
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_4
s : ι → Closeds α
⊢ ↑(⨅ i, s i) = ↑{ carrier := ⋂ i, ↑(s i), closed' := ⋯ }
-- Mathlib/NumberTheory/SumTwoSquares.lean
theorem ZMod.isSquare_neg_one_mul {m n : ℕ} (hc : m.Coprime n) (hm : IsSquare (-1 : ZMod m))
    (hn : IsSquare (-1 : ZMod n)) : IsSquare (-1 : ZMod (m * n))

Proof state:
case intro
m n : ℕ
hc : m.Coprime n
hn : IsSquare (-1)
x : ZMod m
hx : -1 = x * x
⊢ IsSquare (-1, -1)

Tactic:
obtain ⟨y, hy⟩ := hn

Result:
case intro.intro
m n : ℕ
hc : m.Coprime n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
⊢ IsSquare (-1, -1)

Proof state:
case intro.intro
m n : ℕ
hc : m.Coprime n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
⊢ IsSquare (-1, -1)

Tactic:
rw [hx, hy]

Result:
case intro.intro
m n : ℕ
hc : m.Coprime n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
⊢ IsSquare (x * x, y * y)

Proof state:
case intro.intro
m n : ℕ
hc : m.Coprime n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
⊢ IsSquare (x * x, y * y)

Tactic:
exact ⟨(x, y), rfl⟩

Result:
no goals

Proof state:
m n : ℕ
hc : m.Coprime n
hm : IsSquare (-1)
hn : IsSquare (-1)
⊢ IsSquare (-1)

Tactic:
have : IsSquare (-1 : ZMod m × ZMod n) := by
  rw [show (-1 : ZMod m × ZMod n) = ((-1 : ZMod m), (-1 : ZMod n)) from rfl]
  obtain ⟨x, hx⟩ := hm
  obtain ⟨y, hy⟩ := hn
  rw [hx, hy]
  exact ⟨(x, y), rfl⟩

Result:
m n : ℕ
hc : m.Coprime n
hm : IsSquare (-1)
hn : IsSquare (-1)
this : IsSquare (-1)
⊢ IsSquare (-1)

Proof state:
m n : ℕ
hc : m.Coprime n
hm : IsSquare (-1)
hn : IsSquare (-1)
⊢ IsSquare (-1)

Tactic:
rw [show (-1 : ZMod m × ZMod n) = ((-1 : ZMod m), (-1 : ZMod n)) from rfl]

Result:
m n : ℕ
hc : m.Coprime n
hm : IsSquare (-1)
hn : IsSquare (-1)
⊢ IsSquare (-1, -1)

Proof state:
m n : ℕ
hc : m.Coprime n
hm : IsSquare (-1)
hn : IsSquare (-1)
⊢ IsSquare (-1, -1)

Tactic:
obtain ⟨x, hx⟩ := hm

Result:
case intro
m n : ℕ
hc : m.Coprime n
hn : IsSquare (-1)
x : ZMod m
hx : -1 = x * x
⊢ IsSquare (-1, -1)

Proof state:
m n : ℕ
hc : m.Coprime n
hm : IsSquare (-1)
hn : IsSquare (-1)
this : IsSquare (-1)
⊢ IsSquare (-1)

Tactic:
simpa only [RingEquiv.map_neg_one] using this.map (ZMod.chineseRemainder hc).symm

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean
/-- The power series expansion of `Complex.sinh`. -/
lemma hasSum_sinh (z : ℂ) : HasSum (fun n ↦ z ^ (2 * n + 1) / ↑(2 * n + 1)!) (sinh z)

Proof state:
z : ℂ
⊢ HasSum (fun n => z ^ (2 * n + 1) / ↑(2 * n + 1)!) (sinh z)

Tactic:
simpa [mul_assoc, sin_mul_I, neg_pow z, pow_add, pow_mul, neg_mul, neg_div]
  using (hasSum_sin' (z * I)).mul_right (-I)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem map_add_range' (a) : ∀ s n step, map (a + ·) (range' s n step) = range' (a + s) n step
  | _, 0, _ => rfl
  | s, n + 1, step => by simp [range', map_add_range' _ (s + step) n step, Nat.add_assoc]

Proof state:
a s n step : Nat
⊢ map (fun x => a + x) (range' s (n + 1) step) = range' (a + s) (n + 1) step

Tactic:
simp [range', map_add_range' _ (s + step) n step, Nat.add_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem _root_.MeasurableEmbedding.integrable_map_iff {f : α → δ} (hf : MeasurableEmbedding f)
    {g : δ → β} : Integrable g (Measure.map f μ) ↔ Integrable (g ∘ f) μ

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace δ
inst✝ : NormedAddCommGroup β
f : α → δ
hf : MeasurableEmbedding f
g : δ → β
⊢ Integrable g (Measure.map f μ) ↔ Integrable (g ∘ f) μ

Tactic:
simp_rw [← memLp_one_iff_integrable]

Result:
α : Type u_1
β : Type u_2
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace δ
inst✝ : NormedAddCommGroup β
f : α → δ
hf : MeasurableEmbedding f
g : δ → β
⊢ MemLp g 1 (Measure.map f μ) ↔ MemLp (g ∘ f) 1 μ

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MeasurableSpace δ
inst✝ : NormedAddCommGroup β
f : α → δ
hf : MeasurableEmbedding f
g : δ → β
⊢ MemLp g 1 (Measure.map f μ) ↔ MemLp (g ∘ f) 1 μ

Tactic:
exact hf.memLp_map_measure_iff

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma le_of_isAffine [IsAffine X] {I J : IdealSheafData X}
    (H : I.ideal ⟨⊤, isAffineOpen_top X⟩ ≤ J.ideal ⟨⊤, isAffineOpen_top X⟩) : I ≤ J

Proof state:
X : Scheme
inst✝ : IsAffine X
I J : X.IdealSheafData
H : I.ideal ⟨⊤, ⋯⟩ ≤ J.ideal ⟨⊤, ⋯⟩
U : ↑X.affineOpens
⊢ I.ideal U ≤ J.ideal U

Tactic:
rw [← map_ideal (U := U) (V := ⟨⊤, isAffineOpen_top X⟩) I (le_top (a := U.1)),
  ← map_ideal (U := U) (V := ⟨⊤, isAffineOpen_top X⟩) J (le_top (a := U.1))]

Result:
X : Scheme
inst✝ : IsAffine X
I J : X.IdealSheafData
H : I.ideal ⟨⊤, ⋯⟩ ≤ J.ideal ⟨⊤, ⋯⟩
U : ↑X.affineOpens
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal ⟨⊤, ⋯⟩) ≤
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (J.ideal ⟨⊤, ⋯⟩)

Proof state:
X : Scheme
inst✝ : IsAffine X
I J : X.IdealSheafData
H : I.ideal ⟨⊤, ⋯⟩ ≤ J.ideal ⟨⊤, ⋯⟩
⊢ I ≤ J

Tactic:
intro U

Result:
X : Scheme
inst✝ : IsAffine X
I J : X.IdealSheafData
H : I.ideal ⟨⊤, ⋯⟩ ≤ J.ideal ⟨⊤, ⋯⟩
U : ↑X.affineOpens
⊢ I.ideal U ≤ J.ideal U

Proof state:
X : Scheme
inst✝ : IsAffine X
I J : X.IdealSheafData
H : I.ideal ⟨⊤, ⋯⟩ ≤ J.ideal ⟨⊤, ⋯⟩
U : ↑X.affineOpens
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal ⟨⊤, ⋯⟩) ≤
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (J.ideal ⟨⊤, ⋯⟩)

Tactic:
exact Ideal.map_mono H

Result:
no goals
-- Mathlib/Algebra/Lie/Semisimple/Basic.lean
lemma LieModule.nontrivial_of_isIrreducible [LieModule.IsIrreducible R L M] : Nontrivial M where
  exists_pair_ne

Proof state:
case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsIrreducible R L M
aux : ∀ (x y : M), x = y
m : M
⊢ m ∈ ⊥ ↔ m ∈ ⊤

Tactic:
simpa using aux m 0

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsIrreducible R L M
⊢ ∃ x y, x ≠ y

Tactic:
have aux : (⊥ : LieSubmodule R L M) ≠ ⊤ := bot_ne_top

Result:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsIrreducible R L M
aux : ⊥ ≠ ⊤
⊢ ∃ x y, x ≠ y

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsIrreducible R L M
aux : ∀ (x y : M), x = y
⊢ ⊥ = ⊤

Tactic:
ext m

Result:
case h
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsIrreducible R L M
aux : ∀ (x y : M), x = y
m : M
⊢ m ∈ ⊥ ↔ m ∈ ⊤

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsIrreducible R L M
aux : ⊥ ≠ ⊤
⊢ ∃ x y, x ≠ y

Tactic:
contrapose! aux

Result:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : IsIrreducible R L M
aux : ∀ (x y : M), x = y
⊢ ⊥ = ⊤
-- Mathlib/Order/Filter/Basic.lean
theorem eq_biInf_of_mem_iff_exists_mem {f : ι → Filter α} {p : ι → Prop} {l : Filter α}
    (h : ∀ {s}, s ∈ l ↔ ∃ i, p i ∧ s ∈ f i) : l = ⨅ (i) (_ : p i), f i

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
p : ι → Prop
l : Filter α
h : ∀ {s : Set α}, s ∈ l ↔ ∃ i, p i ∧ s ∈ f i
⊢ l = ⨅ i, ⨅ (_ : p i), f i

Tactic:
rw [iInf_subtype']

Result:
α : Type u
ι : Sort x
f : ι → Filter α
p : ι → Prop
l : Filter α
h : ∀ {s : Set α}, s ∈ l ↔ ∃ i, p i ∧ s ∈ f i
⊢ l = ⨅ x, f ↑x

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
p : ι → Prop
l : Filter α
h : ∀ {s : Set α}, s ∈ l ↔ ∃ i, p i ∧ s ∈ f i
⊢ l = ⨅ x, f ↑x

Tactic:
exact eq_iInf_of_mem_iff_exists_mem fun {_} => by simp only [Subtype.exists, h, exists_prop]

Result:
no goals

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
p : ι → Prop
l : Filter α
h : ∀ {s : Set α}, s ∈ l ↔ ∃ i, p i ∧ s ∈ f i
x✝ : Set α
⊢ x✝ ∈ l ↔ ∃ i, x✝ ∈ f ↑i

Tactic:
simp only [Subtype.exists, h, exists_prop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_add : eval .add = ((· + ·) : BitVec w → BitVec w → BitVec w)

Proof state:
w : Nat
⊢ add.eval = fun x1 x2 => x1 + x2

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem swap_def (a : Array α) (i j : Nat) (hi hj) :
    a.swap i j hi hj = (a.set i a[j]).set j a[i] (by simpa using hj)

Proof state:
α : Type ?u.88
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ j < (a.set i a[j] hi).size

Tactic:
simpa using hj

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ a.swap i j hi hj = (a.set i a[j] hi).set j a[i] ⋯

Tactic:
simp [swap]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_inf_distrib_right (s : Finset ι) (f : ι → α) (a : α) :
    s.sup f ⊓ a = s.sup fun i => f i ⊓ a

Proof state:
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (s.sup fun i => a ⊓ f i) = s.sup fun i => f i ⊓ a

Tactic:
simp_rw [_root_.inf_comm]

Result:
no goals

Proof state:
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ s.sup f ⊓ a = s.sup fun i => f i ⊓ a

Tactic:
rw [_root_.inf_comm, s.sup_inf_distrib_left]

Result:
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ (s.sup fun i => a ⊓ f i) = s.sup fun i => f i ⊓ a
-- Mathlib/Topology/Basic.lean
theorem nhds_basis_opens (x : X) :
    (𝓝 x).HasBasis (fun s : Set X => x ∈ s ∧ IsOpen s) fun s => s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ (⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, 𝓟 s).HasBasis (fun s => x ∈ s ∧ IsOpen s) fun s => s

Tactic:
exact hasBasis_biInf_principal
  (fun s ⟨has, hs⟩ t ⟨hat, ht⟩ =>
    ⟨s ∩ t, ⟨⟨has, hat⟩, IsOpen.inter hs ht⟩, ⟨inter_subset_left, inter_subset_right⟩⟩)
  ⟨univ, ⟨mem_univ x, isOpen_univ⟩⟩

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ (𝓝 x).HasBasis (fun s => x ∈ s ∧ IsOpen s) fun s => s

Tactic:
rw [nhds_def]

Result:
X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ (⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, 𝓟 s).HasBasis (fun s => x ∈ s ∧ IsOpen s) fun s => s
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
protected lemma LinearMapClass.map_smul {R M M₂ : outParam Type*} [Semiring R] [AddCommMonoid M]
    [AddCommMonoid M₂] [Module R M] [Module R M₂]
    {F : Type*} [FunLike F M M₂] [LinearMapClass F R M M₂] (f : F) (r : R) (x : M) :
    f (r • x) = r • f x

Proof state:
R : outParam (Type u_14)
M : outParam (Type u_15)
M₂ : outParam (Type u_16)
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R M₂
F : Type u_17
inst✝¹ : FunLike F M M₂
inst✝ : LinearMapClass F R M M₂
f : F
r : R
x : M
⊢ f (r • x) = r • f x

Tactic:
rw [_root_.map_smul]

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem funInvIdAssoc_hom_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
    (funInvIdAssoc e F).hom.app X = F.map (e.unitInv.app X)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : C ⥤ E
X : C
⊢ (e.funInvIdAssoc F).hom.app X = F.map (e.unitInv.app X)

Tactic:
dsimp [funInvIdAssoc]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : C ⥤ E
X : C
⊢ 𝟙 (F.obj (e.inverse.obj (e.functor.obj X))) ≫ F.map (e.unitIso.inv.app X) ≫ 𝟙 (F.obj X) = F.map (e.unitInv.app X)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
e : C ≌ D
F : C ⥤ E
X : C
⊢ 𝟙 (F.obj (e.inverse.obj (e.functor.obj X))) ≫ F.map (e.unitIso.inv.app X) ≫ 𝟙 (F.obj X) = F.map (e.unitInv.app X)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Field/Rat.lean
lemma inv_def (q : ℚ≥0) : q⁻¹ = divNat q.den q.num

Proof state:
q : ℚ≥0
⊢ q⁻¹ = divNat q.den q.num

Tactic:
ext

Result:
case a
q : ℚ≥0
⊢ ↑q⁻¹ = ↑(divNat q.den q.num)

Proof state:
case a
q : ℚ≥0
⊢ ↑q⁻¹ = ↑(divNat q.den q.num)

Tactic:
simp [Rat.inv_def', num_coe, den_coe]

Result:
no goals