harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem Finite.infsep [Decidable s.Nontrivial] (hsf : s.Finite) :
    s.infsep =
      if hs : s.Nontrivial then hsf.offDiag.toFinset.inf' (by simpa) (uncurry dist) else 0

Proof state:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
x✝ : ℝ
⊢ x✝ ≤ s.infsep ↔ x✝ ≤ ⋯.toFinset.inf' ⋯ (uncurry dist)

Tactic:
simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, Finite.mem_toFinset,
  mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
⊢ s.infsep = if hs : s.Nontrivial then ⋯.toFinset.inf' ⋯ (uncurry dist) else 0

Tactic:
split_ifs with hs

Result:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
⊢ s.infsep = ⋯.toFinset.inf' ⋯ (uncurry dist)

case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : ¬s.Nontrivial
⊢ s.infsep = 0

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
⊢ ⋯.toFinset.Nonempty

Tactic:
simpa

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
⊢ s.infsep = ⋯.toFinset.inf' ⋯ (uncurry dist)

Tactic:
refine eq_of_forall_le_iff fun _ => ?_

Result:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
x✝ : ℝ
⊢ x✝ ≤ s.infsep ↔ x✝ ≤ ⋯.toFinset.inf' ⋯ (uncurry dist)

Proof state:
case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : ¬s.Nontrivial
⊢ s.infsep = 0

Tactic:
rw [not_nontrivial_iff] at hs

Result:
case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Subsingleton
⊢ s.infsep = 0

Proof state:
case neg
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Subsingleton
⊢ s.infsep = 0

Tactic:
exact hs.infsep_zero

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem Dense.biUnion_uniformity_ball {s : Set α} {U : Set (α × α)} (hs : Dense s) (hU : U ∈ 𝓤 α) :
    ⋃ x ∈ s, ball x U = univ

Proof state:
case intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set α
U : Set (α × α)
hs : Dense s
hU : U ∈ 𝓤 α
y x : α
hxs : x ∈ s
hxy : (x, y) ∈ U
⊢ ∃ i, ∃ (_ : i ∈ s), y ∈ ball i U

Tactic:
exact ⟨x, hxs, hxy⟩

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set α
U : Set (α × α)
hs : Dense s
hU : U ∈ 𝓤 α
y : α
⊢ ∃ i, ∃ (_ : i ∈ s), y ∈ ball i U

Tactic:
rcases hs.inter_nhds_nonempty (mem_nhds_right y hU) with ⟨x, hxs, hxy : (x, y) ∈ U⟩

Result:
case intro.intro
α : Type ua
inst✝ : UniformSpace α
s : Set α
U : Set (α × α)
hs : Dense s
hU : U ∈ 𝓤 α
y x : α
hxs : x ∈ s
hxy : (x, y) ∈ U
⊢ ∃ i, ∃ (_ : i ∈ s), y ∈ ball i U

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set α
U : Set (α × α)
hs : Dense s
hU : U ∈ 𝓤 α
⊢ ⋃ x ∈ s, ball x U = univ

Tactic:
refine iUnion₂_eq_univ_iff.2 fun y => ?_

Result:
α : Type ua
inst✝ : UniformSpace α
s : Set α
U : Set (α × α)
hs : Dense s
hU : U ∈ 𝓤 α
y : α
⊢ ∃ i, ∃ (_ : i ∈ s), y ∈ ball i U
-- Mathlib/Order/Filter/Ring.lean
theorem EventuallyLE.mul_le_mul [MulZeroClass β] [PartialOrder β] [PosMulMono β] [MulPosMono β]
    {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) (hg₀ : 0 ≤ᶠ[l] g₁)
    (hf₀ : 0 ≤ᶠ[l] f₂) : f₁ * g₁ ≤ᶠ[l] f₂ * g₂

Proof state:
α : Type u
β : Type v
inst✝³ : MulZeroClass β
inst✝² : PartialOrder β
inst✝¹ : PosMulMono β
inst✝ : MulPosMono β
l : Filter α
f₁ f₂ g₁ g₂ : α → β
hf : f₁ ≤ᶠ[l] f₂
hg : g₁ ≤ᶠ[l] g₂
hg₀ : 0 ≤ᶠ[l] g₁
hf₀ : 0 ≤ᶠ[l] f₂
⊢ f₁ * g₁ ≤ᶠ[l] f₂ * g₂

