harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@[simp]
lemma basicOpen_eq_bot_of_isNilpotent (X : LocallyRingedSpace.{u}) (U : Opens X.carrier)
    (f : (X.presheaf.obj <| op U)) (hf : IsNilpotent f) :
    X.toRingedSpace.basicOpen f = ⊥

Proof state:
case intro.inr
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : f ^ n = 0
h : n > 0
⊢ X.toRingedSpace.basicOpen f = ⊥

Tactic:
rw [←  X.toRingedSpace.basicOpen_pow f n h, hn]

Result:
case intro.inr
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : f ^ n = 0
h : n > 0
⊢ X.toRingedSpace.basicOpen 0 = ⊥

Proof state:
case intro.inl
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : 1 = 0
h : n = 0
⊢ X.toRingedSpace.basicOpen f = ⊥

Tactic:
simp [eq_zero_of_zero_eq_one hn.symm f, basicOpen_zero]

Result:
no goals

Proof state:
case intro.inl
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : f ^ n = 0
h : n = 0
⊢ X.toRingedSpace.basicOpen f = ⊥

Tactic:
rw [h, pow_zero] at hn

Result:
case intro.inl
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : 1 = 0
h : n = 0
⊢ X.toRingedSpace.basicOpen f = ⊥

Proof state:
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsNilpotent f
⊢ X.toRingedSpace.basicOpen f = ⊥

Tactic:
obtain ⟨n, hn⟩ := hf

Result:
case intro
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : f ^ n = 0
⊢ X.toRingedSpace.basicOpen f = ⊥

Proof state:
case intro
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : f ^ n = 0
⊢ X.toRingedSpace.basicOpen f = ⊥

Tactic:
cases n.eq_zero_or_pos with
| inr h =>
  rw [←  X.toRingedSpace.basicOpen_pow f n h, hn]
  simp [basicOpen_zero]
| inl h =>
  rw [h, pow_zero] at hn
  simp [eq_zero_of_zero_eq_one hn.symm f, basicOpen_zero]

Result:
no goals

Proof state:
case intro.inr
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : f ^ n = 0
h : n > 0
⊢ X.toRingedSpace.basicOpen 0 = ⊥

Tactic:
simp [basicOpen_zero]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem cylinder_eq_cylinder_of_le_firstDiff (x y : ∀ n, E n) {n : ℕ} (hn : n ≤ firstDiff x y) :
    cylinder x n = cylinder y n

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff x y
⊢ cylinder x n = cylinder y n

Tactic:
rw [← mem_cylinder_iff_eq]

Result:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff x y
⊢ x ∈ cylinder y n

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff x y
i : ℕ
hi : i < n
⊢ x i = y i

Tactic:
exact apply_eq_of_lt_firstDiff (hi.trans_le hn)

Result:
no goals

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff x y
⊢ x ∈ cylinder y n

Tactic:
intro i hi

Result:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hn : n ≤ firstDiff x y
i : ℕ
hi : i < n
⊢ x i = y i
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
lemma prod_swap : (μ.prod ν).map measurable_swap.aemeasurable = ν.prod μ

Proof state:
case a
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ ↑((μ.prod ν).map ⋯) = ↑(ν.prod μ)

Tactic:
simp [Measure.prod_swap]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ (μ.prod ν).map ⋯ = ν.prod μ

Tactic:
apply Subtype.ext

Result:
case a
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ ↑((μ.prod ν).map ⋯) = ↑(ν.prod μ)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem extract_empty_of_size_le_start (as : Array α) {start stop : Nat} (h : as.size ≤ start) :
    as.extract start stop = #[]

Proof state:
α : Type u_1
as : Array α
start stop : Nat
h : as.size ≤ start
⊢ extract.loop as (min stop as.size - start) start #[] = #[]

Tactic:
rw [←Nat.sub_min_sub_right, Nat.sub_eq_zero_of_le h, Nat.min_zero, extract_loop_zero]

Result:
no goals

Proof state:
α : Type u_1
as : Array α
start stop : Nat
h : as.size ≤ start
⊢ as.extract start stop = #[]

Tactic:
simp only [extract, Nat.sub_eq, mkEmpty_eq]

