harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem unitOfDetInvertible_eq_nonsingInvUnit [Invertible A.det] :
    unitOfDetInvertible A = nonsingInvUnit A (isUnit_of_invertible _)

Proof state:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A.det
⊢ A.unitOfDetInvertible = A.nonsingInvUnit ⋯

Tactic:
ext

Result:
case a.a
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A.det
i✝ j✝ : n
⊢ ↑A.unitOfDetInvertible i✝ j✝ = ↑(A.nonsingInvUnit ⋯) i✝ j✝

Proof state:
case a.a
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A.det
i✝ j✝ : n
⊢ ↑A.unitOfDetInvertible i✝ j✝ = ↑(A.nonsingInvUnit ⋯) i✝ j✝

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem map_ext'' {f g : AdicCompletion I M →ₗ[R] N}
    (h : f.comp (AdicCompletion.mk I M) = g.comp (AdicCompletion.mk I M)) :
    f = g

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f g : AdicCompletion I M →ₗ[R] N
h : f ∘ₗ mk I M = g ∘ₗ mk I M
⊢ f = g

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f g : AdicCompletion I M →ₗ[R] N
h : f ∘ₗ mk I M = g ∘ₗ mk I M
x : AdicCompletion I M
⊢ f x = g x

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f g : AdicCompletion I M →ₗ[R] N
h : f ∘ₗ mk I M = g ∘ₗ mk I M
x : AdicCompletion I M
⊢ f x = g x

Tactic:
apply induction_on I M x (fun a ↦ LinearMap.ext_iff.mp h a)

Result:
no goals
-- Mathlib/Data/DFinsupp/WellFounded.lean
theorem Lex.wellFounded (hbot : ∀ ⦃i a⦄, ¬s i a 0) (hs : ∀ i, WellFounded (s i))
    (hr : WellFounded <| rᶜ ⊓ (· ≠ ·)) : WellFounded (DFinsupp.Lex r s) :=
  ⟨fun x => by classical exact Lex.acc hbot hs x fun i _ => hr.apply i⟩

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
hr : WellFounded (rᶜ ⊓ fun x1 x2 => x1 ≠ x2)
x : Π₀ (i : ι), α i
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
exact Lex.acc hbot hs x fun i _ => hr.apply i

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
hs : ∀ (i : ι), WellFounded (s i)
hr : WellFounded (rᶜ ⊓ fun x1 x2 => x1 ≠ x2)
x : Π₀ (i : ι), α i
⊢ Acc (DFinsupp.Lex r s) x

Tactic:
classical exact Lex.acc hbot hs x fun i _ => hr.apply i

Result:
no goals
-- Mathlib/Order/Partition/Finpartition.lean
theorem exists_subset_part_bijOn : ∃ r ⊆ s, Set.BijOn P.part r P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∃ r ⊆ s, Set.BijOn P.part ↑r ↑P.parts

Tactic:
obtain ⟨r, hrs, hr⟩ := P.part_surjOn.exists_bijOn_subset

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
r : Set α
hrs : r ⊆ ↑s
hr : Set.BijOn P.part r ↑P.parts
⊢ ∃ r ⊆ s, Set.BijOn P.part ↑r ↑P.parts

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
r : Set α
hrs : r ⊆ ↑s
hr : Set.BijOn P.part r ↑P.parts
⊢ ∃ r ⊆ s, Set.BijOn P.part ↑r ↑P.parts

Tactic:
lift r to Finset α using s.finite_toSet.subset hrs

Result:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
r : Finset α
hrs : ↑r ⊆ ↑s
hr : Set.BijOn P.part ↑r ↑P.parts
⊢ ∃ r ⊆ s, Set.BijOn P.part ↑r ↑P.parts

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
r : Finset α
hrs : ↑r ⊆ ↑s
hr : Set.BijOn P.part ↑r ↑P.parts
⊢ ∃ r ⊆ s, Set.BijOn P.part ↑r ↑P.parts

