harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Image.lean
theorem property_of_mem_map_subtype {p : α → Prop} (s : Finset { x // p x }) {a : α}
    (h : a ∈ s.map (Embedding.subtype _)) : p a

Proof state:
α : Type u_1
p : α → Prop
s : Finset { x // p x }
a : α
h : a ∈ map (Embedding.subtype fun x => p x) s
⊢ p a

Tactic:
rcases mem_map.1 h with ⟨x, _, rfl⟩

Result:
case intro.intro
α : Type u_1
p : α → Prop
s : Finset { x // p x }
x : { x // p x }
left✝ : x ∈ s
h : (Embedding.subtype fun x => p x) x ∈ map (Embedding.subtype fun x => p x) s
⊢ p ((Embedding.subtype fun x => p x) x)

Proof state:
case intro.intro
α : Type u_1
p : α → Prop
s : Finset { x // p x }
x : { x // p x }
left✝ : x ∈ s
h : (Embedding.subtype fun x => p x) x ∈ map (Embedding.subtype fun x => p x) s
⊢ p ((Embedding.subtype fun x => p x) x)

Tactic:
exact x.2

Result:
no goals
-- Mathlib/GroupTheory/IndexNormal.lean
theorem normal_of_index_eq_one (hH : H.index = 1) : H.Normal

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.index = 1
⊢ H.Normal

Tactic:
rw [index_eq_one] at hH

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H = ⊤
⊢ H.Normal

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H = ⊤
⊢ H.Normal

Tactic:
rw [hH]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H = ⊤
⊢ ⊤.Normal

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H = ⊤
⊢ ⊤.Normal

Tactic:
infer_instance

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
/-- if `f` is integrable, then `g + f` is integrable iff `g` is.
See `integrable_add_iff_integrable_left'` for the same statement with `fun x ↦ g x + f x` instead
of `g + f`. -/
@[simp]
lemma integrable_add_iff_integrable_left {f g : α → β} (hf : Integrable f μ) :
    Integrable (g + f) μ ↔ Integrable g μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
⊢ Integrable (g + f) μ ↔ Integrable g μ

Tactic:
rw [add_comm, integrable_add_iff_integrable_right hf]

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem connectedComponentIn_subset (F : Set α) (x : α) : connectedComponentIn F x ⊆ F

Proof state:
α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
⊢ connectedComponentIn F x ⊆ F

Tactic:
rw [connectedComponentIn]

Result:
α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
⊢ (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅) ⊆ F

Proof state:
α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
⊢ (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅) ⊆ F

Tactic:
split_ifs <;> simp

Result:
no goals
-- Mathlib/Algebra/Lie/Killing.lean
lemma killingForm_nondegenerate :
    (killingForm R L).Nondegenerate

Proof state:
R : Type u_1
L : Type u_3
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsKilling R L
⊢ (killingForm R L).Nondegenerate

Tactic:
simp [LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Lucas.lean
theorem choose_modEq_prod_range_choose {a : ℕ} (ha₁ : n < p ^ a) (ha₂ : k < p ^ a) :
    choose n k ≡ ∏ i ∈ range a, choose (n / p ^ i % p) (k / p ^ i % p) [ZMOD p]

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ ↑(n.choose k) ≡ ∏ i ∈ range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Tactic:
apply (choose_modEq_choose_mul_prod_range_choose a).trans

Result:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ ↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ∏ i ∈ range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Proof state:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
ha₁ : n < p ^ a
ha₂ : k < p ^ a
⊢ ↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ∏ i ∈ range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]

Tactic:
simp_rw [Nat.div_eq_of_lt ha₁, Nat.div_eq_of_lt ha₂, choose, cast_one, one_mul, cast_prod,
  Int.ModEq.refl]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_self_eq_norm_mul_norm (x : E) : re ⟪x, x⟫ = ‖x‖ * ‖x‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ re ⟪x, x⟫_𝕜 = ‖x‖ * ‖x‖

Tactic:
rw [@norm_eq_sqrt_inner 𝕜, ← sqrt_mul inner_self_nonneg (re ⟪x, x⟫),
  sqrt_mul_self inner_self_nonneg]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Prefunctor.lean
theorem congr_hom {U V : Type*} [Quiver U] [Quiver V] {F G : U ⥤q V} (e : F = G) {X Y : U}
    (f : X ⟶ Y) : Quiver.homOfEq (F.map f) (congr_obj e X) (congr_obj e Y) = G.map f

Proof state:
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = F.map f

Tactic:
simp

Result:
no goals

Proof state:
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F G : U ⥤q V
e : F = G
X Y : U
f : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f

Tactic:
subst e

Result:
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = F.map f
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reflect_C (r : R) (N : ℕ) : reflect N (C r) = C r * X ^ N

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
N : ℕ
⊢ reflect N (C r) = C r * X ^ N

Tactic:
conv_lhs => rw [← mul_one (C r), ← pow_zero X, reflect_C_mul_X_pow, revAt_zero]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Decomposition.lean
theorem decompose_of_mem_ne {x : M} {i j : ι} (hx : x ∈ ℳ i) (hij : i ≠ j) :
    (decompose ℳ x j : M) = 0

Proof state:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i j : ι
hx : x ∈ ℳ i
hij : i ≠ j
⊢ ↑(((decompose ℳ) x) j) = 0

Tactic:
rw [decompose_of_mem _ hx, DirectSum.of_eq_of_ne _ _ _ hij, ZeroMemClass.coe_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
protected lemma add_lt_add_right [LT α] [AddRightStrictMono α] (hz : z ≠ ⊥) :
    x < y → x + z < y + z

Proof state:
α : Type u
inst✝² : Add α
x y z : WithBot α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
hz : z ≠ ⊥
⊢ x < y → x + z < y + z

Tactic:
lift z to α using hz

Result:
case intro
α : Type u
inst✝² : Add α
x y : WithBot α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ x < y → x + ↑z < y + ↑z

Proof state:
case intro
α : Type u
inst✝² : Add α
x y : WithBot α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ x < y → x + ↑z < y + ↑z

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Result:
case intro.coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝¹ a✝ : α
⊢ a✝¹ < a✝ → a✝¹ + z < a✝ + z
-- Mathlib/Data/Complex/Order.lean
@[simp]
lemma re_eq_norm {z : ℂ} : z.re = ‖z‖ ↔ 0 ≤ z :=
  have : 0 ≤ ‖z‖ := norm_nonneg z
  ⟨fun h ↦ ⟨h.symm ▸ this, (abs_re_eq_norm.1 <| h.symm ▸ abs_of_nonneg this).symm⟩,
    fun ⟨h₁, h₂⟩ ↦ by rw [← abs_re_eq_norm.2 h₂.symm, abs_of_nonneg h₁]⟩

Proof state:
z : ℂ
this : 0 ≤ ‖z‖
x✝ : 0 ≤ z
h₁ : re 0 ≤ z.re
h₂ : im 0 = z.im
⊢ z.re = ‖z‖

Tactic:
rw [← abs_re_eq_norm.2 h₂.symm, abs_of_nonneg h₁]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem TendstoInMeasure.exists_seq_tendsto_ae' {u : Filter ι} [NeBot u] [IsCountablyGenerated u]
    {f : ι → α → E} {g : α → E} (hfg : TendstoInMeasure μ f u g) :
    ∃ ns : ℕ → ι, Tendsto ns atTop u ∧ ∀ᵐ x ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))

Proof state:
case intro.intro
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ms : ℕ → ι
hms1 : Tendsto ms atTop u
hms2 : TendstoInMeasure μ (fun n => f (ms n)) atTop g
⊢ ∃ ns, Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))

Tactic:
obtain ⟨ns, hns1, hns2⟩ := hms2.exists_seq_tendsto_ae

Result:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ms : ℕ → ι
hms1 : Tendsto ms atTop u
hms2 : TendstoInMeasure μ (fun n => f (ms n)) atTop g
ns : ℕ → ℕ
hns1 : StrictMono ns
hns2 : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ms (ns i)) x) atTop (𝓝 (g x))
⊢ ∃ ns, Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
⊢ ∃ ns, Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))