Result:
α : Type u_1
as : Array α
start stop : Nat
h : as.size ≤ start
⊢ extract.loop as (min stop as.size - start) start #[] = #[]
-- Mathlib/Tactic/NormNum/BigOperators.lean
protected lemma Finset.prod_empty {β α : Type*} [CommSemiring β] (f : α → β) :
    IsNat (Finset.prod ∅ f) 1 :=
  ⟨by simp⟩

Proof state:
β : Type u_1
α : Type u_2
inst✝ : CommSemiring β
f : α → β
⊢ ∅.prod f = ↑1

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/AlgebraicClosure.lean
theorem extendScalars_of_isIntegral [Algebra.IsIntegral R S] : AlgebraicIndependent S x

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsIntegral R S
⊢ AlgebraicIndependent S x

Tactic:
nontriviality S

Result:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsIntegral R S
a✝ : Nontrivial S
⊢ AlgebraicIndependent S x

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsIntegral R S
a✝ : Nontrivial S
this : Nontrivial R
⊢ AlgebraicIndependent S x

Tactic:
exact hx.extendScalars S

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsIntegral R S
a✝ : Nontrivial S
⊢ AlgebraicIndependent S x

Tactic:
have := Module.nontrivial R S

Result:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : IsScalarTower R S A
inst✝¹ : NoZeroDivisors S
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsIntegral R S
a✝ : Nontrivial S
this : Nontrivial R
⊢ AlgebraicIndependent S x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (l H) :
    map g (pmap f l H) = pmap (fun a h => g (f a h)) l H

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
g : β → γ
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ l → p a
⊢ map g (pmap f l H) = pmap (fun a h => g (f a h)) l H

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
g : β → γ
f : (a : α) → p a → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ map g (pmap f { toList := toList✝ } H) = pmap (fun a h => g (f a h)) { toList := toList✝ } H

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
g : β → γ
f : (a : α) → p a → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ map g (pmap f { toList := toList✝ } H) = pmap (fun a h => g (f a h)) { toList := toList✝ } H

Tactic:
simp [List.map_pmap]

Result:
no goals
-- Mathlib/Algebra/Star/StarAlgHom.lean
theorem snd_prod (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : (snd R B C).comp (prod f g) = g

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
⊢ (snd R B C).comp (f.prod g) = g

Tactic:
ext

Result:
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x✝ : A
⊢ ((snd R B C).comp (f.prod g)) x✝ = g x✝

Proof state:
case h
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Star A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Star B
inst✝² : Semiring C
inst✝¹ : Algebra R C
inst✝ : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
x✝ : A
⊢ ((snd R B C).comp (f.prod g)) x✝ = g x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem mul_divByMonic_cancel_left (p : R[X]) {q : R[X]} (hmo : q.Monic) :
    q * p /ₘ q = p

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ degree 0 < q.degree

Tactic:
rw [degree_zero]

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ ⊥ < q.degree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ 0 + q * p = q * p

Tactic:
rw [zero_add]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ q * p /ₘ q = p

Tactic:
refine (div_modByMonic_unique _ 0 hmo ⟨by rw [zero_add], ?_⟩).1

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ degree 0 < q.degree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ ⊥ < q.degree

Tactic:
exact Ne.bot_lt fun h => hmo.ne_zero (degree_eq_bot.1 h)

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
⊢ q * p /ₘ q = p

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hmo : q.Monic
a✝ : Nontrivial R
⊢ q * p /ₘ q = p
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem measurableSet_range (hf : MeasurableEmbedding f) : MeasurableSet (range f)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
⊢ MeasurableSet (range f)

Tactic:
rw [← image_univ]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
⊢ MeasurableSet (f '' univ)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
⊢ MeasurableSet (f '' univ)

Tactic:
exact hf.measurableSet_image' MeasurableSet.univ

Result:
no goals
-- Mathlib/RingTheory/WittVector/Compare.lean
theorem toPadicInt_comp_fromPadicInt : (toPadicInt p).comp (fromPadicInt p) = RingHom.id ℤ_[p]

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (toZModPow p n).comp (fromPadicInt p) = (PadicInt.toZModPow n).comp (RingHom.id ℤ_[p])

Tactic:
simp only [fromPadicInt, toZModPow, RingHom.comp_id]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate n)).comp
      (lift (fun k => (zmodEquivTrunc p k).toRingHom.comp (PadicInt.toZModPow k)) ⋯) =
    PadicInt.toZModPow n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (PadicInt.toZModPow n).comp ((toPadicInt p).comp (fromPadicInt p)) = (PadicInt.toZModPow n).comp (RingHom.id ℤ_[p])