Tactic:
exact ⟨r, mod_cast hrs, hr⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get_insertIfNew [LawfulBEq α] {k a : α} {v : β k} {h₁} : (m.insertIfNew k v).get a h₁ =
    if h₂ : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h₂.1)) v else m.get a
      (mem_of_mem_insertIfNew' h₁ h₂)

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k a : α
v : β k
h₁ : a ∈ m.insertIfNew k v
⊢ (m.insertIfNew k v).get a h₁ = if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.get a ⋯

Tactic:
exact Raw₀.get_insertIfNew ⟨m.1, _⟩ m.2

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k a : α
v : β k
h₁ : a ∈ m.insertIfNew k v
⊢ (m.insertIfNew k v).get a h₁ = if h₂ : (k == a) = true ∧ ¬k ∈ m then cast ⋯ v else m.get a ⋯

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k a : α
v : β k
h₁ : a ∈ m.insertIfNew k v
⊢ (m.insertIfNew k v).get a h₁ = if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.get a ⋯
-- Mathlib/Analysis/Complex/Basic.lean
theorem ringHom_eq_id_or_conj_of_continuous {f : ℂ →+* ℂ} (hf : Continuous f) :
    f = RingHom.id ℂ ∨ f = conj

Proof state:
f : ℂ →+* ℂ
hf : Continuous ⇑f
⊢ f = RingHom.id ℂ ∨ f = starRingEnd ℂ

Tactic:
simpa only [DFunLike.ext_iff] using real_algHom_eq_id_or_conj (AlgHom.mk' f (map_real_smul f hf))

Result:
no goals
-- Mathlib/Data/NNReal/Basic.lean
theorem mul_iSup_le {a : ℝ≥0} {g : ℝ≥0} {h : ι → ℝ≥0} (H : ∀ j, g * h j ≤ a) : g * iSup h ≤ a

Proof state:
ι : Sort u_2
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ ⨆ i, g * h i ≤ a

Tactic:
exact ciSup_le' H

Result:
no goals

Proof state:
ι : Sort u_2
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ g * iSup h ≤ a

Tactic:
rw [mul_iSup]

Result:
ι : Sort u_2
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), g * h j ≤ a
⊢ ⨆ i, g * h i ≤ a
-- Mathlib/RingTheory/HahnSeries/HEval.lean
theorem coeff_heval (f : PowerSeries R) (g : Γ) :
    (heval hx f).coeff g = ∑ᶠ n, ((powerSeriesFamily hx f).coeff g) n

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
f : R⟦X⟧
g : Γ
⊢ ((heval hx) f).coeff g = ∑ᶠ (n : ℕ), ((powerSeriesFamily hx f).coeff g) n

Tactic:
rw [heval_apply, coeff_hsum]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
f : R⟦X⟧
g : Γ
⊢ ∑ᶠ (i : ℕ), ((powerSeriesFamily hx f) i).coeff g = ∑ᶠ (n : ℕ), ((powerSeriesFamily hx f).coeff g) n

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
f : R⟦X⟧
g : Γ
⊢ ∑ᶠ (i : ℕ), ((powerSeriesFamily hx f) i).coeff g = ∑ᶠ (n : ℕ), ((powerSeriesFamily hx f).coeff g) n

Tactic:
exact rfl

Result:
no goals
-- Mathlib/Analysis/MeanInequalitiesPow.lean
lemma rpow_add_le_add_rpow {p : ℝ} {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hp : 0 ≤ p)
    (hp1 : p ≤ 1) :
    (a + b) ^ p ≤ a ^ p + b ^ p

Proof state:
p a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp : 0 ≤ p
hp1 : p ≤ 1
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
lift a to NNReal using ha

Result:
case intro
p b : ℝ
hb : 0 ≤ b
hp : 0 ≤ p
hp1 : p ≤ 1
a : ℝ≥0
⊢ (↑a + b) ^ p ≤ ↑a ^ p + b ^ p

Proof state:
case intro.intro
p : ℝ
hp : 0 ≤ p
hp1 : p ≤ 1
a b : ℝ≥0
⊢ (↑a + ↑b) ^ p ≤ ↑a ^ p + ↑b ^ p

Tactic:
exact_mod_cast NNReal.rpow_add_le_add_rpow a b hp hp1

Result:
no goals

Proof state:
case intro
p b : ℝ
hb : 0 ≤ b
hp : 0 ≤ p
hp1 : p ≤ 1
a : ℝ≥0
⊢ (↑a + b) ^ p ≤ ↑a ^ p + b ^ p

Tactic:
lift b to NNReal using hb

Result:
case intro.intro
p : ℝ
hp : 0 ≤ p
hp1 : p ≤ 1
a b : ℝ≥0
⊢ (↑a + ↑b) ^ p ≤ ↑a ^ p + ↑b ^ p
-- Mathlib/Algebra/Regular/SMul.lean
theorem IsUnit.isSMulRegular (ua : IsUnit a) : IsSMulRegular M a

Proof state:
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ua : IsUnit a
⊢ IsSMulRegular M a

Tactic:
rcases ua with ⟨a, rfl⟩

Result:
case intro
R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a : Rˣ
⊢ IsSMulRegular M ↑a

Proof state:
case intro
R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a : Rˣ
⊢ IsSMulRegular M ↑a

Tactic:
exact a.isSMulRegular M

Result:
no goals
-- Mathlib/Order/Antichain.lean
theorem image (hs : IsAntichain r s) (f : α → β) (h : ∀ ⦃a b⦄, r' (f a) (f b) → r a b) :
    IsAntichain r' (f '' s)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
f : α → β
h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : f b ≠ f c
hr : r' (f b) (f c)
⊢ False

Tactic:
exact hs hb hc (ne_of_apply_ne _ hbc) (h hr)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
f : α → β
h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b
⊢ IsAntichain r' (f '' s)

Tactic:
rintro _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ hbc hr

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
f : α → β
h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : f b ≠ f c
hr : r' (f b) (f c)
⊢ False
-- Mathlib/Topology/Sets/Closeds.lean
@[simp, norm_cast] lemma Closeds.isAtom_coe [T1Space α] {s : Closeds α} :
    IsAtom (s : Set α) ↔ IsAtom s :=
  Closeds.gi.isAtom_iff' rfl
    (fun t ht ↦ by obtain ⟨x, rfl⟩ := Set.isAtom_iff.1 ht; exact closure_singleton) s

Proof state:
case intro
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Closeds α
x : α
ht : IsAtom {x}
⊢ ↑(Closeds.closure {x}) = {x}

Tactic:
exact closure_singleton

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Closeds α
t : Set α
ht : IsAtom t
⊢ ↑(Closeds.closure t) = t

Tactic:
obtain ⟨x, rfl⟩ := Set.isAtom_iff.1 ht

Result:
case intro
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Closeds α
x : α
ht : IsAtom {x}
⊢ ↑(Closeds.closure {x}) = {x}
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Fractions.lean
lemma fst (h : LeftFraction₂Rel z₁ z₂) : LeftFractionRel z₁.fst z₂.fst

Proof state:
case intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction₂ X Y
Z : C
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
w✝ : z₁.f' ≫ t₁ = z₂.f' ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ LeftFractionRel z₁.fst z₂.fst

Tactic:
exact ⟨Z, t₁, t₂, hst, hft, ht⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction₂ X Y
h : LeftFraction₂Rel z₁ z₂
⊢ LeftFractionRel z₁.fst z₂.fst

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, _, ht⟩ := h

Result:
case intro.intro.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction₂ X Y
Z : C
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
w✝ : z₁.f' ≫ t₁ = z₂.f' ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ LeftFractionRel z₁.fst z₂.fst
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem intMax_add_one {w : Nat} : intMax w + 1#w = intMin w

Proof state:
w : Nat
⊢ (2 ^ (w - 1) - 1 + 1) % 2 ^ w = 2 ^ (w - 1) % 2 ^ w

Tactic:
by_cases h : w = 0

Result:
case pos
w : Nat
h : w = 0
⊢ (2 ^ (w - 1) - 1 + 1) % 2 ^ w = 2 ^ (w - 1) % 2 ^ w

case neg
w : Nat
h : ¬w = 0
⊢ (2 ^ (w - 1) - 1 + 1) % 2 ^ w = 2 ^ (w - 1) % 2 ^ w

Proof state:
w : Nat
⊢ intMax w + 1#w = intMin w

Tactic:
simp only [toNat_eq, toNat_intMax, toNat_add, toNat_intMin, toNat_ofNat, Nat.add_mod_mod]

Result:
w : Nat
⊢ (2 ^ (w - 1) - 1 + 1) % 2 ^ w = 2 ^ (w - 1) % 2 ^ w

Proof state:
case neg
w : Nat
h : ¬w = 0
⊢ (2 ^ (w - 1) - 1 + 1) % 2 ^ w = 2 ^ (w - 1) % 2 ^ w

Tactic:
rw [Nat.sub_add_cancel (Nat.two_pow_pos (w - 1)), Nat.two_pow_pred_mod_two_pow (by omega)]

Result:
no goals

Proof state:
w : Nat
h : ¬w = 0
⊢ 0 < w

Tactic:
omega

Result:
no goals

Proof state:
case pos
w : Nat
h : w = 0
⊢ (2 ^ (w - 1) - 1 + 1) % 2 ^ w = 2 ^ (w - 1) % 2 ^ w

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem head?_take {l : List α} {n : Nat} :
    (l.take n).head? = if n = 0 then none else l.head?

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ (take n l).head? = if n = 0 then none else l.head?

Tactic:
simp [head?_eq_getElem?, getElem?_take]

Result:
α : Type u_1
l : List α
n : Nat
⊢ (if 0 < n then l[0]? else none) = if n = 0 then none else l[0]?

Proof state:
α : Type u_1
l : List α
n : Nat
h✝ : ¬0 < n
⊢ n = 0

Tactic:
omega

Result:
no goals

Proof state:
case isTrue
α : Type u_1
l : List α
n : Nat
h✝ : 0 < n
⊢ l[0]? = if n = 0 then none else l[0]?

Tactic:
rw [if_neg (by omega)]

Result:
no goals

Proof state:
case isFalse
α : Type u_1
l : List α
n : Nat
h✝ : ¬0 < n
⊢ none = if n = 0 then none else l[0]?

Tactic:
rw [if_pos (by omega)]

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
h✝ : 0 < n
⊢ ¬n = 0

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ (if 0 < n then l[0]? else none) = if n = 0 then none else l[0]?

Tactic:
split

Result:
case isTrue
α : Type u_1
l : List α
n : Nat
h✝ : 0 < n
⊢ l[0]? = if n = 0 then none else l[0]?

case isFalse
α : Type u_1
l : List α
n : Nat
h✝ : ¬0 < n
⊢ none = if n = 0 then none else l[0]?
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem uniqueDiffWithinAt_or_nhdsWithin_eq_bot (s : Set 𝕜) (x : 𝕜) :
    UniqueDiffWithinAt 𝕜 s x ∨ 𝓝[s \ {x}] x = ⊥

Proof state:
case inr.refine_1
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
h : (𝓝[s \ {x}] x).NeBot
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x))