Tactic:
obtain ⟨ms, hms1, hms2⟩ := hfg.exists_seq_tendstoInMeasure_atTop

Result:
case intro.intro
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ms : ℕ → ι
hms1 : Tendsto ms atTop u
hms2 : TendstoInMeasure μ (fun n => f (ms n)) atTop g
⊢ ∃ ns, Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))

Proof state:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝² : MetricSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hfg : TendstoInMeasure μ f u g
ms : ℕ → ι
hms1 : Tendsto ms atTop u
hms2 : TendstoInMeasure μ (fun n => f (ms n)) atTop g
ns : ℕ → ℕ
hns1 : StrictMono ns
hns2 : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ms (ns i)) x) atTop (𝓝 (g x))
⊢ ∃ ns, Tendsto ns atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))

Tactic:
exact ⟨ms ∘ ns, hms1.comp hns1.tendsto_atTop, hns2⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem filter_subset {l₁ l₂ : List α} (p : α → Bool) (H : l₁ ⊆ l₂) : filter p l₁ ⊆ filter p l₂ :=
  fun x => by simp_all [mem_filter, subset_def.1 H]

Proof state:
α : Type u_1
l₁ l₂ : List α
p : α → Bool
H : l₁ ⊆ l₂
x : α
⊢ x ∈ filter p l₁ → x ∈ filter p l₂