Tactic:
rw [← RingHom.comp_assoc, toPadicInt, PadicInt.lift_spec]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (toZModPow p n).comp (fromPadicInt p) = (PadicInt.toZModPow n).comp (RingHom.id ℤ_[p])

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate n)).comp
      (lift (fun k => (zmodEquivTrunc p k).toRingHom.comp (PadicInt.toZModPow k)) ⋯) =
    PadicInt.toZModPow n

Tactic:
rw [RingHom.comp_assoc, truncate_comp_lift, ← RingHom.comp_assoc]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((zmodEquivTrunc p n).symm.toRingHom.comp (zmodEquivTrunc p n).toRingHom).comp (PadicInt.toZModPow n) =
    PadicInt.toZModPow n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (toPadicInt p).comp (fromPadicInt p) = RingHom.id ℤ_[p]

Tactic:
rw [← PadicInt.toZModPow_eq_iff_ext]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (n : ℕ),
    (PadicInt.toZModPow n).comp ((toPadicInt p).comp (fromPadicInt p)) = (PadicInt.toZModPow n).comp (RingHom.id ℤ_[p])

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((zmodEquivTrunc p n).symm.toRingHom.comp (zmodEquivTrunc p n).toRingHom).comp (PadicInt.toZModPow n) =
    PadicInt.toZModPow n

Tactic:
simp only [RingEquiv.symm_toRingHom_comp_toRingHom, RingHom.id_comp]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (n : ℕ),
    (PadicInt.toZModPow n).comp ((toPadicInt p).comp (fromPadicInt p)) = (PadicInt.toZModPow n).comp (RingHom.id ℤ_[p])

Tactic:
intro n

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (PadicInt.toZModPow n).comp ((toPadicInt p).comp (fromPadicInt p)) = (PadicInt.toZModPow n).comp (RingHom.id ℤ_[p])
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem inv_eq_one_divp (u : αˣ) : ↑u⁻¹ = 1 /ₚ u

Proof state:
α : Type u
inst✝ : Monoid α
u : αˣ
⊢ ↑u⁻¹ = 1 /ₚ u

Tactic:
rw [one_divp]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem splitLower_eq_bot {i x} : I.splitLower i x = ⊥ ↔ x ≤ I.lower i

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitLower i x = ⊥ ↔ x ≤ I.lower i