Tactic:
filter_upwards [hf, hg, hg₀, hf₀] with x using _root_.mul_le_mul

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem continuousAt_extend_symm {x : M} (h : x ∈ f.source) :
    ContinuousAt (f.extend I).symm (f.extend I x) :=
  continuousAt_extend_symm' f <| (f.extend I).map_source <| by rwa [f.extend_source]

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
h : x ∈ f.source
⊢ x ∈ (f.extend I).source

Tactic:
rwa [f.extend_source]

Result:
no goals
-- Mathlib/Analysis/Convex/Strict.lean
theorem strictConvex_univ : StrictConvex 𝕜 (univ : Set E)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝⁵ : x ∈ univ
y : E
a✝⁴ : y ∈ univ
a✝³ : x ≠ y
a b : 𝕜
a✝² : 0 < a
a✝¹ : 0 < b
a✝ : a + b = 1
⊢ a • x + b • y ∈ univ

Tactic:
exact mem_univ _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝⁵ : x ∈ univ
y : E
a✝⁴ : y ∈ univ
a✝³ : x ≠ y
a b : 𝕜
a✝² : 0 < a
a✝¹ : 0 < b
a✝ : a + b = 1
⊢ a • x + b • y ∈ interior univ

Tactic:
rw [interior_univ]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝⁵ : x ∈ univ
y : E
a✝⁴ : y ∈ univ
a✝³ : x ≠ y
a b : 𝕜
a✝² : 0 < a
a✝¹ : 0 < b
a✝ : a + b = 1
⊢ a • x + b • y ∈ univ

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
⊢ StrictConvex 𝕜 univ

Tactic:
intro x _ y _ _ a b _ _ _

Result:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x : E
a✝⁵ : x ∈ univ
y : E
a✝⁴ : y ∈ univ
a✝³ : x ≠ y
a b : 𝕜
a✝² : 0 < a
a✝¹ : 0 < b
a✝ : a + b = 1
⊢ a • x + b • y ∈ interior univ
-- Mathlib/Topology/Order.lean
theorem gc_nhds (a : α) : GaloisConnection (nhdsAdjoint a) fun t => @nhds α t a := fun f t => by
  rw [le_nhds_iff]
  exact ⟨fun H s hs has => H _ has hs, fun H s has hs => H _ hs has⟩

Proof state:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ ∀ (s : Set α), a ∈ s → IsOpen s → s ∈ f

Tactic:
exact ⟨fun H s hs has => H _ has hs, fun H s has hs => H _ hs has⟩

Result:
no goals

Proof state:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ f ≤ (fun t => 𝓝 a) t

Tactic:
rw [le_nhds_iff]

Result:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ ∀ (s : Set α), a ∈ s → IsOpen s → s ∈ f
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem degree_add_div (hq0 : q ≠ 0) (hpq : degree q ≤ degree p) :
    degree q + degree (p / q) = degree p

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
hpq : q.degree ≤ p.degree
this : (p % q).degree < (q * (p / q)).degree
⊢ q.degree + (p / q).degree = p.degree

Tactic:
conv_rhs =>
  rw [← EuclideanDomain.div_add_mod p q, degree_add_eq_left_of_degree_lt this, degree_mul]

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
hpq : q.degree ≤ p.degree
⊢ q.degree + (p / q).degree = p.degree

Tactic:
have : degree (p % q) < degree (q * (p / q)) :=
  calc
    degree (p % q) < degree q := EuclideanDomain.mod_lt _ hq0
    _ ≤ _ := degree_le_mul_left _ (mt (div_eq_zero_iff hq0).1 (not_lt_of_ge hpq))

Result:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
hpq : q.degree ≤ p.degree
this : (p % q).degree < (q * (p / q)).degree
⊢ q.degree + (p / q).degree = p.degree
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.le_lo (u w v k : Nat) : u ≤ w → w + k ≤ v → u + k ≤ v

