harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range'_zero : range' s 0 step = #v[]

Proof state:
s step : Nat
⊢ range' s 0 step = { toArray := #[], size_toArray := ⋯ }

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma dblY_of_Y_eq' [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) (hy : P y * Q z = Q y * P z)
    (hy' : P y * Q z = W'.negY Q * P z) : W'.dblY P * P z ^ 2 = eval P W'.polynomialX ^ 3

Proof state:
case a.a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.dblY P * P z ^ 2 + W'.negDblY P * P z ^ 2 - ((eval P) W'.polynomialX ^ 3 + -(eval P) W'.polynomialX ^ 3) = 0

Tactic:
rw [dblY, negY_eq, dblX_of_Y_eq hP hPz hQz hx hy hy',
dblZ_of_Y_eq hQz hx hy hy']

Result:
case a.a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ (-W'.negDblY P - W'.a₁ * 0 - W'.a₃ * 0) * P z ^ 2 + W'.negDblY P * P z ^ 2 -
      ((eval P) W'.polynomialX ^ 3 + -(eval P) W'.polynomialX ^ 3) =
    0

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.dblY P * P z ^ 2 = (eval P) W'.polynomialX ^ 3

Tactic:
linear_combination (norm := (rw [dblY, negY_eq, dblX_of_Y_eq hP hPz hQz hx hy hy',
  dblZ_of_Y_eq hQz hx hy hy']; ring1)) -negDblY_of_Y_eq' hP hQz hx hy hy'

Result:
no goals

Proof state:
case a.a
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ (-W'.negDblY P - W'.a₁ * 0 - W'.a₃ * 0) * P z ^ 2 + W'.negDblY P * P z ^ 2 -
      ((eval P) W'.polynomialX ^ 3 + -(eval P) W'.polynomialX ^ 3) =
    0

Tactic:
ring1

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Opposites.lean
theorem opRingEquiv_symm_C_mul_X_pow (r : Rᵐᵒᵖ) (n : ℕ) :
    (opRingEquiv R).symm (C r * X ^ n : Rᵐᵒᵖ[X]) = op (C (unop r) * X ^ n)

Proof state:
R : Type u_1
inst✝ : Semiring R
r : Rᵐᵒᵖ
n : ℕ
⊢ (opRingEquiv R).symm (C r * X ^ n) = op (C (unop r) * X ^ n)

Tactic:
rw [C_mul_X_pow_eq_monomial, opRingEquiv_symm_monomial, C_mul_X_pow_eq_monomial]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem Function.Surjective.denseRange (hf : Function.Surjective f) : DenseRange f := fun x => by
  simp [hf.range_eq]

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_4
f : α → X
hf : Surjective f
x : X
⊢ x ∈ closure (range f)

Tactic:
simp [hf.range_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_add_one (hx : x ≠ 0) (y : ℝ) : x ^ (y + 1) = x ^ y * x

Proof state:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
simpa using rpow_add_natCast hx y 1

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_midpoint_right (p₁ p₂ : P) :
    dist (midpoint 𝕜 p₁ p₂) p₂ = ‖(2 : 𝕜)‖⁻¹ * dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ : P
⊢ dist (midpoint 𝕜 p₁ p₂) p₂ = ‖2‖⁻¹ * dist p₁ p₂

Tactic:
rw [midpoint_comm, dist_midpoint_left, dist_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_le_lintegral_pos (hf : AEMeasurable f μ) : 0 < μ {x | f x ≤ ∫⁻ a, f a ∂μ}

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inst✝ : IsProbabilityMeasure μ
hf : AEMeasurable f μ
⊢ 0 < μ {x | f x ≤ ∫⁻ (a : α), f a ∂μ}

Tactic:
simpa only [laverage_eq_lintegral] using
  measure_le_laverage_pos (IsProbabilityMeasure.ne_zero μ) hf

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem length_listTransvecCol : (listTransvecCol M).length = r

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
⊢ (listTransvecCol M).length = r

Tactic:
simp [listTransvecCol]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Category.lean
theorem mono_of_mono_app (α : F ⟶ G) [∀ X : C, Mono (α.app X)] : Mono α :=
  ⟨fun g h eq => by
    ext X
    rw [← cancel_mono (α.app X), ← comp_app, eq, comp_app]⟩

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Mono (α.app X)
Z✝ : C ⥤ D
g h : Z✝ ⟶ F
eq : g ≫ α = h ≫ α
⊢ g = h

Tactic:
ext X

Result:
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Mono (α.app X)
Z✝ : C ⥤ D
g h : Z✝ ⟶ F
eq : g ≫ α = h ≫ α
X : C
⊢ g.app X = h.app X

Proof state:
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Mono (α.app X)
Z✝ : C ⥤ D
g h : Z✝ ⟶ F
eq : g ≫ α = h ≫ α
X : C
⊢ g.app X = h.app X

Tactic:
rw [← cancel_mono (α.app X), ← comp_app, eq, comp_app]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findSome?_guard (l : Array α) : findSome? (Option.guard fun x => p x) l = find? p l

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ findSome? (Option.guard fun x => p x = true) l = find? p l

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ findSome? (Option.guard fun x => p x = true) { toList := toList✝ } = find? p { toList := toList✝ }

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ findSome? (Option.guard fun x => p x = true) { toList := toList✝ } = find? p { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem reverse_prefix : reverse l₁ <+: reverse l₂ ↔ l₁ <:+ l₂

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ l₁.reverse <+: l₂.reverse ↔ l₁ <:+ l₂

Tactic:
rw [← reverse_suffix]

Result:
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ l₁.reverse.reverse <:+ l₂.reverse.reverse ↔ l₁ <:+ l₂

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ l₁.reverse.reverse <:+ l₂.reverse.reverse ↔ l₁ <:+ l₂

Tactic:
simp only [reverse_reverse]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem le_mul_left {a b : Associates M} : a ≤ b * a

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
⊢ a ≤ a * b

Tactic:
exact le_mul_right

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
⊢ a ≤ b * a

Tactic:
rw [mul_comm]

Result:
M : Type u_1
inst✝ : CommMonoid M
a b : Associates M
⊢ a ≤ a * b
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_conj : sinh (conj x) = conj (sinh x)

Proof state:
x : ℂ
⊢ (starRingEnd ℂ) (cexp x - cexp (-x)) / 2 = (starRingEnd ℂ) (cexp x - cexp (-x)) / (starRingEnd ℂ) 2

Tactic:
simp [← one_add_one_eq_two]

Result:
no goals

Proof state:
x : ℂ
⊢ sinh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (sinh x)

Tactic:
rw [sinh, ← RingHom.map_neg, exp_conj, exp_conj, ← RingHom.map_sub, sinh, map_div₀]

Result:
x : ℂ
⊢ (starRingEnd ℂ) (cexp x - cexp (-x)) / 2 = (starRingEnd ℂ) (cexp x - cexp (-x)) / (starRingEnd ℂ) 2
-- Mathlib/Computability/Primrec.lean
theorem fin_curry₁ {n} {f : Fin n → α → σ} : Primrec₂ f ↔ ∀ i, Primrec (f i) :=
  ⟨fun h i => h.comp (const i) .id, fun h =>
    (vector_get.comp ((vector_ofFn h).comp snd) fst).of_eq fun a => by simp⟩

Proof state:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
h : ∀ (i : Fin n), Primrec (f i)
a : Fin n × α
⊢ (List.Vector.ofFn fun i => f i a.2).get a.1 = f a.1 a.2

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_eq_getValueD [BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β}
    (h : containsKey a l = true) : getValue a l h = getValueD a l fallback

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
a : α
fallback : β
h : containsKey a l = true
⊢ getValue a l h = getValueD a l fallback

Tactic:
rw [getValueD_eq_getValue?, getValue, Option.get_eq_getD]

Result:
no goals
-- Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean
theorem Module.finrank_linearMap :
    finrank S (M →ₗ[R] N) = finrank R M * finrank S N

Proof state:
R : Type u
S : Type u'
M : Type v
N : Type w
inst✝¹² : Ring R
inst✝¹¹ : Ring S
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : Free R M
inst✝⁷ : Module.Finite R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : Module S N
inst✝³ : SMulCommClass R S N
inst✝² : StrongRankCondition R
inst✝¹ : StrongRankCondition S
inst✝ : Free S N
⊢ finrank S (M →ₗ[R] N) = finrank R M * finrank S N

Tactic:
simp_rw [finrank, rank_linearMap, toNat_mul, toNat_lift]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma mem_weightSpace (χ : L → R) (m : M) : m ∈ weightSpace M χ ↔ ∀ x, ⁅x, m⁆ = χ x • m

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
χ : L → R
m : M
⊢ m ∈ weightSpace M χ ↔ ∀ (x : L), ⁅x, m⁆ = χ x • m

Tactic:
simp [weightSpace]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem mem_closure_pi {ι : Type*} {α : ι → Type*} [∀ i, TopologicalSpace (α i)] {I : Set ι}
    {s : ∀ i, Set (α i)} {x : ∀ i, α i} : x ∈ closure (pi I s) ↔ ∀ i ∈ I, x i ∈ closure (s i)

Proof state:
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
I : Set ι
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ x ∈ closure (I.pi s) ↔ ∀ i ∈ I, x i ∈ closure (s i)

Tactic:
simp only [mem_closure_iff_nhdsWithin_neBot, nhdsWithin_pi_neBot]

Result:
no goals
-- Mathlib/Algebra/Homology/ExactSequence.lean
lemma exact₀ (S : ComposableArrows C 0) : S.Exact where
  toIsComplex := S.isComplex₀
  -- See https://github.com/leanprover/lean4/issues/2862
  exact i hi

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ComposableArrows C 0
i : ℕ
hi : autoParam (i + 2 ≤ 0) _auto✝
⊢ (S.sc ⋯ i ⋯).Exact

Tactic:
simp at hi

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
theorem pullbackSymmetry_hom_comp_snd [HasPullback f g] :
    (pullbackSymmetry f g).hom ≫ pullback.snd g f = pullback.fst f g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (pullbackSymmetry f g).hom ≫ pullback.snd g f = pullback.fst f g

Tactic:
simp [pullbackSymmetry]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem back!_push [Inhabited α] (a : Array α) : (a.push x).back! = x

Proof state:
α : Type u_1
x : α
inst✝ : Inhabited α
a : Array α
⊢ (a.push x).back! = x

Tactic:
simp [back!_eq_back?]

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem K'.elim_update_stack {a b c d d'} :
    update (K'.elim a b c d) stack d' = K'.elim a b c d'

Proof state:
case h
a b c d d' : List Γ'
x : K'
⊢ update (elim a b c d) stack d' x = elim a b c d' x

Tactic:
cases x <;> rfl

Result:
no goals

Proof state:
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' = elim a b c d'

Tactic:
funext x

Result:
case h
a b c d d' : List Γ'
x : K'
⊢ update (elim a b c d) stack d' x = elim a b c d' x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attach_reverse (xs : Array α) :
    xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ map (fun x => ⟨x.val, ⋯⟩) toList✝.reverse.toArray.attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      { toList := toList✝ }.attach.reverse

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.reverse.attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      { toList := toList✝ }.attach.reverse

Tactic:
rw [attach_congr (List.reverse_toArray _)]

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ map (fun x => ⟨x.val, ⋯⟩) toList✝.reverse.toArray.attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      { toList := toList✝ }.attach.reverse

Proof state:
α : Type ?u.130113
xs : Array α
x✝ : { x // x ∈ xs }
x : α
h : x ∈ xs
⊢ x ∈ xs.reverse

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
⊢ xs.reverse.attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.attach.reverse

Tactic:
cases xs

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ { toList := toList✝ }.reverse.attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      { toList := toList✝ }.attach.reverse
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_coeff_natDegree : f.eraseLead.coeff f.natDegree = 0

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

Tactic:
simp [eraseLead_coeff]

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem insert_singleton_eq {a : α} {b b' : β a} : insert a b (singleton a b') = singleton a b :=
  ext <| by
    simp only [AList.entries_insert, List.kerase_cons_eq, and_self_iff, AList.singleton_entries,
      heq_iff_eq, eq_self_iff_true]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
⊢ (insert a b (singleton a b')).entries = (singleton a b).entries

Tactic:
simp only [AList.entries_insert, List.kerase_cons_eq, and_self_iff, AList.singleton_entries,
  heq_iff_eq, eq_self_iff_true]

Result:
no goals
-- Mathlib/Probability/ConditionalProbability.lean
@[simp] lemma cond_empty : μ[|∅] = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
⊢ μ[|∅] = 0

Tactic:
simp [cond]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpOrder.lean
theorem coeFn_le (f g : Lp E p μ) : f ≤ᵐ[μ] g ↔ f ≤ g

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g : ↥(Lp E p μ)
⊢ ↑↑f ≤ᶠ[ae μ] ↑↑g ↔ f ≤ g

Tactic:
rw [← Subtype.coe_le_coe, ← AEEqFun.coeFn_le]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_nsmul_coe_div_two (θ : ℝ) : (2 : ℕ) • (↑(θ / 2) : Angle) = θ

Proof state:
θ : ℝ
⊢ 2 • ↑(θ / 2) = ↑θ

Tactic:
rw [← coe_nsmul, two_nsmul, add_halves]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_empty_iff (a : α) : a ∈ (#v[] : Vector α 0) ↔ False

Proof state:
α : Type u_1
a : α
⊢ a ∈ { toArray := #[], size_toArray := ⋯ } ↔ False

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem veblen_zero_apply (a : Ordinal) : veblen 0 a = ω ^ a

Proof state:
a : Ordinal.{u_1}
⊢ veblen 0 a = ω ^ a

Tactic:
rw [veblen_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@[reassoc (attr := simp)] lemma w₁₃_τ₁ : S.v₁₂.τ₁ ≫ S.v₂₃.τ₁ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₁₂.τ₁ ≫ S.v₂₃.τ₁ = 0

Tactic:
rw [← comp_τ₁, S.w₁₃, zero_τ₁]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem HasDerivAtFilter.congr_of_eventuallyEq (h : HasDerivAtFilter f f' x L) (hL : f₁ =ᶠ[L] f)
    (hx : f₁ x = f x) : HasDerivAtFilter f₁ f' x L

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
h : HasDerivAtFilter f f' x L
hL : f₁ =ᶠ[L] f
hx : f₁ x = f x
⊢ HasDerivAtFilter f₁ f' x L

Tactic:
rwa [hL.hasDerivAtFilter_iff hx rfl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem dite_cond_eq_false' {α : Sort u} {c : Prop} {_ : Decidable c} {a : c → α} {b : ¬ c → α} {r : α} (h₁ : c = False) (h₂ : b (of_eq_false h₁) = r) : (dite c a b) = r

Proof state:
α : Sort u
c : Prop
x✝ : Decidable c
a : c → α
b : ¬c → α
r : α
h₁ : c = False
h₂ : b ⋯ = r
⊢ dite c a b = r

Tactic:
simp [h₁, h₂]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem sdiff_symmDiff' : c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)

Tactic:
rw [sdiff_symmDiff, sdiff_sup]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem sum_divisors_mul {m n : ℕ} (hmn : m.Coprime n) :
    ∑ d ∈ (m * n).divisors, d = (∑ d ∈ m.divisors, d) * ∑ d ∈ n.divisors, d

Proof state:
m n : ℕ
hmn : m.Coprime n
⊢ ∑ d ∈ (m * n).divisors, d = (∑ d ∈ m.divisors, d) * ∑ d ∈ n.divisors, d

Tactic:
simp only [← sigma_one_apply, isMultiplicative_sigma.map_mul_of_coprime hmn]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem update_apply {β : Sort*} (f : α → β) (a' : α) (b : β) (a : α) :
    update f a' b a = if a = a' then b else f a

Proof state:
α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f : α → β
a' : α
b : β
a : α
⊢ update f a' b a = if a = a' then b else f a

Tactic:
rcases Decidable.eq_or_ne a a' with rfl | hne <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Basic.lean
theorem factorThruImage_comp_coimageIsoImage'_inv :
    factorThruImage f ≫ (coimageIsoImage' f).inv = cokernel.π _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ factorThruImage f ≫ (coimageIsoImage' f).inv = cokernel.π (kernel.ι f)

Tactic:
simp only [IsImage.isoExt_inv, image.isImage_lift, image.fac_lift,
  coimageStrongEpiMonoFactorisation_e]

Result:
no goals
-- Mathlib/Algebra/Module/NatInt.lean
theorem Nat.smul_one_eq_cast {R : Type*} [NonAssocSemiring R] (m : ℕ) : m • (1 : R) = ↑m

Proof state:
R : Type u_5
inst✝ : NonAssocSemiring R
m : ℕ
⊢ m • 1 = ↑m

Tactic:
rw [nsmul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem nonempty_embedding_to_cardinal : Nonempty (α ↪ Cardinal.{u}) :=
  (Embedding.total _ _).resolve_left fun ⟨⟨f, hf⟩⟩ =>
    let g : α → Cardinal.{u} := invFun f
    let ⟨x, (hx : g x = 2 ^ sum g)⟩ := invFun_surjective hf (2 ^ sum g)
    have : g x ≤ sum g := le_sum.{u, u} g x
    not_le_of_gt (by rw [hx]; exact cantor _) this

Proof state:
α : Type u
x✝ : Nonempty (Cardinal.{u} ↪ α)
f : Cardinal.{u} → α
hf : Injective f
g : α → Cardinal.{u} := invFun f
x : α
hx : g x = 2 ^ sum g
this : g x ≤ sum g
⊢ g x > sum g

Tactic:
rw [hx]

Result:
α : Type u
x✝ : Nonempty (Cardinal.{u} ↪ α)
f : Cardinal.{u} → α
hf : Injective f
g : α → Cardinal.{u} := invFun f
x : α
hx : g x = 2 ^ sum g
this : g x ≤ sum g
⊢ 2 ^ sum g > sum g

Proof state:
α : Type u
x✝ : Nonempty (Cardinal.{u} ↪ α)
f : Cardinal.{u} → α
hf : Injective f
g : α → Cardinal.{u} := invFun f
x : α
hx : g x = 2 ^ sum g
this : g x ≤ sum g
⊢ 2 ^ sum g > sum g

Tactic:
exact cantor _

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem bicone_ι_π_ne {F : J → C} (B : Bicone F) {j j' : J} (h : j ≠ j') : B.ι j ≫ B.π j' = 0

Proof state:
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
B : Bicone F
j j' : J
h : j ≠ j'
⊢ B.ι j ≫ B.π j' = 0

Tactic:
simpa [h] using B.ι_π j j'

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem lcm_mul_right {m n k : ℕ} : (m * n).lcm (k * n) = m.lcm k * n

Proof state:
m n k : ℕ
⊢ (m * n).lcm (k * n) = m.lcm k * n

Tactic:
rw [mul_comm, mul_comm k n, lcm_mul_left, mul_comm]

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.seq {β γ} {f : α → Part (β → γ)} {g : α → Part β} (hf : ωScottContinuous f)
    (hg : ωScottContinuous g) : ωScottContinuous fun x ↦ f x <*> g x

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part (β → γ)
g : α → Part β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous fun x => do
    let x_1 ← f x
    x_1 <$> g x

Tactic:
exact ωScottContinuous.bind hf <| ωScottContinuous.of_apply₂ fun _ ↦ ωScottContinuous.map hg

Result:
no goals

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part (β → γ)
g : α → Part β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous fun x => f x <*> g x

Tactic:
simp only [seq_eq_bind_map]

Result:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part (β → γ)
g : α → Part β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous fun x => do
    let x_1 ← f x
    x_1 <$> g x
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.principal_inf (hl : l.HasBasis p s) (s' : Set α) :
    (𝓟 s' ⊓ l).HasBasis p fun i => s' ∩ s i

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
s' : Set α
⊢ (𝓟 s' ⊓ l).HasBasis p fun i => s' ∩ s i

Tactic:
simpa only [inf_comm, inter_comm] using hl.inf_principal s'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.get!_val [BEq α] [Hashable α] [Inhabited β] {m : Raw₀ α (fun _ => β)} {a : α} :
    Raw.Const.get! m.val a = Raw₀.Const.get! m a

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : Inhabited β
m : Raw₀ α fun x => β
a : α
⊢ Raw.Const.get! m.val a = Raw₀.Const.get! m a

Tactic:
simp [Raw.Const.get!, m.2]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma rpow_neg_one_le_one {a : A} (ha : 1 ≤ a) : a ^ (-1 : ℝ) ≤ 1

Proof state:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : 1 ≤ ↑a
⊢ ↑a ^ (-1) ≤ 1

Tactic:
rw [rpow_neg_one_eq_inv a (zero_le_one.trans ha)]

Result:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : 1 ≤ ↑a
⊢ ↑a⁻¹ ≤ 1

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 1 ≤ a
⊢ a ^ (-1) ≤ 1

Tactic:
lift a to Aˣ using isUnit_of_le isUnit_one zero_le_one ha

Result:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : 1 ≤ ↑a
⊢ ↑a ^ (-1) ≤ 1

Proof state:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : 1 ≤ ↑a
⊢ ↑a⁻¹ ≤ 1

Tactic:
exact inv_le_one ha

Result:
no goals
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem uniformContinuous_dom₂ {f : SeparationQuotient α × SeparationQuotient β → γ} :
    UniformContinuous f ↔ UniformContinuous fun p : α × β ↦ f (mk p.1, mk p.2)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : SeparationQuotient α × SeparationQuotient β → γ
⊢ UniformContinuous f ↔ UniformContinuous fun p => f (mk p.1, mk p.2)

Tactic:
simp only [UniformContinuous, uniformity_prod_eq_prod, uniformity_eq, prod_map_map_eq,
  tendsto_map'_iff]

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : SeparationQuotient α × SeparationQuotient β → γ
⊢ Tendsto
      (((fun x => (f x.1, f x.2)) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun p =>
        (Prod.map mk mk p.1, Prod.map mk mk p.2))
      (𝓤 α ×ˢ 𝓤 β) (𝓤 γ) ↔
    Tendsto ((fun x => (f (mk x.1.1, mk x.1.2), f (mk x.2.1, mk x.2.2))) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2))
      (𝓤 α ×ˢ 𝓤 β) (𝓤 γ)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : SeparationQuotient α × SeparationQuotient β → γ
⊢ Tendsto
      (((fun x => (f x.1, f x.2)) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ∘ fun p =>
        (Prod.map mk mk p.1, Prod.map mk mk p.2))
      (𝓤 α ×ˢ 𝓤 β) (𝓤 γ) ↔
    Tendsto ((fun x => (f (mk x.1.1, mk x.1.2), f (mk x.2.1, mk x.2.2))) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2))
      (𝓤 α ×ˢ 𝓤 β) (𝓤 γ)

Tactic:
rfl

Result:
no goals