Tactic:
simp [tangentCone_eq_univ h]

Result:
no goals

Proof state:
case inr.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
h : (𝓝[s \ {x}] x).NeBot
⊢ (𝓝[s] x).NeBot

Tactic:
apply neBot_of_le (hf := h)

Result:
case inr.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
h : (𝓝[s \ {x}] x).NeBot
⊢ 𝓝[s \ {x}] x ≤ 𝓝[s] x

Proof state:
case inr.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
h : (𝓝[s \ {x}] x).NeBot
⊢ x ∈ closure s

Tactic:
simp only [mem_closure_iff_nhdsWithin_neBot]

Result:
case inr.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
h : (𝓝[s \ {x}] x).NeBot
⊢ (𝓝[s] x).NeBot

Proof state:
case inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
h : 𝓝[s \ {x}] x = ⊥
⊢ UniqueDiffWithinAt 𝕜 s x ∨ 𝓝[s \ {x}] x = ⊥

Tactic:
exact Or.inr h

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
h : (𝓝[s \ {x}] x).NeBot
⊢ UniqueDiffWithinAt 𝕜 s x ∨ 𝓝[s \ {x}] x = ⊥

Tactic:
refine Or.inl ⟨?_, ?_⟩

Result:
case inr.refine_1
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
h : (𝓝[s \ {x}] x).NeBot
⊢ Dense ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x))

