harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/UrysohnsLemma.lean
theorem lim_eq_midpoint (c : CU P) (x : X) :
    c.lim x = midpoint ℝ (c.left.lim x) (c.right.lim x)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
x : X
⊢ Tendsto (fun n => midpoint ℝ (approx n c.left x) (approx n c.right x)) atTop
    (𝓝 (midpoint ℝ (c.left.lim x) (c.right.lim x)))

Tactic:
exact (c.left.tendsto_approx_atTop x).midpoint (c.right.tendsto_approx_atTop x)

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
x : X
⊢ c.lim x = midpoint ℝ (c.left.lim x) (c.right.lim x)

Tactic:
refine tendsto_nhds_unique (c.tendsto_approx_atTop x) ((tendsto_add_atTop_iff_nat 1).1 ?_)

Result:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
x : X
⊢ Tendsto (fun n => approx (n + 1) c x) atTop (𝓝 (midpoint ℝ (c.left.lim x) (c.right.lim x)))

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
x : X
⊢ Tendsto (fun n => approx (n + 1) c x) atTop (𝓝 (midpoint ℝ (c.left.lim x) (c.right.lim x)))

Tactic:
simp only [approx]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
x : X
⊢ Tendsto (fun n => midpoint ℝ (approx n c.left x) (approx n c.right x)) atTop
    (𝓝 (midpoint ℝ (c.left.lim x) (c.right.lim x)))
-- Mathlib/FieldTheory/Finite/GaloisField.lean
theorem galois_poly_separable {K : Type*} [Field K] (p q : ℕ) [CharP K p] (h : p ∣ q) :
    Separable (X ^ q - X : K[X])

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
p q : ℕ
inst✝ : CharP K p
h : ↑q = 0
⊢ 1 * (X ^ q - X) + (X ^ q - X - 1) * derivative (X ^ q - X) = 1

Tactic:
rw [derivative_sub, derivative_X_pow, derivative_X, C_eq_natCast, h]

Result:
case h
K : Type u_1
inst✝¹ : Field K
p q : ℕ
inst✝ : CharP K p
h : ↑q = 0
⊢ 1 * (X ^ q - X) + (X ^ q - X - 1) * (0 * X ^ (q - 1) - 1) = 1

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
p q : ℕ
inst✝ : CharP K p
h : ↑q = 0
⊢ 1 * (X ^ q - X) + (X ^ q - X - 1) * (0 * X ^ (q - 1) - 1) = 1

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
p q : ℕ
inst✝ : CharP K p
h : p ∣ q
⊢ (X ^ q - X).Separable

Tactic:
use 1, X ^ q - X - 1

Result:
case h
K : Type u_1
inst✝¹ : Field K
p q : ℕ
inst✝ : CharP K p
h : p ∣ q
⊢ 1 * (X ^ q - X) + (X ^ q - X - 1) * derivative (X ^ q - X) = 1

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
p q : ℕ
inst✝ : CharP K p
h : p ∣ q
⊢ 1 * (X ^ q - X) + (X ^ q - X - 1) * derivative (X ^ q - X) = 1

Tactic:
rw [← CharP.cast_eq_zero_iff K[X] p] at h