Proof state:
u w v k : Nat
⊢ u ≤ w → w + k ≤ v → u + k ≤ v

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem summable_norm_apply (p : FormalMultilinearSeries 𝕜 E F) {x : E}
    (hx : x ∈ EMetric.ball (0 : E) p.radius) : Summable fun n : ℕ => ‖p n fun _ => x‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
hx : x ∈ EMetric.ball 0 p.radius
⊢ Summable fun n => ‖(p n) fun x_1 => x‖

Tactic:
rw [mem_emetric_ball_zero_iff] at hx

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
hx : ‖x‖ₑ < p.radius
⊢ Summable fun n => ‖(p n) fun x_1 => x‖

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
hx : ‖x‖ₑ < p.radius
⊢ Summable fun n => ‖(p n) fun x_1 => x‖

Tactic:
refine .of_nonneg_of_le
  (fun _ ↦ norm_nonneg _) (fun n ↦ ((p n).le_opNorm _).trans_eq ?_) (p.summable_norm_mul_pow hx)

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
hx : ‖x‖ₑ < p.radius
n : ℕ
⊢ ‖p n‖ * ∏ i : Fin n, ‖x‖ = ‖p n‖ * ↑‖x‖₊ ^ n

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
hx : ‖x‖ₑ < p.radius
n : ℕ
⊢ ‖p n‖ * ∏ i : Fin n, ‖x‖ = ‖p n‖ * ↑‖x‖₊ ^ n

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem sub_def' (a b : Rat) : a - b = mkRat (a.num * b.den - b.num * a.den) (a.den * b.den)

Proof state:
a b : Rat
⊢ a - b = mkRat (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den)

Tactic:
rw [sub_def, normalize_eq_mkRat]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lt_sup {ι : Type u} {f : ι → Ordinal.{max u v}} {a} : a < sup.{_, v} f ↔ ∃ i, a < f i

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ a < sup f ↔ ∃ i, a < f i

Tactic:
simpa only [not_forall, not_le] using not_congr (@sup_le_iff.{_, v} _ f a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.srem_umod (x y : BitVec w) :
    x.srem y =
      bif x.getLsbD (w - 1) then
        bif y.getLsbD (w - 1) then
          -((-x) % (-y))
        else
          -((-x) % y)
      else
        bif y.getLsbD (w - 1) then
          x % (-y)
        else
          x % y

Proof state:
w : Nat
x y : BitVec w
⊢ x.srem y =
    bif x.getLsbD (w - 1) then bif y.getLsbD (w - 1) then -(-x % -y) else -(-x % y)
    else bif y.getLsbD (w - 1) then x % -y else x % y

Tactic:
rw [BitVec.srem_eq, ← BitVec.msb_eq_getLsbD_last, ← BitVec.msb_eq_getLsbD_last]

Result:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x % y
    | false, true => x % -y
    | true, false => -(-x % y)
    | true, true => -(-x % -y)) =
    bif x.msb then bif y.msb then -(-x % -y) else -(-x % y) else bif y.msb then x % -y else x % y

Proof state:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x % y
    | false, true => x % -y
    | true, false => -(-x % y)
    | true, true => -(-x % -y)) =
    bif x.msb then bif y.msb then -(-x % -y) else -(-x % y) else bif y.msb then x % -y else x % y

Tactic:
cases x.msb <;> cases y.msb <;> simp

Result:
no goals
-- Mathlib/ModelTheory/Basic.lean
theorem toFun_inducedStructureEquiv_Symm (e : M ≃ N) :
    (by
    letI : L.Structure N := inducedStructure e
    exact DFunLike.coe (@inducedStructureEquiv L M N _ e).symm) = (e.symm : N → M) :=
  rfl

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝ : L.Structure M
e : M ≃ N
⊢ N → M

Tactic:
letI : L.Structure N := inducedStructure e

Result:
L : Language
M : Type u_1
N : Type u_2
inst✝ : L.Structure M
e : M ≃ N
this : L.Structure N := e.inducedStructure
⊢ N → M

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝ : L.Structure M
e : M ≃ N
this : L.Structure N := e.inducedStructure
⊢ N → M