case inr.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
h : (𝓝[s \ {x}] x).NeBot
⊢ x ∈ closure s

Proof state:
case inr.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
h : (𝓝[s \ {x}] x).NeBot
⊢ 𝓝[s \ {x}] x ≤ 𝓝[s] x

Tactic:
exact nhdsWithin_mono _ diff_subset

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
⊢ UniqueDiffWithinAt 𝕜 s x ∨ 𝓝[s \ {x}] x = ⊥

Tactic:
rcases eq_or_neBot (𝓝[s \ {x}] x) with h | h

Result:
case inl
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
h : 𝓝[s \ {x}] x = ⊥
⊢ UniqueDiffWithinAt 𝕜 s x ∨ 𝓝[s \ {x}] x = ⊥

case inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : Set 𝕜
x : 𝕜
h : (𝓝[s \ {x}] x).NeBot
⊢ UniqueDiffWithinAt 𝕜 s x ∨ 𝓝[s \ {x}] x = ⊥
-- Mathlib/Data/Finset/Basic.lean
theorem sdiff_union_erase_cancel (hts : t ⊆ s) (ha : a ∈ t) : s \ t ∪ t.erase a = s.erase a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
hts : t ⊆ s
ha : a ∈ t
⊢ s \ t ∪ t.erase a = s.erase a