Tactic:
rw [splitLower, mk'_eq_bot, exists_update_iff I.upper fun j y => y ≤ I.lower j]

Result:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (x ⊓ I.upper i ≤ I.lower i ∨ ∃ x, x ≠ i ∧ I.upper x ≤ I.lower x) ↔ x ≤ I.lower i

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (x ⊓ I.upper i ≤ I.lower i ∨ ∃ x, x ≠ i ∧ I.upper x ≤ I.lower x) ↔ x ≤ I.lower i

Tactic:
simp [(I.lower_lt_upper _).not_le]

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitLower i x = ⊥ ↔ x ≤ I.lower i

Tactic:
classical
rw [splitLower, mk'_eq_bot, exists_update_iff I.upper fun j y => y ≤ I.lower j]
simp [(I.lower_lt_upper _).not_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem constModifyKey_eq_modifyKey {β : Type v} [BEq α] [LawfulBEq α] {k : α} {f : β → β}
    {l : List ((_ : α) × β)} :
    Const.modifyKey k f l = modifyKey k f l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β → β
l : List ((_ : α) × β)
⊢ Const.modifyKey k f l = modifyKey k f l

Tactic:
rw [modifyKey, Const.modifyKey, getValue?_eq_getValueCast?]

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β → β
l : List ((_ : α) × β)
⊢ (match getValueCast? k l with
    | none => l
    | some v => replaceEntry k (f v) l) =
    match getValueCast? k l with
    | none => l
    | some v => replaceEntry k (f v) l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β → β
l : List ((_ : α) × β)
⊢ (match getValueCast? k l with
    | none => l
    | some v => replaceEntry k (f v) l) =
    match getValueCast? k l with
    | none => l
    | some v => replaceEntry k (f v) l

Tactic:
cases getValueCast? k l <;> rfl

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem factors_subsingleton [Subsingleton α] {a : Associates α} : a.factors = ⊤

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton α
a : Associates α
this : Subsingleton (Associates α)
⊢ a.factors = ⊤

Tactic:
convert factors_zero

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton α
a : Associates α
⊢ a.factors = ⊤

Tactic:
have : Subsingleton (Associates α) := inferInstance

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Subsingleton α
a : Associates α
this : Subsingleton (Associates α)
⊢ a.factors = ⊤
-- Mathlib/Analysis/Convex/Star.lean
theorem starConvex_singleton (x : E) : StarConvex 𝕜 x {x}

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
y : E
a b : 𝕜
a✝¹ : 0 ≤ a
a✝ : 0 ≤ b
hab : a + b = 1
⊢ a • y + b • y ∈ {y}

Tactic:
exact Convex.combo_self hab _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
⊢ StarConvex 𝕜 x {x}

Tactic:
rintro y (rfl : y = x) a b _ _ hab

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
y : E
a b : 𝕜
a✝¹ : 0 ≤ a
a✝ : 0 ≤ b
hab : a + b = 1
⊢ a • y + b • y ∈ {y}
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigOWith.isBigO (h : IsBigOWith c l f g) : f =O[l] g

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
h : IsBigOWith c l f g
⊢ ∃ c, IsBigOWith c l f g

Tactic:
exact ⟨c, h⟩

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
h : IsBigOWith c l f g
⊢ f =O[l] g

Tactic:
rw [IsBigO_def]

Result:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
h : IsBigOWith c l f g
⊢ ∃ c, IsBigOWith c l f g
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_le_iff_one_le_mul' : a⁻¹ ≤ b ↔ 1 ≤ a * b :=
  (mul_le_mul_iff_left a).symm.trans <| by rw [mul_inv_cancel]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b : α
⊢ a * a⁻¹ ≤ a * b ↔ 1 ≤ a * b

Tactic:
rw [mul_inv_cancel]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWith_comm_of_comm (f : α → α → β) (comm : ∀ x y : α, f x y = f y x) (l l' : Array α) :
    zipWith f l l' = zipWith f l' l

Proof state:
α : Type u_1
β : Type u_2
f : α → α → β
comm : ∀ (x y : α), f x y = f y x
l l' : Array α
⊢ zipWith (fun b a => f a b) l' l = zipWith f l' l

Tactic:
simp only [comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → α → β
comm : ∀ (x y : α), f x y = f y x
l l' : Array α
⊢ zipWith f l l' = zipWith f l' l

Tactic:
rw [zipWith_comm]

Result:
α : Type u_1
β : Type u_2
f : α → α → β
comm : ∀ (x y : α), f x y = f y x
l l' : Array α
⊢ zipWith (fun b a => f a b) l' l = zipWith f l' l
-- Mathlib/NumberTheory/Divisors.lean
theorem snd_mem_divisors_of_mem_antidiagonal {x : ℕ × ℕ} (h : x ∈ divisorsAntidiagonal n) :
    x.snd ∈ divisors n

Proof state:
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n ∧ n ≠ 0
⊢ x.2 ∈ n.divisors

Tactic:
simp [Dvd.intro_left _ h.1, h.2]

Result:
no goals

Proof state:
n : ℕ
x : ℕ × ℕ
h : x ∈ n.divisorsAntidiagonal
⊢ x.2 ∈ n.divisors

Tactic:
rw [mem_divisorsAntidiagonal] at h

Result:
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n ∧ n ≠ 0
⊢ x.2 ∈ n.divisors
-- Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean
theorem exp_eq (q : Quaternion ℝ) :
    exp ℝ q = exp ℝ q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)

Proof state:
q : ℍ
⊢ Commute (↑q.re) q.im

Tactic:
exact Algebra.commutes q.re (_ : ℍ[ℝ])

Result:
no goals

Proof state:
q : ℍ
⊢ exp ℝ q = exp ℝ q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)

Tactic:
rw [← exp_of_re_eq_zero q.im q.im_re, ← coe_mul_eq_smul, ← exp_coe, ← exp_add_of_commute,
  re_add_im]

Result:
q : ℍ
⊢ Commute (↑q.re) q.im
-- Mathlib/Data/Erased.lean
theorem mk_out {α} : ∀ a : Erased α, mk (out a) = a
  | ⟨s, h⟩ => by simp only [mk]; congr; exact Classical.choose_spec h

Proof state:
case e_val
α : Sort u_1
s : α → Prop
h : ∃ a, (fun x => a = x) = s
⊢ (fun b => out ⟨s, h⟩ = b) = s

Tactic:
exact Classical.choose_spec h

Result:
no goals

Proof state:
α : Sort u_1
s : α → Prop
h : ∃ a, (fun x => a = x) = s
⊢ ⟨fun b => out ⟨s, h⟩ = b, ⋯⟩ = ⟨s, h⟩

Tactic:
congr

Result:
case e_val
α : Sort u_1
s : α → Prop
h : ∃ a, (fun x => a = x) = s
⊢ (fun b => out ⟨s, h⟩ = b) = s

Proof state:
α : Sort u_1
s : α → Prop
h : ∃ a, (fun x => a = x) = s
⊢ mk (out ⟨s, h⟩) = ⟨s, h⟩

Tactic:
simp only [mk]

Result:
α : Sort u_1
s : α → Prop
h : ∃ a, (fun x => a = x) = s
⊢ ⟨fun b => out ⟨s, h⟩ = b, ⋯⟩ = ⟨s, h⟩
-- Mathlib/Algebra/Group/Subsemigroup/Operations.lean
theorem bot_prod_bot : (⊥ : Subsemigroup M).prod (⊥ : Subsemigroup N) = ⊥ :=
  SetLike.coe_injective <| by simp [coe_prod]

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
⊢ ↑(⊥.prod ⊥) = ↑⊥

Tactic:
simp [coe_prod]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_pos {x : ℝ} : 0 < arccos x ↔ x < 1

Proof state:
x : ℝ
⊢ 0 < arccos x ↔ x < 1

Tactic:
simp [arccos]

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma yonedaEquiv_symm_map {X Y : Cᵒᵖ} (f : X ⟶ Y) {F : Cᵒᵖ ⥤ Type v₁} (t : F.obj X) :
    yonedaEquiv.symm (F.map f t) = yoneda.map f.unop ≫ yonedaEquiv.symm t

Proof state:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type v₁
u : yoneda.obj (unop X) ⟶ F
⊢ yonedaEquiv.symm (F.map f (yonedaEquiv u)) = yoneda.map f.unop ≫ yonedaEquiv.symm (yonedaEquiv u)

Tactic:
rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type v₁
t : F.obj X
⊢ yonedaEquiv.symm (F.map f t) = yoneda.map f.unop ≫ yonedaEquiv.symm t

Tactic:
obtain ⟨u, rfl⟩ := yonedaEquiv.surjective t

Result:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type v₁
u : yoneda.obj (unop X) ⟶ F
⊢ yonedaEquiv.symm (F.map f (yonedaEquiv u)) = yoneda.map f.unop ≫ yonedaEquiv.symm (yonedaEquiv u)
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem self (hp : 1 < p) : padicValRat p p = 1

Proof state:
p : ℕ
hp : 1 < p
⊢ padicValRat p ↑p = 1

Tactic:
simp [hp]

Result:
no goals
-- Mathlib/Algebra/Homology/SingleHomology.lean
@[reassoc (attr := simp)]
lemma homologyπ_singleObjHomologySelfIso_hom :
    ((single C c j).obj A).homologyπ j ≫ (singleObjHomologySelfIso _ _ _).hom =
      (singleObjCyclesSelfIso _ _ _).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ ((single C c j).obj A).homologyπ j ≫ (singleObjHomologySelfIso c j A).hom = (singleObjCyclesSelfIso c j A).hom

Tactic:
simp [singleObjCyclesSelfIso, singleObjHomologySelfIso]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueD_modifyKey [EquivBEq α] {k k' : α} {fallback : β} {f : β → β}
    (l : List ((_ : α) × β)) (hl : DistinctKeys l) :
    getValueD k' (modifyKey k f l) fallback =
      if k == k' then
        getValue? k l |>.map f |>.getD fallback
      else
        getValueD k' l fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
fallback : β
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getValueD k' (modifyKey k f l) fallback =
    if (k == k') = true then (Option.map f (getValue? k l)).getD fallback else getValueD k' l fallback

Tactic:
simp [modifyKey_eq_alterKey, getValueD_alterKey, hl]

Result:
no goals