Tactic:
simp_all [mem_filter, subset_def.1 H]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_insertList_of_contains_eq_false [BEq α] [EquivBEq α] [Inhabited α]
    {l toInsert : List ((a : α) × β a)} {k : α}
    (contains_false : (toInsert.map Sigma.fst).contains k = false) :
    getKey! k (insertList l toInsert) = getKey! k l

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
l toInsert : List ((a : α) × β a)
k : α
contains_false : (List.map Sigma.fst toInsert).contains k = false
⊢ getKey! k (insertList l toInsert) = getKey! k l

Tactic:
rw [getKey!_eq_getKey?, getKey?_insertList_of_contains_eq_false contains_false, getKey!_eq_getKey?]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_map_hom (L : List ι) (f : ι → M) {G : Type*} [FunLike G M N] [MonoidHomClass G M N]
    (g : G) :
    (L.map (g ∘ f)).prod = g (L.map f).prod

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
L : List ι
f : ι → M
G : Type u_8
inst✝¹ : FunLike G M N
inst✝ : MonoidHomClass G M N
g : G
⊢ (map (⇑g ∘ f) L).prod = g (map f L).prod

Tactic:
rw [← prod_hom, map_map]

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem flip_separatingLeft {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M} :
    B.flip.SeparatingLeft ↔ SeparatingRight B

Proof state:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : CommSemiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
⊢ B.flip.SeparatingLeft ↔ B.SeparatingRight

Tactic:
rw [← flip_separatingRight, flip_flip]

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- `m` is `n`-smooth if and only if `m` is nonzero and all prime divisors `≤ m` of `m`
are less than `n`. -/
lemma mem_smoothNumbers_iff_forall_le {n m : ℕ} :
    m ∈ smoothNumbers n ↔ m ≠ 0 ∧ ∀ p ≤ m, p.Prime → p ∣ m → p < n

Proof state:
n m : ℕ
⊢ m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p < n

Tactic:
simp only [smoothNumbers_eq_factoredNumbers, mem_factoredNumbers_iff_forall_le, Finset.mem_range]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Continuity.lean
theorem tendsto_iff_norm_div_tendsto_zero {f : α → E} {a : Filter α} {b : E} :
    Tendsto f a (𝓝 b) ↔ Tendsto (fun e => ‖f e / b‖) a (𝓝 0)

Proof state:
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
f : α → E
a : Filter α
b : E
⊢ Tendsto f a (𝓝 b) ↔ Tendsto (fun e => ‖f e / b‖) a (𝓝 0)

Tactic:
simp only [← dist_eq_norm_div, ← tendsto_iff_dist_tendsto_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorCompIsoId_zero_zero_hom_app (X : C) :
    (shiftFunctorCompIsoId C 0 0 (add_zero 0)).hom.app X =
      ((shiftFunctorZero C A).hom.app X)⟦0⟧' ≫ (shiftFunctorZero C A).hom.app X

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
⊢ (shiftFunctorCompIsoId C 0 0 ⋯).hom.app X =
    (shiftFunctor C 0).map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero C A).hom.app X