Tactic:
simp_rw [erase_eq, sdiff_union_sdiff_cancel hts (singleton_subset_iff.2 ha)]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean
@[simp]
lemma inv_hom_apply {M N : SemiNormedGrp₁} (e : M ≅ N) (r : M) : e.inv (e.hom r) = r

Proof state:
M N : SemiNormedGrp₁
e : M ≅ N
r : M.carrier
⊢ ↑(Hom.hom (e.hom ≫ e.inv)) r = r

Tactic:
simp

Result:
no goals

Proof state:
M N : SemiNormedGrp₁
e : M ≅ N
r : M.carrier
⊢ ↑(Hom.hom e.inv) (↑(Hom.hom e.hom) r) = r

Tactic:
rw [← comp_apply]

Result:
M N : SemiNormedGrp₁
e : M ≅ N
r : M.carrier
⊢ ↑(Hom.hom (e.hom ≫ e.inv)) r = r
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem size_erase_of_mem [LawfulBEq α] {a : α} {l : Array α} (h : a ∈ l) :
    (l.erase a).size = l.size - 1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
h : a ∈ l
⊢ (l.erase a).size = l.size - 1

Tactic:
rw [erase_eq_eraseP]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
h : a ∈ l
⊢ (l.eraseP fun x => a == x).size = l.size - 1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
h : a ∈ l
⊢ (l.eraseP fun x => a == x).size = l.size - 1

