harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem Basis.exists_opNNNorm_le {ι : Type*} [Finite ι] (v : Basis ι 𝕜 E) :
    ∃ C > (0 : ℝ≥0), ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ i, ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M

Proof state:
case intro
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
val✝ : Fintype ι
⊢ ∃ C > 0, ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M

Tactic:
exact
  ⟨max (Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖₊) 1,
    zero_lt_one.trans_le (le_max_right _ _), fun {u} M hu =>
    (v.opNNNorm_le M hu).trans <| mul_le_mul_of_nonneg_right (le_max_left _ _) (zero_le M)⟩

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
⊢ ∃ C > 0, ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M

Tactic:
cases nonempty_fintype ι

Result:
case intro
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type w
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
v : Basis ι 𝕜 E
val✝ : Fintype ι
⊢ ∃ C > 0, ∀ {u : E →L[𝕜] F} (M : ℝ≥0), (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ C * M
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_smul [NormedSpace 𝕜 E] (c : 𝕜) (f : α → E) (m : MeasurableSpace α) :
    μ[c • f|m] =ᵐ[μ] c • μ[f|m]

Proof state:
case pos
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ ∀ᵐ (x : α) ∂μ, (μ[f|m]) x = ↑↑(condExpL1 hm μ f) x → ↑↑(c • condExpL1 hm μ f) x = (c • μ[f|m]) x

Tactic:
refine (coeFn_smul c (condExpL1 hm μ f)).mono fun x hx1 hx2 => ?_

Result:
case pos
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
x : α
hx1 : ↑↑(c • condExpL1 hm μ f) x = (c • ↑↑(condExpL1 hm μ f)) x
hx2 : (μ[f|m]) x = ↑↑(condExpL1 hm μ f) x
⊢ ↑↑(c • condExpL1 hm μ f) x = (c • μ[f|m]) x

Proof state:
case neg
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
hm : ¬m ≤ m₀
⊢ μ[c • f|m] =ᶠ[ae μ] c • μ[f|m]

Tactic:
simp_rw [condExp_of_not_le hm]

Result:
case neg
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
hm : ¬m ≤ m₀
⊢ 0 =ᶠ[ae μ] c • 0

Proof state:
case pos
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ ↑↑(c • condExpL1 hm μ f) =ᶠ[ae μ] c • μ[f|m]

Tactic:
refine (condExp_ae_eq_condExpL1 hm f).mp ?_

Result:
case pos
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst✝⁴ : RCLike 𝕜
m₀ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
f : α → E
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ ∀ᵐ (x : α) ∂μ, (μ[f|m]) x = ↑↑(condExpL1 hm μ f) x → ↑↑(c • condExpL1 hm μ f) x = (c • μ[f|m]) x
-- Mathlib/Data/List/SplitOn.lean
theorem splitOnP_first (h : ∀ x ∈ xs, ¬p x) (sep : α) (hsep : p sep) (as : List α) :
    (xs ++ sep :: as).splitOnP p = xs :: as.splitOnP p

Proof state:
case nil
α : Type u_1
p : α → Bool
xs : List α
sep : α
hsep : p sep = true
as : List α
h : ∀ (x : α), x ∈ [] → ¬p x = true
⊢ splitOnP p ([] ++ sep :: as) = [] :: splitOnP p as

Tactic:
simp [hsep]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
xs : List α
h : ∀ (x : α), x ∈ xs → ¬p x = true
sep : α
hsep : p sep = true
as : List α
⊢ splitOnP p (xs ++ sep :: as) = xs :: splitOnP p as

Tactic:
induction xs with
| nil => simp [hsep]
| cons hd tl ih => simp [h hd _, ih <| forall_mem_of_forall_mem_cons h]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
xs : List α
sep : α
hsep : p sep = true
as : List α
hd : α
tl : List α
ih : (∀ (x : α), x ∈ tl → ¬p x = true) → splitOnP p (tl ++ sep :: as) = tl :: splitOnP p as
h : ∀ (x : α), x ∈ hd :: tl → ¬p x = true
⊢ splitOnP p (hd :: tl ++ sep :: as) = (hd :: tl) :: splitOnP p as

Tactic:
simp [h hd _, ih <| forall_mem_of_forall_mem_cons h]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
@[simp] lemma append_cast_left {n m} (xs : Fin n → α) (ys : Fin m → α) (n' : ℕ)
    (h : n' = n) :
    Fin.append (xs ∘ Fin.cast h) ys = Fin.append xs ys ∘ (Fin.cast <| by rw [h])

Proof state:
m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Sort u
x : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ i.succ
i : Fin n✝
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
n' : ℕ
h : n' = n
⊢ n' + m = n + m

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Sort u_1
m : ℕ
ys : Fin m → α
n' : ℕ
xs : Fin n' → α
⊢ append (xs ∘ Fin.cast ⋯) ys = append xs ys ∘ Fin.cast ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
n' : ℕ
h : n' = n
⊢ append (xs ∘ Fin.cast h) ys = append xs ys ∘ Fin.cast ⋯

Tactic:
subst h

Result:
α : Sort u_1
m : ℕ
ys : Fin m → α
n' : ℕ
xs : Fin n' → α
⊢ append (xs ∘ Fin.cast ⋯) ys = append xs ys ∘ Fin.cast ⋯
-- Mathlib/CategoryTheory/Endomorphism.lean
theorem isUnit_iff_isIso {C : Type u} [Category.{v} C] {X : C} (f : End X) :
    IsUnit (f : End X) ↔ IsIso f :=
  ⟨fun h => { out := ⟨h.unit.inv, ⟨h.unit.inv_val, h.unit.val_inv⟩⟩ }, fun h =>
    ⟨⟨f, inv f, by simp, by simp⟩, rfl⟩⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
h : IsIso f
⊢ f * inv f = 1

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
h : IsIso f
⊢ inv f * f = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem rpow_logb (hx : 0 < x) : b ^ logb b x = x

Proof state:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
⊢ b ^ logb b x = x

Tactic:
rw [rpow_logb_eq_abs b_pos b_ne_one hx.ne']

Result:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
⊢ |x| = x

Proof state:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : 0 < x
⊢ |x| = x

Tactic:
exact abs_of_pos hx

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem generatePiSystem_measurableSet [M : MeasurableSpace α] {S : Set (Set α)}
    (h_meas_S : ∀ s ∈ S, MeasurableSet s) (t : Set α) (h_in_pi : t ∈ generatePiSystem S) :
    MeasurableSet t

Proof state:
case inter
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ s ∈ S, MeasurableSet s
t s✝ t✝ : Set α
h_s✝ : generatePiSystem S s✝
h_t✝ : generatePiSystem S t✝
h_nonempty✝ : (s✝ ∩ t✝).Nonempty
h_s : MeasurableSet s✝
h_u : MeasurableSet t✝
⊢ MeasurableSet (s✝ ∩ t✝)

Tactic:
apply MeasurableSet.inter h_s h_u

Result:
no goals

Proof state:
case base
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ s ∈ S, MeasurableSet s
t s✝ : Set α
h_s : s✝ ∈ S
⊢ MeasurableSet s✝

Tactic:
apply h_meas_S _ h_s

Result:
no goals

Proof state:
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ s ∈ S, MeasurableSet s
t : Set α
h_in_pi : t ∈ generatePiSystem S
⊢ MeasurableSet t

Tactic:
induction h_in_pi with
| base h_s => apply h_meas_S _ h_s
| inter _ _ _ h_s h_u => apply MeasurableSet.inter h_s h_u

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_set {l : Vector α n} {i : Nat} {h : i < n} {a : α} :
    (l.set i a).mapIdx f = (l.mapIdx f).set i (f i a) (by simpa)

Proof state:
case mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
i : Nat
a : α
l : Array α
h : i < l.size
⊢ mapIdx f ({ toArray := l, size_toArray := ⋯ }.set i a h) =
    (mapIdx f { toArray := l, size_toArray := ⋯ }).set i (f i a) h

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
α✝ : Type u_2
f : Nat → α → α✝
l : Vector α n
i : Nat
h : i < n
a : α
⊢ mapIdx f (l.set i a h) = (mapIdx f l).set i (f i a) h

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
i : Nat
a : α
l : Array α
h : i < l.size
⊢ mapIdx f ({ toArray := l, size_toArray := ⋯ }.set i a h) =
    (mapIdx f { toArray := l, size_toArray := ⋯ }).set i (f i a) h

Proof state:
α : Type ?u.87087
n : Nat
f : Nat → α → ?m.87155
l : Vector α n
i : Nat
h : i < n
a : α
⊢ i < n

Tactic:
simpa

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
lemma diam_eq_zero_of_not_connected (h : ¬G.Connected) : G.diam = 0

Proof state:
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
⊢ G.diam = 0

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h✝ : IsEmpty α
⊢ G.diam = 0

case inr
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h✝ : Nonempty α
⊢ G.diam = 0

Proof state:
case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h✝ : IsEmpty α
⊢ ENat.toNat 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case inr
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h✝ : Nonempty α
⊢ G.diam = 0

Tactic:
rw [diam, ediam_eq_top_of_not_connected h, ENat.toNat_top]

Result:
no goals

Proof state:
case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h✝ : IsEmpty α
⊢ G.diam = 0

Tactic:
rw [diam, ediam, ciSup_of_empty, bot_eq_zero']

Result:
case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h✝ : IsEmpty α
⊢ ENat.toNat 0 = 0
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma hom_inv_apply {R S : RingCat} (e : R ≅ S) (s : S) : e.hom (e.inv s) = s

Proof state:
R S : RingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Catalan.lean
theorem catalan_succ' (n : ℕ) :
    catalan (n + 1) = ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2

Proof state:
n : ℕ
⊢ catalan (n + 1) = ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2

Tactic:
rw [catalan_succ, Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => catalan x * catalan y) n,
  sum_range]

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem max_erase_ne_self {s : Finset α} : (s.erase x).max ≠ x

Proof state:
case neg
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : ¬(s.erase x).Nonempty
⊢ (s.erase x).max ≠ ↑x

Tactic:
rw [not_nonempty_iff_eq_empty.mp s0, max_empty]

Result:
case neg
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : ¬(s.erase x).Nonempty
⊢ ⊥ ≠ ↑x

Proof state:
case pos
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ ↑((s.erase x).max' s0) ≠ ↑x

Tactic:
exact WithBot.coe_eq_coe.not.mpr (max'_erase_ne_self _)

Result:
no goals

Proof state:
case pos
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ (s.erase x).max ≠ ↑x

Tactic:
refine ne_of_eq_of_ne (coe_max' s0).symm ?_

Result:
case pos
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ ↑((s.erase x).max' s0) ≠ ↑x

Proof state:
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
⊢ (s.erase x).max ≠ ↑x

Tactic:
by_cases s0 : (s.erase x).Nonempty

Result:
case pos
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : (s.erase x).Nonempty
⊢ (s.erase x).max ≠ ↑x

case neg
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : ¬(s.erase x).Nonempty
⊢ (s.erase x).max ≠ ↑x

Proof state:
case neg
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : ¬(s.erase x).Nonempty
⊢ ⊥ ≠ ↑x

Tactic:
exact WithBot.bot_ne_coe

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem Topology.IsClosedEmbedding.compactSpace [h : CompactSpace Y] {f : X → Y}
    (hf : IsClosedEmbedding f) : CompactSpace X :=
  ⟨by rw [hf.isInducing.isCompact_iff, image_univ]; exact hf.isClosed_range.isCompact⟩

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact (range f)

Tactic:
exact hf.isClosed_range.isCompact

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact univ

Tactic:
rw [hf.isInducing.isCompact_iff, image_univ]

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact (range f)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range_succ_eq_map (n : Nat) : range (n + 1) = #[0] ++ map succ (range n)

Proof state:
case h₁
n : Nat
⊢ (range (n + 1)).size = (#[0] ++ map succ (range n)).size

Tactic:
simp

Result:
case h₁
n : Nat
⊢ n + 1 = 1 + n

Proof state:
case h₁
n : Nat
⊢ n + 1 = 1 + n

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
⊢ range (n + 1) = #[0] ++ map succ (range n)

Tactic:
ext i h₁ h₂

Result:
case h₁
n : Nat
⊢ (range (n + 1)).size = (#[0] ++ map succ (range n)).size

case h₂
n i : Nat
h₁ : i < (range (n + 1)).size
h₂ : i < (#[0] ++ map succ (range n)).size
⊢ (range (n + 1))[i] = (#[0] ++ map succ (range n))[i]

Proof state:
case h₂
n i : Nat
h₁ : i < (range (n + 1)).size
h₂ : i < (#[0] ++ map succ (range n)).size
⊢ i = if i = 0 then 0 else i - 1 + 1

Tactic:
split <;> omega

Result:
no goals

Proof state:
case h₂
n i : Nat
h₁ : i < (range (n + 1)).size
h₂ : i < (#[0] ++ map succ (range n)).size
⊢ (range (n + 1))[i] = (#[0] ++ map succ (range n))[i]

Tactic:
simp only [getElem_range, getElem_append, size_toArray, List.length_cons, List.length_nil,
  Nat.zero_add, lt_one_iff, List.getElem_toArray, List.getElem_singleton, getElem_map,
  succ_eq_add_one, dite_eq_ite]

Result:
case h₂
n i : Nat
h₁ : i < (range (n + 1)).size
h₂ : i < (#[0] ++ map succ (range n)).size
⊢ i = if i = 0 then 0 else i - 1 + 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem append_subset {l₁ l₂ l : List α} :
    l₁ ++ l₂ ⊆ l ↔ l₁ ⊆ l ∧ l₂ ⊆ l

Proof state:
α : Type u_1
l₁ l₂ l : List α
⊢ l₁ ++ l₂ ⊆ l ↔ l₁ ⊆ l ∧ l₂ ⊆ l

Tactic:
simp [subset_def, or_imp, forall_and]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem le_of_nhds_le_nhds (h : ∀ x, @nhds α t₁ x ≤ @nhds α t₂ x) : t₁ ≤ t₂ := fun s => by
  rw [@isOpen_iff_mem_nhds _ _ t₁, @isOpen_iff_mem_nhds α _ t₂]
  exact fun hs a ha => h _ (hs _ ha)

Proof state:
α : Type u_1
t₁ t₂ : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
s : Set α
⊢ (∀ x ∈ s, s ∈ 𝓝 x) → ∀ x ∈ s, s ∈ 𝓝 x

Tactic:
exact fun hs a ha => h _ (hs _ ha)

Result:
no goals

Proof state:
α : Type u_1
t₁ t₂ : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
s : Set α
⊢ IsOpen s → IsOpen s

Tactic:
rw [@isOpen_iff_mem_nhds _ _ t₁, @isOpen_iff_mem_nhds α _ t₂]

Result:
α : Type u_1
t₁ t₂ : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
s : Set α
⊢ (∀ x ∈ s, s ∈ 𝓝 x) → ∀ x ∈ s, s ∈ 𝓝 x
-- Mathlib/Data/List/TakeDrop.lean
theorem length_dropSlice_lt (i j : ℕ) (hj : 0 < j) (xs : List α) (hi : i < xs.length) :
    (List.dropSlice i j xs).length < xs.length

Proof state:
α : Type u
i j : ℕ
hj : 0 < j
xs : List α
hi : i < xs.length
⊢ (dropSlice i j xs).length < xs.length

Tactic:
simp

Result:
α : Type u
i j : ℕ
hj : 0 < j
xs : List α
hi : i < xs.length
⊢ xs.length - min j (xs.length - i) < xs.length

Proof state:
α : Type u
i j : ℕ
hj : 0 < j
xs : List α
hi : i < xs.length
⊢ xs.length - min j (xs.length - i) < xs.length

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem lcm_insert [DecidableEq β] {b : β} :
    (insert b s : Finset β).lcm f = GCDMonoid.lcm (f b) (s.lcm f)

Proof state:
case neg
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∉ s
⊢ (insert b s).lcm f = GCDMonoid.lcm (f b) (s.lcm f)

Tactic:
apply fold_insert h

Result:
no goals

Proof state:
case pos
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ (insert b s).lcm f = GCDMonoid.lcm (f b) (s.lcm f)

Tactic:
rw [insert_eq_of_mem h,
  (lcm_eq_right_iff (f b) (s.lcm f) (Multiset.normalize_lcm (s.1.map f))).2 (dvd_lcm h)]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
⊢ (insert b s).lcm f = GCDMonoid.lcm (f b) (s.lcm f)

Tactic:
by_cases h : b ∈ s

Result:
case pos
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ (insert b s).lcm f = GCDMonoid.lcm (f b) (s.lcm f)

case neg
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∉ s
⊢ (insert b s).lcm f = GCDMonoid.lcm (f b) (s.lcm f)
-- Mathlib/Data/Int/Init.lean
protected lemma le_of_eq (hab : a = b) : a ≤ b

Proof state:
a b : ℤ
hab : a = b
⊢ b ≤ b

Tactic:
exact Int.le_rfl

Result:
no goals

Proof state:
a b : ℤ
hab : a = b
⊢ a ≤ b

Tactic:
rw [hab]

Result:
a b : ℤ
hab : a = b
⊢ b ≤ b
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_union_Ioo (h₁ : min a b < max c d) (h₂ : min c d < max a b) :
    Ioo a b ∪ Ioo c d = Ioo (min a c) (max b d)

Proof state:
case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a < c
h₂ : d < b
⊢ Ioo a b ∪ Ioo c d = Ioo (a ⊓ c) (b ⊔ d)

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b < d
h₂ : c < a
⊢ Ioo a b ∪ Ioo c d = Ioo (a ⊓ c) (b ⊔ d)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b < c
h₂ : d < a
⊢ Ioo a b ∪ Ioo c d = Ioo (a ⊓ c) (b ⊔ d)

Tactic:
all_goals
  simp [*, min_eq_left_of_lt, min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt,
    le_of_lt h₂, le_of_lt h₁]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : a ⊓ b < c ⊔ d
h₂ : c ⊓ d < a ⊔ b
⊢ Ioo a b ∪ Ioo c d = Ioo (a ⊓ c) (b ⊔ d)

Tactic:
rcases le_total a b with hab | hab <;> rcases le_total c d with hcd | hcd <;>
  simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, hab, hcd] at h₁ h₂

Result:
case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a < d
h₂ : c < b
⊢ Ioo a b ∪ Ioo c d = Ioo (a ⊓ c) (b ⊔ d)

case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : d ≤ c
h₁ : a < c
h₂ : d < b
⊢ Ioo a b ∪ Ioo c d = Ioo (a ⊓ c) (b ⊔ d)

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : c ≤ d
h₁ : b < d
h₂ : c < a
⊢ Ioo a b ∪ Ioo c d = Ioo (a ⊓ c) (b ⊔ d)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b < c
h₂ : d < a
⊢ Ioo a b ∪ Ioo c d = Ioo (a ⊓ c) (b ⊔ d)

Proof state:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b ≤ a
hcd : d ≤ c
h₁ : b < c
h₂ : d < a
⊢ Ioo a b ∪ Ioo c d = Ioo (a ⊓ c) (b ⊔ d)

Tactic:
simp [*, min_eq_left_of_lt, min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt,
  le_of_lt h₂, le_of_lt h₁]

Result:
no goals

Proof state:
case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a < d
h₂ : c < b
⊢ Ioo a b ∪ Ioo c d = Ioo (a ⊓ c) (b ⊔ d)

Tactic:
exact Ioo_union_Ioo' h₂ h₁

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem isRed_reverse {t : RBNode α} : t.reverse.isRed = t.isRed

Proof state:
α : Type u_1
t : RBNode α
⊢ t.reverse.isRed = t.isRed

Tactic:
cases t <;> simp [isRed]

Result:
no goals
-- Mathlib/Data/Nat/WithBot.lean
theorem add_eq_two_iff {n m : WithBot ℕ} :
    n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0

Proof state:
case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 2 ↔ ↑a✝ = 0 ∧ m = 2 ∨ ↑a✝ = 1 ∧ m = 1 ∨ ↑a✝ = 2 ∧ m = 0

Tactic:
cases m

Result:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 2 ↔ ↑a✝ = 0 ∧ ⊥ = 2 ∨ ↑a✝ = 1 ∧ ⊥ = 1 ∨ ↑a✝ = 2 ∧ ⊥ = 0

case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 2 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 2 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 2 ∧ ↑a✝ = 0

Proof state:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 2 ↔ ↑a✝ = 0 ∧ ⊥ = 2 ∨ ↑a✝ = 1 ∧ ⊥ = 1 ∨ ↑a✝ = 2 ∧ ⊥ = 0

Tactic:
simp [WithBot.add_bot]

Result:
no goals

Proof state:
n m : WithBot ℕ
⊢ n + m = 2 ↔ n = 0 ∧ m = 2 ∨ n = 1 ∧ m = 1 ∨ n = 2 ∧ m = 0

Tactic:
cases n

Result:
case bot
m : WithBot ℕ
⊢ ⊥ + m = 2 ↔ ⊥ = 0 ∧ m = 2 ∨ ⊥ = 1 ∧ m = 1 ∨ ⊥ = 2 ∧ m = 0

case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 2 ↔ ↑a✝ = 0 ∧ m = 2 ∨ ↑a✝ = 1 ∧ m = 1 ∨ ↑a✝ = 2 ∧ m = 0

Proof state:
case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 2 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 2 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 2 ∧ ↑a✝ = 0

Tactic:
simp [← WithBot.coe_add, Nat.add_eq_two_iff]

Result:
no goals

Proof state:
case bot
m : WithBot ℕ
⊢ ⊥ + m = 2 ↔ ⊥ = 0 ∧ m = 2 ∨ ⊥ = 1 ∧ m = 1 ∨ ⊥ = 2 ∧ m = 0

Tactic:
simp [WithBot.bot_add]

Result:
no goals
-- Mathlib/Algebra/CharP/Lemmas.lean
lemma neg_one_pow_expChar : (-1 : R) ^ p = -1

Proof state:
R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1) ^ p + 1 ^ p = 0

Tactic:
rw [← add_pow_expChar_of_commute _ (Commute.one_right _), neg_add_cancel,
  zero_pow (expChar_ne_zero R p)]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1) ^ p + 1 = 0

Tactic:
nth_rw 2 [← one_pow p]

Result:
R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1) ^ p + 1 ^ p = 0

Proof state:
R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1) ^ p = -1

Tactic:
rw [eq_neg_iff_add_eq_zero]

Result:
R : Type u_1
inst✝ : Ring R
p : ℕ
hR : ExpChar R p
⊢ (-1) ^ p + 1 = 0
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- One direction of `mul_inv_le_iff₀` where `b` is allowed to be `0` (but `c` must be nonnegative).
-/
lemma mul_inv_le_of_le_mul₀ (hb : 0 ≤ b) (hc : 0 ≤ c) (h : a ≤ c * b) : a * b⁻¹ ≤ c

Proof state:
case inr
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
hb : 0 < b
⊢ a * b⁻¹ ≤ c

Tactic:
rwa [mul_inv_le_iff₀ hb]

Result:
no goals

Proof state:
case inl
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a c : G₀
inst✝ : MulPosMono G₀
hc : 0 ≤ c
hb : 0 ≤ 0
h : a ≤ c * 0
⊢ a * 0⁻¹ ≤ c

Tactic:
simp [hc]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
⊢ a * b⁻¹ ≤ c

Tactic:
obtain rfl | hb := hb.eq_or_lt

Result:
case inl
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a c : G₀
inst✝ : MulPosMono G₀
hc : 0 ≤ c
hb : 0 ≤ 0
h : a ≤ c * 0
⊢ a * 0⁻¹ ≤ c

case inr
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosMono G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
hb : 0 < b
⊢ a * b⁻¹ ≤ c