Tactic:
simp [shiftFunctorCompIsoId, shiftFunctorAdd'_zero_add_inv_app]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
@[to_additive]
lemma isComplement_subgroup_left_iff_existsUnique_quotientMk'' :
    IsComplement H T ↔
      ∀ q : Quotient (QuotientGroup.rightRel H), ∃! t : T, Quotient.mk'' t.1 = q

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
⊢ IsComplement (↑H) T ↔ ∀ (q : Quotient (QuotientGroup.rightRel H)), ∃! t, Quotient.mk'' ↑t = q

Tactic:
simp_rw [isComplement_iff_existsUnique_mul_inv_mem, SetLike.mem_coe,
  ← QuotientGroup.rightRel_apply, ← Quotient.eq'', Quotient.forall]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem add_zero (x : BitVec n) : x + 0#n = x

Proof state:
n : Nat
x : BitVec n
⊢ x + 0#n = x

Tactic:
simp [add_def]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem abs_volumeForm_apply_of_orthonormal (v : OrthonormalBasis (Fin n) ℝ E) :
    |o.volumeForm v| = 1

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
v : OrthonormalBasis (Fin n) ℝ E
⊢ |o.volumeForm ⇑v| = 1

Tactic:
simpa [o.volumeForm_robust' v v] using congr_arg abs v.toBasis.det_self

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem add_le_iff {a b c : Ordinal} (hb : b ≠ 0) : a + b ≤ c ↔ ∀ d < b, a + d < c

Proof state:
a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ a + b ≤ c ↔ ∀ d < b, a + d < c

Tactic:
simpa using (lt_add_iff hb).not

Result:
no goals
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem perpBisector_ne_bot : perpBisector p₁ p₂ ≠ ⊥

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ (↑(perpBisector p₁ p₂)).Nonempty

Tactic:
exact perpBisector_nonempty

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ perpBisector p₁ p₂ ≠ ⊥

Tactic:
rw [← nonempty_iff_ne_bot]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ (↑(perpBisector p₁ p₂)).Nonempty
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem direction_inf (s₁ s₂ : AffineSubspace k P) :
    (s₁ ⊓ s₂).direction ≤ s₁.direction ⊓ s₂.direction

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ Submodule.span k (↑(s₁ ⊓ s₂) -ᵥ ↑(s₁ ⊓ s₂)) ≤ Submodule.span k (↑s₁ -ᵥ ↑s₁) ⊓ Submodule.span k (↑s₂ -ᵥ ↑s₂)

Tactic:
exact
  le_inf (sInf_le_sInf fun p hp => trans (vsub_self_mono inter_subset_left) hp)
    (sInf_le_sInf fun p hp => trans (vsub_self_mono inter_subset_right) hp)

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ (s₁ ⊓ s₂).direction ≤ s₁.direction ⊓ s₂.direction

Tactic:
simp only [direction_eq_vectorSpan, vectorSpan_def]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s₁ s₂ : AffineSubspace k P
⊢ Submodule.span k (↑(s₁ ⊓ s₂) -ᵥ ↑(s₁ ⊓ s₂)) ≤ Submodule.span k (↑s₁ -ᵥ ↑s₁) ⊓ Submodule.span k (↑s₂ -ᵥ ↑s₂)
-- Mathlib/Control/Monad/Cont.lean
theorem WriterT.goto_mkLabel' {α β ω : Type _} [Monoid ω] (x : Label (α × ω) m β) (i : α) :
    goto (WriterT.mkLabel' x) i = monadLift (goto x (i, 1))

Proof state:
case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : Monoid ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel' { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, 1))

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : Monoid ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel' x) i = monadLift (goto x (i, 1))

Tactic:
cases x

Result:
case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : Monoid ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel' { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, 1))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem map_eq_mapTR : @map = @mapTR :=
  funext fun α => funext fun β => funext fun f => funext fun as => by
    simp [mapTR, mapTR_loop_eq]

Proof state:
α : Type u_2
β : Type u_1
f : α → β
as : List α
⊢ map f as = mapTR f as

Tactic:
simp [mapTR, mapTR_loop_eq]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Binomial.lean
theorem binomial_apply_last (p : ℝ≥0∞) (h : p ≤ 1) (n : ℕ) :
    binomial p h n (.last n) = p^n

Proof state:
p : ℝ≥0∞
h : p ≤ 1
n : ℕ
⊢ (binomial p h n) (Fin.last n) = p ^ n

Tactic:
simp [binomial_apply]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem ext (j k : S → P) (hj1 : j 1 = 1) (hk1 : k 1 = 1)
    (hjm : ∀ a b, j (a * b) = j a * j b) (hkm : ∀ a b, k (a * b) = k a * k b)
    (h : ∀ a, j (algebraMap R S a) = k (algebraMap R S a)) : j = k :=
  let j' : MonoidHom S P :=
    { toFun := j, map_one' := hj1, map_mul' := hjm }
  let k' : MonoidHom S P :=
    { toFun := k, map_one' := hk1, map_mul' := hkm }
  have : j' = k' := monoidHom_ext M (MonoidHom.ext h)
  show j'.toFun = k'.toFun by rw [this]

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
j k : S → P
hj1 : j 1 = 1
hk1 : k 1 = 1
hjm : ∀ (a b : S), j (a * b) = j a * j b
hkm : ∀ (a b : S), k (a * b) = k a * k b
h : ∀ (a : R), j ((algebraMap R S) a) = k ((algebraMap R S) a)
j' : S →* P := { toFun := j, map_one' := hj1, map_mul' := hjm }
k' : S →* P := { toFun := k, map_one' := hk1, map_mul' := hkm }
this : j' = k'
⊢ (↑j').toFun = (↑k').toFun

Tactic:
rw [this]

Result:
no goals
-- Mathlib/Data/Multiset/Nodup.lean
theorem nodup_iff_count_eq_one [DecidableEq α] : Nodup s ↔ ∀ a ∈ s, count a s = 1 :=
  Quot.induction_on s fun _l => by simpa using List.nodup_iff_count_eq_one

Proof state:
α : Type u_1
s : Multiset α
inst✝ : DecidableEq α
_l : List α
⊢ Nodup (Quot.mk (⇑(isSetoid α)) _l) ↔ ∀ a ∈ Quot.mk (⇑(isSetoid α)) _l, count a (Quot.mk (⇑(isSetoid α)) _l) = 1

Tactic:
simpa using List.nodup_iff_count_eq_one

Result:
no goals
-- Mathlib/Topology/Algebra/Algebra/Equiv.lean
theorem toAlgEquiv_injective : Function.Injective (toAlgEquiv : (A ≃A[R] B) → A ≃ₐ[R] B)

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Injective toAlgEquiv

Tactic:
rintro ⟨e, _, _⟩ ⟨e', _, _⟩ rfl

Result:
case mk.mk
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
continuous_toFun✝¹ : Continuous e.toFun
continuous_invFun✝¹ : Continuous e.invFun
continuous_toFun✝ :
  Continuous { toAlgEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }.toFun
continuous_invFun✝ :
  Continuous
    { toAlgEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }.invFun
⊢ { toAlgEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ } =
    {
      toAlgEquiv :=
        { toAlgEquiv := e, continuous_toFun := continuous_toFun✝¹,
            continuous_invFun := continuous_invFun✝¹ }.toAlgEquiv,
      continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }

Proof state:
case mk.mk
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
continuous_toFun✝¹ : Continuous e.toFun
continuous_invFun✝¹ : Continuous e.invFun
continuous_toFun✝ :
  Continuous { toAlgEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }.toFun
continuous_invFun✝ :
  Continuous
    { toAlgEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }.invFun
⊢ { toAlgEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ } =
    {
      toAlgEquiv :=
        { toAlgEquiv := e, continuous_toFun := continuous_toFun✝¹,
            continuous_invFun := continuous_invFun✝¹ }.toAlgEquiv,
      continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/LocallyClosed.lean
lemma subset_coborder :
    s ⊆ coborder s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ Disjoint s (closure s \ s)

Tactic:
exact disjoint_sdiff_self_right

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ s ⊆ coborder s

Tactic:
rw [coborder, subset_compl_iff_disjoint_right]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ Disjoint s (closure s \ s)
-- Mathlib/SetTheory/Nimber/Field.lean
theorem cons_mem_invSet {a' : Nimber} (ha₀ : a' ≠ 0) (ha : a' < a) (hb : b ∈ invSet a) :
    invAux a' * (1 + (a + a') * b) ∈ invSet a

Proof state:
a b a' : Nimber
ha₀ : a' ≠ 0
ha : a' < a
hb : b ∈ a.invSet
⊢ a'.invAux * (1 + (a + a') * b) ∈ a.invSet

Tactic:
rw [invSet] at hb ⊢

Result:
a b a' : Nimber
ha₀ : a' ≠ 0
ha : a' < a
hb : b ∈ ⋂₀ {s | 0 ∈ s ∧ ∀ a' < a, a' ≠ 0 → ∀ b ∈ s, a'.invAux * (1 + (a + a') * b) ∈ s}
⊢ a'.invAux * (1 + (a + a') * b) ∈ ⋂₀ {s | 0 ∈ s ∧ ∀ a' < a, a' ≠ 0 → ∀ b ∈ s, a'.invAux * (1 + (a + a') * b) ∈ s}

Proof state:
a b a' : Nimber
ha₀ : a' ≠ 0
ha : a' < a
hb : b ∈ ⋂₀ {s | 0 ∈ s ∧ ∀ a' < a, a' ≠ 0 → ∀ b ∈ s, a'.invAux * (1 + (a + a') * b) ∈ s}
⊢ a'.invAux * (1 + (a + a') * b) ∈ ⋂₀ {s | 0 ∈ s ∧ ∀ a' < a, a' ≠ 0 → ∀ b ∈ s, a'.invAux * (1 + (a + a') * b) ∈ s}

Tactic:
exact Set.mem_sInter.2 fun _ hs => hs.2 _ ha ha₀ _ (Set.mem_sInter.1 hb _ hs)

Result:
no goals