Tactic:
exact size_eraseP_of_mem h (beq_self_eq_true a)

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toOuterMeasure_apply_finset (s : Finset α) : p.toOuterMeasure s = ∑ x ∈ s, p x

Proof state:
α : Type u_1
p : PMF α
s : Finset α
⊢ p.toOuterMeasure ↑s = ∑ x ∈ s, p x

Tactic:
refine (toOuterMeasure_apply p s).trans ((tsum_eq_sum (s := s) ?_).trans ?_)

Result:
case refine_1
α : Type u_1
p : PMF α
s : Finset α
⊢ ∀ b ∉ s, (↑s).indicator (⇑p) b = 0

case refine_2
α : Type u_1
p : PMF α
s : Finset α
⊢ ∑ b ∈ s, (↑s).indicator (⇑p) b = ∑ x ∈ s, p x

Proof state:
case refine_1
α : Type u_1
p : PMF α
s : Finset α
⊢ ∀ b ∉ s, (↑s).indicator (⇑p) b = 0

Tactic:
exact fun x hx => Set.indicator_of_not_mem (Finset.mem_coe.not.2 hx) _

Result:
no goals

Proof state:
case refine_2
α : Type u_1
p : PMF α
s : Finset α
⊢ ∑ b ∈ s, (↑s).indicator (⇑p) b = ∑ x ∈ s, p x

Tactic:
exact Finset.sum_congr rfl fun x hx => Set.indicator_of_mem (Finset.mem_coe.2 hx) _

Result:
no goals
-- Mathlib/Data/Finite/Perm.lean
theorem card_perm {α : Type*} [Finite α] : Nat.card (Equiv.Perm α) = (Nat.card α)!

Proof state:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (Equiv.Perm α) = (Nat.card α)!