Tactic:
exact DFunLike.coe (@inducedStructureEquiv L M N _ e).symm

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem nodupKeys_cons {s : Sigma β} {l : List (Sigma β)} :
    NodupKeys (s :: l) ↔ s.1 ∉ l.keys ∧ NodupKeys l

Proof state:
α : Type u
β : α → Type v
s : Sigma β
l : List (Sigma β)
⊢ (s :: l).NodupKeys ↔ s.fst ∉ l.keys ∧ l.NodupKeys

Tactic:
simp [keys, NodupKeys]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean
theorem exists_mul_lt_apply_of_lt_opNNNorm (f : E →SL[σ₁₂] F) {r : ℝ≥0} (hr : r < ‖f‖₊) :
    ∃ x, r * ‖x‖₊ < ‖f x‖₊

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_6
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
⊢ ∃ x, r * ‖x‖₊ < ‖f x‖₊

Tactic:
simpa only [not_forall, not_le, Set.mem_setOf] using
  not_mem_of_lt_csInf (nnnorm_def f ▸ hr : r < sInf { c : ℝ≥0 | ∀ x, ‖f x‖₊ ≤ c * ‖x‖₊ })
    (OrderBot.bddBelow _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldl_append {β : Type _} (f : β → α → β) (b) (l : Vector α n) (l' : Vector α k) :
    (l ++ l').foldl f b = l'.foldl f (l.foldl f b)

Proof state:
α : Type u_1
n k : Nat
β : Type u_2
f : β → α → β
b : β
l : Vector α n
l' : Vector α k
⊢ foldl f b (l ++ l') = foldl f (foldl f b l) l'

Tactic:
simp [foldl_eq_foldlM]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem _root_.IsOpen.analyticSet_image {β : Type*} [TopologicalSpace β] [PolishSpace β]
    {s : Set β} (hs : IsOpen s) {f : β → α} (f_cont : Continuous f) : AnalyticSet (f '' s)

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
s : Set β
hs : IsOpen s
f : β → α
f_cont : Continuous f
⊢ AnalyticSet (range fun x => f ↑x)

Tactic:
haveI : PolishSpace s := hs.polishSpace

Result:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
s : Set β
hs : IsOpen s
f : β → α
f_cont : Continuous f
this : PolishSpace ↑s
⊢ AnalyticSet (range fun x => f ↑x)

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
s : Set β
hs : IsOpen s
f : β → α
f_cont : Continuous f
this : PolishSpace ↑s
⊢ AnalyticSet (range fun x => f ↑x)

Tactic:
exact analyticSet_range_of_polishSpace (f_cont.comp continuous_subtype_val)

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
s : Set β
hs : IsOpen s
f : β → α
f_cont : Continuous f
⊢ AnalyticSet (f '' s)

Tactic:
rw [image_eq_range]

Result:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_3
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
s : Set β
hs : IsOpen s
f : β → α
f_cont : Continuous f
⊢ AnalyticSet (range fun x => f ↑x)
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem mapQ_mkQ (f : M →ₛₗ[τ₁₂] M₂) {h} : (mapQ p q f h).comp p.mkQ = q.mkQ.comp f

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
x : M
⊢ ((p.mapQ q f h).comp p.mkQ) x = (q.mkQ.comp f) x

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ (p.mapQ q f h).comp p.mkQ = q.mkQ.comp f

Tactic:
ext x

Result:
case h
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
x : M
⊢ ((p.mapQ q f h).comp p.mkQ) x = (q.mkQ.comp f) x
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm'_measure_zero_of_pos {f : α → ε} (hq_pos : 0 < q) :
    eLpNorm' f q (0 : Measure α) = 0

Proof state:
α : Type u_1
ε : Type u_2
q : ℝ
inst✝¹ : ENorm ε
inst✝ : MeasurableSpace α
f : α → ε
hq_pos : 0 < q
⊢ eLpNorm' f q 0 = 0

Tactic:
simp [eLpNorm', hq_pos]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Bimon_.lean
theorem compatibility (M : Bimon_ C) :
    (M.comul.hom ⊗ M.comul.hom) ≫
      (α_ _ _ (M.X.X ⊗ M.X.X)).hom ≫ M.X.X ◁ (α_ _ _ _).inv ≫
      M.X.X ◁ (β_ M.X.X M.X.X).hom ▷ M.X.X ≫
      M.X.X ◁ (α_ _ _ _).hom ≫ (α_ _ _ _).inv ≫
      (M.X.mul ⊗ M.X.mul) =
    M.X.mul ≫ M.comul.hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon_ C
this : (M.comul.hom ⊗ M.comul.hom) ≫ (M.X ⊗ M.X).mul = M.X.mul ≫ M.comul.hom
⊢ (M.comul.hom ⊗ M.comul.hom) ≫
      (α_ M.X.X M.X.X (M.X.X ⊗ M.X.X)).hom ≫
        M.X.X ◁ (α_ M.X.X M.X.X M.X.X).inv ≫
          M.X.X ◁ (β_ M.X.X M.X.X).hom ▷ M.X.X ≫
            M.X.X ◁ (α_ M.X.X M.X.X M.X.X).hom ≫ (α_ M.X.X M.X.X (M.X.X ⊗ M.X.X)).inv ≫ (M.X.mul ⊗ M.X.mul) =
    M.X.mul ≫ M.comul.hom

Tactic:
simpa [-Mon_.Hom.mul_hom, tensorμ] using this

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon_ C
⊢ (M.comul.hom ⊗ M.comul.hom) ≫
      (α_ M.X.X M.X.X (M.X.X ⊗ M.X.X)).hom ≫
        M.X.X ◁ (α_ M.X.X M.X.X M.X.X).inv ≫
          M.X.X ◁ (β_ M.X.X M.X.X).hom ▷ M.X.X ≫
            M.X.X ◁ (α_ M.X.X M.X.X M.X.X).hom ≫ (α_ M.X.X M.X.X (M.X.X ⊗ M.X.X)).inv ≫ (M.X.mul ⊗ M.X.mul) =
    M.X.mul ≫ M.comul.hom

Tactic:
have := (Mon_.Hom.mul_hom M.comul).symm

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M : Bimon_ C
this : (M.comul.hom ⊗ M.comul.hom) ≫ (M.X ⊗ M.X).mul = M.X.mul ≫ M.comul.hom
⊢ (M.comul.hom ⊗ M.comul.hom) ≫
      (α_ M.X.X M.X.X (M.X.X ⊗ M.X.X)).hom ≫
        M.X.X ◁ (α_ M.X.X M.X.X M.X.X).inv ≫
          M.X.X ◁ (β_ M.X.X M.X.X).hom ▷ M.X.X ≫
            M.X.X ◁ (α_ M.X.X M.X.X M.X.X).hom ≫ (α_ M.X.X M.X.X (M.X.X ⊗ M.X.X)).inv ≫ (M.X.mul ⊗ M.X.mul) =
    M.X.mul ≫ M.comul.hom
-- Mathlib/Data/Nat/Cast/Defs.lean
theorem cast_ite (P : Prop) [Decidable P] (m n : ℕ) :
    ((ite P m n : ℕ) : R) = ite P (m : R) (n : R)

Proof state:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
⊢ ↑(if P then m else n) = if P then ↑m else ↑n

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_neg_Ioo : Neg.neg '' Ioo a b = Ioo (-b) (-a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ Neg.neg '' Ioo a b = Ioo (-b) (-a)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iUnion_Ico_left (b : α) : ⋃ a, Ico a b = Iio b

Proof state:
α : Type v
inst✝ : Preorder α
b : α
⊢ ⋃ a, Ico a b = Iio b

Tactic:
simp only [← Ici_inter_Iio, ← iUnion_inter, iUnion_Ici, univ_inter]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem top_add_of_ne_bot {x : EReal} (h : x ≠ ⊥) : ⊤ + x = ⊤

Proof state:
case h_bot
h : ⊥ ≠ ⊥
⊢ ⊤ + ⊥ = ⊤

Tactic:
exfalso

Result:
case h_bot
h : ⊥ ≠ ⊥
⊢ False

Proof state:
x : EReal
h : x ≠ ⊥
⊢ ⊤ + x = ⊤

Tactic:
induction x

Result:
case h_bot
h : ⊥ ≠ ⊥
⊢ ⊤ + ⊥ = ⊤

case h_real
a✝ : ℝ
h : ↑a✝ ≠ ⊥
⊢ ⊤ + ↑a✝ = ⊤

case h_top
h : ⊤ ≠ ⊥
⊢ ⊤ + ⊤ = ⊤

Proof state:
case h_real
a✝ : ℝ
h : ↑a✝ ≠ ⊥
⊢ ⊤ + ↑a✝ = ⊤

Tactic:
exact top_add_coe _

Result:
no goals

Proof state:
case h_bot
h : ⊥ ≠ ⊥
⊢ False

Tactic:
exact h (Eq.refl ⊥)

Result:
no goals

Proof state:
case h_top
h : ⊤ ≠ ⊥
⊢ ⊤ + ⊤ = ⊤

Tactic:
exact top_add_top

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_cast {l : Vector α n} {m : Nat} {w : n = m} {i : Nat} :
    (l.cast w)[i]? = l[i]?

Proof state:
case mk
α : Type u_1
m i : Nat
l : Array α
w : l.size = m
⊢ (Vector.cast w { toArray := l, size_toArray := ⋯ })[i]? = { toArray := l, size_toArray := ⋯ }[i]?

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
m : Nat
w : n = m
i : Nat
⊢ (Vector.cast w l)[i]? = l[i]?

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
m i : Nat
l : Array α
w : l.size = m
⊢ (Vector.cast w { toArray := l, size_toArray := ⋯ })[i]? = { toArray := l, size_toArray := ⋯ }[i]?
-- Mathlib/RingTheory/Ideal/Quotient/Basic.lean
theorem subsingleton_iff : Subsingleton (R ⧸ I) ↔ I = ⊤

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ Subsingleton (R ⧸ I) ↔ I = ⊤

Tactic:
rw [Submodule.Quotient.subsingleton_iff, eq_top_iff, SetLike.le_def]

Result:
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ (∀ (x : R), x ∈ I) ↔ ∀ ⦃x : R⦄, x ∈ ⊤ → x ∈ I

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
⊢ (∀ (x : R), x ∈ I) ↔ ∀ ⦃x : R⦄, x ∈ ⊤ → x ∈ I

Tactic:
simp_rw [Submodule.mem_top, true_implies]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean
theorem ordinaryHypergeometricSeries_apply_zero (n : ℕ) :
    (ordinaryHypergeometricSeries 𝔸 a b c n fun _ => 0) = Pi.single (f := fun _ => 𝔸) 0 1 n

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n : ℕ
⊢ ((ordinaryHypergeometricSeries 𝔸 a b c n) fun x => 0) = Pi.single 0 1 n

Tactic:
rw [ordinaryHypergeometricSeries, ofScalars_apply_eq, ordinaryHypergeometricCoefficient]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n : ℕ
⊢ ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      0 ^ n =
    Pi.single 0 1 n

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n : ℕ
⊢ ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      0 ^ n =
    Pi.single 0 1 n

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem iSup₂_inf_eq {f : ∀ i, κ i → α} (a : α) :
    (⨆ (i) (j), f i j) ⊓ a = ⨆ (i) (j), f i j ⊓ a

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
f : (i : ι) → κ i → α
a : α
⊢ (⨆ i, ⨆ j, f i j) ⊓ a = ⨆ i, ⨆ j, f i j ⊓ a

Tactic:
simp only [iSup_inf_eq]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
@[simp] lemma Iic_True : Iic True = univ

Proof state:
⊢ Iic True = univ

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_sub_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_sub_natCast hx y 1

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem card_support_eq_zero {f : α →₀ M} : #f.support = 0 ↔ f = 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
⊢ #f.support = 0 ↔ f = 0

Tactic:
simp

Result:
no goals