Result:
case h
K : Type u_1
inst✝¹ : Field K
p q : ℕ
inst✝ : CharP K p
h : ↑q = 0
⊢ 1 * (X ^ q - X) + (X ^ q - X - 1) * derivative (X ^ q - X) = 1
-- Mathlib/Data/Matroid/Circuit.lean
lemma restrict_isCircuit_iff (hR : R ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
C R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ ¬M.Indep C →
    C ⊆ R →
      (∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C) →
        ((¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D ∧ D ⊆ M.E → D ⊆ C → D = C) ∧ C ⊆ R

Tactic:
exact fun hC hCR h ↦ ⟨⟨⟨hC,hCR.trans hR⟩,fun I hI hIC ↦ h hI.1 (hIC.trans hCR) hIC⟩,hCR⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
C R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (M ↾ R).IsCircuit C → M.IsCircuit C ∧ C ⊆ R

Tactic:
simp_rw [isCircuit_iff, restrict_dep_iff, and_imp, dep_iff]

Result:
α : Type u_1
M : Matroid α
C R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ ¬M.Indep C →
    C ⊆ R →
      (∀ ⦃D : Set α⦄, ¬M.Indep D → D ⊆ R → D ⊆ C → D = C) →
        ((¬M.Indep C ∧ C ⊆ M.E) ∧ ∀ ⦃D : Set α⦄, ¬M.Indep D ∧ D ⊆ M.E → D ⊆ C → D = C) ∧ C ⊆ R

Proof state:
α : Type u_1
M : Matroid α
C R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (M ↾ R).IsCircuit C ↔ M.IsCircuit C ∧ C ⊆ R

Tactic:
refine ⟨?_, fun h ↦ h.1.isCircuit_restrict_of_subset h.2⟩

Result:
α : Type u_1
M : Matroid α
C R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (M ↾ R).IsCircuit C → M.IsCircuit C ∧ C ⊆ R
-- Mathlib/Data/Num/Lemmas.lean
theorem ofInt'_toZNum : ∀ n : ℕ, toZNum n = ZNum.ofInt' n
  | 0 => rfl
  | n + 1 => by
    rw [Nat.cast_succ, Num.add_one, toZNum_succ, ofInt'_toZNum n, Nat.cast_succ, succ_ofInt',
      ZNum.add_one]

Proof state:
n : ℕ
⊢ (↑(n + 1)).toZNum = ZNum.ofInt' ↑(n + 1)

Tactic:
rw [Nat.cast_succ, Num.add_one, toZNum_succ, ofInt'_toZNum n, Nat.cast_succ, succ_ofInt',
  ZNum.add_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_append_of_containsKey_eq_false [BEq α] [PartialEquivBEq α]
    {l l' : List ((a : α) × β a)} {a : α} (hl' : containsKey a l' = false) :
    getKey? a (l ++ l') = getKey? a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
hl' : containsKey a l' = false
⊢ getKey? a (l ++ l') = getKey? a l

Tactic:
simp [getKey?_eq_getEntry?, getEntry?_eq_none.2 hl']

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Alternating.lean
theorem two_mul_card_alternatingGroup [Nontrivial α] :
    2 * card (alternatingGroup α) = card (Perm α)

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ 2 * card ↥(alternatingGroup α) = card (Perm α)

Tactic:
simp only [← Nat.card_eq_fintype_card, ← alternatingGroup.index_eq_two (α := α), index_mul_card]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem ofSet_trans_ofSet {s : Set X} (hs : IsOpen s) {s' : Set X} (hs' : IsOpen s') :
    (ofSet s hs).trans (ofSet s' hs') = ofSet (s ∩ s') (IsOpen.inter hs hs')

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
s' : Set X
hs' : IsOpen s'
⊢ (ofSet s hs).trans (ofSet s' hs') = ofSet (s ∩ s') ⋯

Tactic:
rw [(ofSet s hs).trans_ofSet hs']

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
s' : Set X
hs' : IsOpen s'
⊢ (ofSet s hs).restr (↑(ofSet s hs) ⁻¹' s') = ofSet (s ∩ s') ⋯

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
s' : Set X
hs' : IsOpen s'
⊢ (ofSet s hs).restr (↑(ofSet s hs) ⁻¹' s') = ofSet (s ∩ s') ⋯

Tactic:
ext <;> simp [hs'.interior_eq]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem coe_upperClosure (s : Set α) : ↑(upperClosure s) = ⋃ a ∈ s, Ici a

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ ↑(upperClosure s) = ⋃ a ∈ s, Ici a

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : Preorder α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(upperClosure s) ↔ x✝ ∈ ⋃ a ∈ s, Ici a

Proof state:
case h
α : Type u_1
inst✝ : Preorder α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(upperClosure s) ↔ x✝ ∈ ⋃ a ∈ s, Ici a

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem comap_snd : q.comap (snd R M M₂) = prod ⊤ q

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
q : Submodule R M₂
⊢ comap (snd R M M₂) q = ⊤.prod q

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
q : Submodule R M₂
x : M
y : M₂
⊢ (x, y) ∈ comap (snd R M M₂) q ↔ (x, y) ∈ ⊤.prod q

Proof state:
case h.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
q : Submodule R M₂
x : M
y : M₂
⊢ (x, y) ∈ comap (snd R M M₂) q ↔ (x, y) ∈ ⊤.prod q

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_inter_eq_of_measure_eq {s t u : Set α} (hs : MeasurableSet s) (h : μ t = μ u)
    (htu : t ⊆ u) (ht_ne_top : μ t ≠ ∞) : μ (t ∩ s) = μ (u ∩ s)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ⊤
⊢ μ (t ∩ s) ≤ μ (u ∩ s)

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ⊤
⊢ μ (t ∩ s) + μ (t \ s) ≤ μ (t ∩ s) + μ (u \ s)

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ⊤
A : μ (u ∩ s) + μ (u \ s) ≤ μ (t ∩ s) + μ (u \ s)
B : μ (u \ s) ≠ ⊤
⊢ μ (u ∩ s) ≤ μ (t ∩ s)

Tactic:
exact ENNReal.le_of_add_le_add_right B A

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ⊤
⊢ μ (u ∩ s) ≤ μ (t ∩ s)

Tactic:
have A : μ (u ∩ s) + μ (u \ s) ≤ μ (t ∩ s) + μ (u \ s) :=
  calc
    μ (u ∩ s) + μ (u \ s) = μ u := measure_inter_add_diff _ hs
    _ = μ t := h.symm
    _ = μ (t ∩ s) + μ (t \ s) := (measure_inter_add_diff _ hs).symm
    _ ≤ μ (t ∩ s) + μ (u \ s) := by gcongr

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ⊤
A : μ (u ∩ s) + μ (u \ s) ≤ μ (t ∩ s) + μ (u \ s)
⊢ μ (u ∩ s) ≤ μ (t ∩ s)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ⊤
A : μ (u ∩ s) + μ (u \ s) ≤ μ (t ∩ s) + μ (u \ s)
⊢ μ (u ∩ s) ≤ μ (t ∩ s)

Tactic:
have B : μ (u \ s) ≠ ∞ := (lt_of_le_of_lt (measure_mono diff_subset) ht_ne_top.lt_top).ne

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ⊤
A : μ (u ∩ s) + μ (u \ s) ≤ μ (t ∩ s) + μ (u \ s)
B : μ (u \ s) ≠ ⊤
⊢ μ (u ∩ s) ≤ μ (t ∩ s)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ⊤
⊢ μ (t ∩ s) = μ (u ∩ s)

Tactic:
refine le_antisymm (by gcongr) ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ⊤
⊢ μ (u ∩ s) ≤ μ (t ∩ s)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ t ≠ ⊤
⊢ μ (t ∩ s) = μ (u ∩ s)

Tactic:
rw [h] at ht_ne_top

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ⊤
⊢ μ (t ∩ s) = μ (u ∩ s)
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem sub_comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₃] (g₁ g₂ : M₂ →SL[σ₂₃] M₃)
    (f : M →SL[σ₁₂] M₂) : (g₁ - g₂).comp f = g₁.comp f - g₂.comp f

Proof state:
case h
R : Type u_1
inst✝¹³ : Ring R
R₂ : Type u_2
inst✝¹² : Ring R₂
R₃ : Type u_3
inst✝¹¹ : Ring R₃
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : AddCommGroup M
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : IsTopologicalAddGroup M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
x✝ : M
⊢ ((g₁ - g₂).comp f) x✝ = (g₁.comp f - g₂.comp f) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹³ : Ring R
R₂ : Type u_2
inst✝¹² : Ring R₂
R₃ : Type u_3
inst✝¹¹ : Ring R₃
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : AddCommGroup M
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : IsTopologicalAddGroup M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
⊢ (g₁ - g₂).comp f = g₁.comp f - g₂.comp f

Tactic:
ext

Result:
case h
R : Type u_1
inst✝¹³ : Ring R
R₂ : Type u_2
inst✝¹² : Ring R₂
R₃ : Type u_3
inst✝¹¹ : Ring R₃
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : AddCommGroup M
M₂ : Type u_5
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : IsTopologicalAddGroup M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
x✝ : M
⊢ ((g₁ - g₂).comp f) x✝ = (g₁.comp f - g₂.comp f) x✝
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem exp_zsmul (z : ℤ) (x : 𝔸) : exp 𝕂 (z • x) = exp 𝕂 x ^ z

Proof state:
case intro.inl
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
⊢ exp 𝕂 (↑n • x) = exp 𝕂 x ^ ↑n

Tactic:
rw [zpow_natCast, natCast_zsmul, exp_nsmul]

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
z : ℤ
x : 𝔸
⊢ exp 𝕂 (z • x) = exp 𝕂 x ^ z

Tactic:
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg

Result:
case intro.inl
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
⊢ exp 𝕂 (↑n • x) = exp 𝕂 x ^ ↑n

case intro.inr
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
⊢ exp 𝕂 (-↑n • x) = exp 𝕂 x ^ (-↑n)

Proof state:
case intro.inr
𝕂 : Type u_1
𝔸 : Type u_2
inst✝³ : RCLike 𝕂
inst✝² : NormedDivisionRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
⊢ exp 𝕂 (-↑n • x) = exp 𝕂 x ^ (-↑n)

Tactic:
rw [zpow_neg, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_congr_left {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (l : List α) {H₁ H₂}
    (h : ∀ a ∈ l, ∀ (h₁ h₂), f a h₁ = g a h₂) : pmap f l H₁ = pmap g l H₂

Proof state:
case cons
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
x : α
l : List α
ih :
  ∀ {H₁ : ∀ (a : α), a ∈ l → p a} {H₂ : ∀ (a : α), a ∈ l → q a},
    (∀ (a : α), a ∈ l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → pmap f l H₁ = pmap g l H₂
H₁ : ∀ (a : α), a ∈ x :: l → p a
H₂ : ∀ (a : α), a ∈ x :: l → q a
h : ∀ (a : α), a ∈ x :: l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f (x :: l) H₁ = pmap g (x :: l) H₂

Tactic:
rw [pmap, pmap, h _ (mem_cons_self _ _), ih fun a ha => h a (mem_cons_of_mem _ ha)]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
l : List α
H₁ : ∀ (a : α), a ∈ l → p a
H₂ : ∀ (a : α), a ∈ l → q a
h : ∀ (a : α), a ∈ l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f l H₁ = pmap g l H₂

Tactic:
induction l with
| nil => rfl
| cons x l ih =>
  rw [pmap, pmap, h _ (mem_cons_self _ _), ih fun a ha => h a (mem_cons_of_mem _ ha)]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
H₁ : ∀ (a : α), a ∈ [] → p a
H₂ : ∀ (a : α), a ∈ [] → q a
h : ∀ (a : α), a ∈ [] → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f [] H₁ = pmap g [] H₂

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Pointed.lean
theorem mem_dual {S : PointedCone ℝ E} {y : E} : y ∈ dual S ↔ ∀ ⦃x⦄, x ∈ S → 0 ≤ ⟪x, y⟫_ℝ

Proof state:
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
S : PointedCone ℝ E
y : E
⊢ y ∈ S.dual ↔ ∀ ⦃x : E⦄, x ∈ S → 0 ≤ ⟪x, y⟫_ℝ

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_eq_one_iff_mem_frontier (hc : Convex ℝ s) (hs₀ : s ∈ 𝓝 0) :
    gauge s x = 1 ↔ x ∈ frontier s

Proof state:
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
x : E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
⊢ gauge s x = 1 ↔ x ∈ frontier s

Tactic:
rw [eq_iff_le_not_lt, gauge_le_one_iff_mem_closure hc hs₀, gauge_lt_one_iff_mem_interior hc hs₀]

Result:
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
x : E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
⊢ x ∈ closure s ∧ x ∉ interior s ↔ x ∈ frontier s

Proof state:
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
x : E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
⊢ x ∈ closure s ∧ x ∉ interior s ↔ x ∈ frontier s

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_le_length_insertListIfNewUnit [BEq α] [EquivBEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α}:
    l.length ≤ (insertListIfNewUnit l toInsert).length

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
hd : α
tl : List α
ih : ∀ {l : List ((_ : α) × Unit)}, l.length ≤ (insertListIfNewUnit l tl).length
l : List ((_ : α) × Unit)
⊢ l.length ≤ (insertListIfNewUnit l (hd :: tl)).length

Tactic:
exact Nat.le_trans length_le_length_insertEntryIfNew ih

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
⊢ l.length ≤ (insertListIfNewUnit l toInsert).length

Tactic:
induction toInsert generalizing l with
| nil => apply Nat.le_refl
| cons hd tl ih => exact Nat.le_trans length_le_length_insertEntryIfNew ih

Result:
no goals

Proof state:
case nil
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
⊢ l.length ≤ (insertListIfNewUnit l []).length

Tactic:
apply Nat.le_refl

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma mul_lt_mul_pow_succ (ha : 0 < a) (hb : 1 < b) : n * b < a * b ^ (n + 1)

Proof state:
a b n : ℕ
ha : 0 < a
hb : 1 < b
⊢ n * b < a * b ^ (n + 1)

Tactic:
rw [Nat.pow_succ, ← Nat.mul_assoc, Nat.mul_lt_mul_right (Nat.lt_trans Nat.zero_lt_one hb)]

Result:
a b n : ℕ
ha : 0 < a
hb : 1 < b
⊢ n < a * b ^ n

Proof state:
a b n : ℕ
ha : 0 < a
hb : 1 < b
⊢ n < a * b ^ n

Tactic:
exact Nat.lt_of_le_of_lt (Nat.le_mul_of_pos_left _ ha)
  ((Nat.mul_lt_mul_left ha).2 <| Nat.lt_pow_self hb)

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem iSup_lt_ord_lift_of_isRegular {ι} {f : ι → Ordinal} {c} (hc : IsRegular c)
    (hι : Cardinal.lift.{v, u} #ι < c) : (∀ i, f i < c.ord) → iSup f < c.ord :=
  iSup_lt_ord_lift (by rwa [hc.cof_eq])

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
⊢ lift.{?u.103863, u} #ι < c.ord.cof

Tactic:
rwa [hc.cof_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Properties.lean
lemma Nondegenerate.flip {B : BilinForm K V} (hB : B.Nondegenerate) :
    B.flip.Nondegenerate

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
x : V
hx : ∀ (n : V), (B.flip x) n = 0
⊢ x = 0

Tactic:
apply (Module.evalEquiv K V).injective

Result:
case a
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
x : V
hx : ∀ (n : V), (B.flip x) n = 0
⊢ (Module.evalEquiv K V) x = (Module.evalEquiv K V) 0

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
⊢ B.flip.Nondegenerate

Tactic:
intro x hx

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
x : V
hx : ∀ (n : V), (B.flip x) n = 0
⊢ x = 0

Proof state:
case a.h.intro
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
x : V
hx : ∀ (n : V), (B.flip x) n = 0
y : V
⊢ ((Module.evalEquiv K V) x) ((B.toDual hB) y) = ((Module.evalEquiv K V) 0) ((B.toDual hB) y)

Tactic:
simpa using hx y

Result:
no goals

Proof state:
case a.h
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
x : V
hx : ∀ (n : V), (B.flip x) n = 0
f : Module.Dual K V
⊢ ((Module.evalEquiv K V) x) f = ((Module.evalEquiv K V) 0) f

Tactic:
obtain ⟨y, rfl⟩ := (B.toDual hB).surjective f

Result:
case a.h.intro
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
x : V
hx : ∀ (n : V), (B.flip x) n = 0
y : V
⊢ ((Module.evalEquiv K V) x) ((B.toDual hB) y) = ((Module.evalEquiv K V) 0) ((B.toDual hB) y)

Proof state:
case a
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
x : V
hx : ∀ (n : V), (B.flip x) n = 0
⊢ (Module.evalEquiv K V) x = (Module.evalEquiv K V) 0

Tactic:
ext f

Result:
case a.h
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
x : V
hx : ∀ (n : V), (B.flip x) n = 0
f : Module.Dual K V
⊢ ((Module.evalEquiv K V) x) f = ((Module.evalEquiv K V) 0) f
-- Mathlib/Algebra/Order/Ring/Canonical.lean
theorem mul_pos [NoZeroDivisors α] {a b : α} :
    0 < a * b ↔ 0 < a ∧ 0 < b

Proof state:
α : Type u
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : NoZeroDivisors α
a b : α
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b

Tactic:
simp only [pos_iff_ne_zero, ne_eq, mul_eq_zero, not_or]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem HasFDerivAt.eventually_ne (h : HasFDerivAt f f' x) (hf' : ∃ C, ∀ z, ‖z‖ ≤ C * ‖f' z‖) :
    ∀ᶠ z in 𝓝[≠] x, f z ≠ f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖
⊢ ∀ᶠ (z : E) in 𝓝[≠] x, f z ≠ f x

Tactic:
simpa only [compl_eq_univ_diff] using (hasFDerivWithinAt_univ.2 h).eventually_ne hf'

Result:
no goals
-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem mem_support_ind (x : M) (hx : x ∈ s) : x ∈ support (fs <| fs.ind x hx)

Proof state:
ι : Type uι
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ x ∈ support ↑(fs.toFun (fs.ind x hx))

Tactic:
simp [fs.apply_ind x hx]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem equiv_of_mem {s t : Computation α} {a} (h1 : a ∈ s) (h2 : a ∈ t) : s ~ t := fun a' =>
  ⟨fun ma => by rw [mem_unique ma h1]; exact h2, fun ma => by rw [mem_unique ma h2]; exact h1⟩

Proof state:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a' ∈ t

Tactic:
rw [mem_unique ma h1]

Result:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a ∈ t

Proof state:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ t
⊢ a ∈ s

Tactic:
exact h1

Result:
no goals

Proof state:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ t
⊢ a' ∈ s

Tactic:
rw [mem_unique ma h2]

Result:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ t
⊢ a ∈ s

Proof state:
α : Type u
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a ∈ t

Tactic:
exact h2

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma IsBasis'.isBasis_closure_right (h : M.IsBasis' I X) : M.IsBasis I (M.closure X)

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis' I X
⊢ M.IsBasis I (M.closure I)

Tactic:
exact h.indep.isBasis_closure

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis' I X
⊢ M.IsBasis I (M.closure X)

Tactic:
rw [← h.closure_eq_closure]

Result:
α : Type u_2
M : Matroid α
X I : Set α
h : M.IsBasis' I X
⊢ M.IsBasis I (M.closure I)