Tactic:
rw [card_eq_fintype_card, card_eq_fintype_card, Fintype.card_perm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Finite α
⊢ Nat.card (Equiv.Perm α) = (Nat.card α)!

Tactic:
have := Fintype.ofFinite α

Result:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card (Equiv.Perm α) = (Nat.card α)!

Proof state:
α : Type u_1
inst✝ : Finite α
⊢ Nat.card (Equiv.Perm α) = (Nat.card α)!

Tactic:
classical
have := Fintype.ofFinite α
rw [card_eq_fintype_card, card_eq_fintype_card, Fintype.card_perm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_filter (xs : List α) (p : α → Bool) (q : α → Bool) :
    (xs.filter p).find? q = xs.find? (fun a => p a ∧ q a)

Proof state:
case nil
α : Type u_1
p q : α → Bool
⊢ find? q (filter p []) = find? (fun a => decide (p a = true ∧ q a = true)) []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : find? q (filter p xs) = find? (fun a => decide (p a = true ∧ q a = true)) xs
⊢ find? q (filter p (x :: xs)) = find? (fun a => decide (p a = true ∧ q a = true)) (x :: xs)

Tactic:
simp only [filter_cons]

Result:
case cons
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : find? q (filter p xs) = find? (fun a => decide (p a = true ∧ q a = true)) xs
⊢ find? q (if p x = true then x :: filter p xs else filter p xs) =
    find? (fun a => decide (p a = true ∧ q a = true)) (x :: xs)

Proof state:
case cons.isFalse
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : find? q (filter p xs) = find? (fun a => decide (p a = true ∧ q a = true)) xs
h✝ : ¬p x = true
⊢ find? q (filter p xs) =
    match decide (p x = true ∧ q x = true) with
    | true => some x
    | false => find? (fun a => decide (p a = true ∧ q a = true)) xs

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case cons.isFalse
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : find? q (filter p xs) = find? (fun a => decide (p a = true ∧ q a = true)) xs
h✝ : ¬p x = true
⊢ find? q (filter p xs) = find? (fun a => decide (p a = true ∧ q a = true)) (x :: xs)

Tactic:
simp only [find?_cons]

Result:
case cons.isFalse
α : Type u_1
p q : α → Bool
x : α
xs : List α
ih : find? q (filter p xs) = find? (fun a => decide (p a = true ∧ q a = true)) xs
h✝ : ¬p x = true
⊢ find? q (filter p xs) =
    match decide (p x = true ∧ q x = true) with
    | true => some x
    | false => find? (fun a => decide (p a = true ∧ q a = true)) xs
-- Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean
@[simp]
lemma smul_coroot : B x x • coroot B hx = 2 • B x

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
⊢ (B x) x • coroot B hx = 2 • B x

Tactic:
ext y

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
y : M
⊢ ((B x) x • coroot B hx) y = (2 • B x) y

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
y : M
⊢ ((B x) x • coroot B hx) y = (2 • B x) y

Tactic:
simp [smul_apply, smul_eq_mul, nsmul_eq_mul, Nat.cast_ofNat, apply_self_mul_coroot_apply]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem aeval_unique (φ : MvPolynomial σ R →ₐ[R] S₁) : φ = aeval (φ ∘ X)

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
φ : MvPolynomial σ R →ₐ[R] S₁
⊢ φ = aeval (⇑φ ∘ X)

Tactic:
ext i

Result:
case hf
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
φ : MvPolynomial σ R →ₐ[R] S₁
i : σ
⊢ φ (X i) = (aeval (⇑φ ∘ X)) (X i)

Proof state:
case hf
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
φ : MvPolynomial σ R →ₐ[R] S₁
i : σ
⊢ φ (X i) = (aeval (⇑φ ∘ X)) (X i)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
/-- Represent `log (1 - z)⁻¹` as an integral over the unit interval -/
lemma log_inv_eq_integral {z : ℂ} (hz : 1 - z ∈ slitPlane) :
    log (1 - z)⁻¹ = z * ∫ (t : ℝ) in (0 : ℝ)..1, (1 - t • z)⁻¹

Proof state:
z : ℂ
hz : 1 + -z ∈ slitPlane
⊢ log (1 + -z) = -z * ∫ (t : ℝ) in 0 ..1, (1 - t • z)⁻¹

Tactic:
convert log_eq_integral hz using 5

Result:
case h.e'_3.h.e'_6.h.e'_4.h.h.e'_3
z : ℂ
hz : 1 + -z ∈ slitPlane
x✝ : ℝ
⊢ 1 - x✝ • z = 1 + x✝ • -z

Proof state:
case h.e'_3.h.e'_6.h.e'_4.h.h.e'_3
z : ℂ
hz : 1 + -z ∈ slitPlane
x✝ : ℝ
⊢ 1 - x✝ • z = 1 + x✝ • -z

Tactic:
rw [sub_eq_add_neg, smul_neg]

Result:
no goals

Proof state:
z : ℂ
hz : 1 - z ∈ slitPlane
⊢ log (1 - z)⁻¹ = z * ∫ (t : ℝ) in 0 ..1, (1 - t • z)⁻¹

Tactic:
rw [sub_eq_add_neg 1 z] at hz ⊢

Result:
z : ℂ
hz : 1 + -z ∈ slitPlane
⊢ log (1 + -z)⁻¹ = z * ∫ (t : ℝ) in 0 ..1, (1 - t • z)⁻¹

Proof state:
z : ℂ
hz : 1 + -z ∈ slitPlane
⊢ log (1 + -z)⁻¹ = z * ∫ (t : ℝ) in 0 ..1, (1 - t • z)⁻¹

Tactic:
rw [log_inv _ <| slitPlane_arg_ne_pi hz, neg_eq_iff_eq_neg, ← neg_mul]

Result:
z : ℂ
hz : 1 + -z ∈ slitPlane
⊢ log (1 + -z) = -z * ∫ (t : ℝ) in 0 ..1, (1 - t • z)⁻¹