harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/PSeries.lean
theorem sum_condensed_le' (hf : ∀ ⦃m n⦄, 1 < m → m ≤ n → f n ≤ f m) (n : ℕ) :
    (∑ k ∈ range n, 2 ^ k • f (2 ^ (k + 1))) ≤ ∑ k ∈ Ico 2 (2 ^ n + 1), f k

Proof state:
case h.e'_3.a
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n x✝ : ℕ
a✝ : x✝ ∈ range n
⊢ 2 ^ x✝ • f (2 ^ (x✝ + 1)) = (2 ^ (x✝ + 1) - 2 ^ x✝) • f (2 ^ (x✝ + 1))

Tactic:
simp [pow_succ, mul_two, two_mul]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k ∈ range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k ∈ Ico 2 (2 ^ n + 1), f k

Tactic:
convert sum_schlomilch_le' hf (fun n => pow_pos zero_lt_two n)
  (fun m n hm => pow_right_mono₀ one_le_two hm) n using 2

Result:
case h.e'_3.a
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n x✝ : ℕ
a✝ : x✝ ∈ range n
⊢ 2 ^ x✝ • f (2 ^ (x✝ + 1)) = (2 ^ (x✝ + 1) - 2 ^ x✝) • f (2 ^ (x✝ + 1))
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
theorem tendsto_sub_mul_tsum_nat_rpow :
    Tendsto (fun s : ℝ ↦ (s - 1) * ∑' (n : ℕ), 1 / (n : ℝ) ^ s) (𝓝[>] 1) (𝓝 1)

Proof state:
⊢ Tendsto (fun x => ↑((x - 1) * ∑' (n : ℕ), 1 / ↑n ^ x)) (𝓝[>] 1) (𝓝 1)

Tactic:
have : Tendsto (fun s : ℝ ↦ (s : ℂ)) (𝓝[>] 1) (𝓝[{s | 1 < re s}] 1) :=
  continuous_ofReal.continuousWithinAt.tendsto_nhdsWithin (fun _ _ ↦ by aesop)

Result:
this : Tendsto (fun s => ↑s) (𝓝[>] 1) (𝓝[{s | 1 < s.re}] 1)
⊢ Tendsto (fun x => ↑((x - 1) * ∑' (n : ℕ), 1 / ↑n ^ x)) (𝓝[>] 1) (𝓝 1)

Proof state:
this : Tendsto (fun s => ↑s) (𝓝[>] 1) (𝓝[{s | 1 < s.re}] 1)
⊢ Tendsto (fun x => ↑((x - 1) * ∑' (n : ℕ), 1 / ↑n ^ x)) (𝓝[>] 1) (𝓝 1)

Tactic:
apply (tendsto_sub_mul_tsum_nat_cpow.comp this).congr fun s ↦ ?_

Result:
this : Tendsto (fun s => ↑s) (𝓝[>] 1) (𝓝[{s | 1 < s.re}] 1)
s : ℝ
⊢ ((fun s => (s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s) ∘ fun s => ↑s) s = ↑((s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s)

Proof state:
⊢ Tendsto (fun s => (s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s) (𝓝[>] 1) (𝓝 1)

Tactic:
rw [← tendsto_ofReal_iff, ofReal_one]

Result:
⊢ Tendsto (fun x => ↑((x - 1) * ∑' (n : ℕ), 1 / ↑n ^ x)) (𝓝[>] 1) (𝓝 1)

Proof state:
x✝¹ : ℝ
x✝ : x✝¹ ∈ Ioi 1
⊢ ↑x✝¹ ∈ {s | 1 < s.re}

Tactic:
aesop

Result:
no goals

Proof state:
this : Tendsto (fun s => ↑s) (𝓝[>] 1) (𝓝[{s | 1 < s.re}] 1)
s : ℝ
⊢ ((fun s => (s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s) ∘ fun s => ↑s) s = ↑((s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s)

Tactic:
simp only [one_div, Function.comp_apply, ofReal_mul, ofReal_sub, ofReal_one, ofReal_tsum,
  ofReal_inv, ofReal_cpow (Nat.cast_nonneg _), ofReal_natCast]

Result:
no goals
-- Mathlib/Order/RelClasses.lean
lemma subset_of_subset_of_eq (hab : a ⊆ b) (hbc : b = c) : a ⊆ c

Proof state:
α : Type u
inst✝ : HasSubset α
a b c : α
hab : a ⊆ b
hbc : b = c
⊢ a ⊆ c

Tactic:
rwa [← hbc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_singleton {a : α} : mapIdx f #[a] = #[f 0 a]

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
a : α
⊢ mapIdx f #[a] = #[f 0 a]

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Int/Init.lean
protected lemma lt_or_le (a b : ℤ) : a < b ∨ b ≤ a

Proof state:
a b : ℤ
⊢ a < b ∨ ¬a < b

Tactic:
exact Decidable.em _

Result:
no goals

Proof state:
a b : ℤ
⊢ a < b ∨ b ≤ a

Tactic:
rw [← Int.not_lt]

Result:
a b : ℤ
⊢ a < b ∨ ¬a < b
-- Mathlib/Data/Fintype/Card.lean
theorem surjective_iff_bijective {f : α → α} : Surjective f ↔ Bijective f

Proof state:
α : Type u_1
inst✝ : Finite α
f : α → α
⊢ Surjective f ↔ Bijective f

Tactic:
simp [Bijective, injective_iff_surjective]

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem totient_eq_one_iff : ∀ {n : ℕ}, n.totient = 1 ↔ n = 1 ∨ n = 2
  | 0 => by simp
  | 1 => by simp
  | 2 => by simp
  | n + 3 => by
    have : 3 ≤ n + 3 := le_add_self
    simp only [succ_succ_ne_one, false_or]
    exact ⟨fun h => not_even_one.elim <| h ▸ totient_even this, by rintro ⟨⟩⟩

Proof state:
n : ℕ
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2

Tactic:
have : 3 ≤ n + 3 := le_add_self

Result:
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2

Proof state:
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 2

Tactic:
exact ⟨fun h => not_even_one.elim <| h ▸ totient_even this, by rintro ⟨⟩⟩

Result:
no goals

Proof state:
n : ℕ
this : 3 ≤ n + 3
⊢ n + 3 = 2 → φ (n + 3) = 1

Tactic:
rintro ⟨⟩

Result:
no goals

Proof state:
⊢ φ 1 = 1 ↔ 1 = 1 ∨ 1 = 2

Tactic:
simp

Result:
no goals

Proof state:
⊢ φ 0 = 1 ↔ 0 = 1 ∨ 0 = 2

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 1 ∨ n + 3 = 2

Tactic:
simp only [succ_succ_ne_one, false_or]

Result:
n : ℕ
this : 3 ≤ n + 3
⊢ φ (n + 3) = 1 ↔ n + 3 = 2

Proof state:
⊢ φ 2 = 1 ↔ 2 = 1 ∨ 2 = 2

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem cpow_sub {x : ℂ} (y z : ℂ) (hx : x ≠ 0) : x ^ (y - z) = x ^ y / x ^ z

Proof state:
x y z : ℂ
hx : x ≠ 0
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
rw [sub_eq_add_neg, cpow_add _ _ hx, cpow_neg, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_fiberwise_of_maps_to' {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : κ → α) :
    ∏ j ∈ t, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s, f (g i)

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝¹ : CommMonoid α
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : κ → α
⊢ ∏ j ∈ t, ∏ i ∈ filter (fun i => g i = j) s, f j = ∏ i ∈ s, f (g i)

Tactic:
calc
  _ = ∏ j ∈ t, ∏ i ∈ s with g i = j, f (g i) :=
      prod_congr rfl fun y _ ↦ prod_congr rfl fun x hx ↦ by rw [(mem_filter.1 hx).2]
  _ = _ := prod_fiberwise_of_maps_to h _

Result:
no goals

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝¹ : CommMonoid α
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : κ → α
y : κ
x✝ : y ∈ t
x : ι
hx : x ∈ filter (fun i => g i = y) s
⊢ f y = f (g x)

Tactic:
rw [(mem_filter.1 hx).2]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem le_of_lt_add_one (h : x < y + 1) : x ≤ y

Proof state:
α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < y + 1
⊢ x ≤ y

Tactic:
rw [← succ_eq_add_one] at h

Result:
α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < succ y
⊢ x ≤ y

Proof state:
α : Type u_1
x y : α
inst✝³ : LinearOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
h : x < succ y
⊢ x ≤ y

Tactic:
exact le_of_lt_succ h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
lemma logTaylor_at_zero (n : ℕ) : logTaylor n 0 = 0

Proof state:
case succ
n : ℕ
ih : logTaylor n 0 = 0
⊢ logTaylor (n + 1) 0 = 0

Tactic:
simpa [logTaylor_succ, ih] using ne_or_eq n 0

Result:
no goals

Proof state:
n : ℕ
⊢ logTaylor n 0 = 0

Tactic:
induction n with
| zero => simp [logTaylor_zero]
| succ n ih => simpa [logTaylor_succ, ih] using ne_or_eq n 0

Result:
no goals

Proof state:
case zero

⊢ logTaylor 0 0 = 0

Tactic:
simp [logTaylor_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
lemma T_S_rel : S • S • S • T • S • T • S = T⁻¹

Proof state:
case a
i j : Fin 2
⊢ ↑(S • S • S • T • S • T • S) i j = ↑T⁻¹ i j

Tactic:
fin_cases i <;> fin_cases j <;> rfl

Result:
no goals

Proof state:
⊢ S • S • S • T • S • T • S = T⁻¹

Tactic:
ext i j

Result:
case a
i j : Fin 2
⊢ ↑(S • S • S • T • S • T • S) i j = ↑T⁻¹ i j
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₆_of_isCharTwoJNeZeroNF : W.c₆ = -W.b₂ ^ 3 - 864 * W.a₆

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ -W.b₂ ^ 3 + 36 * W.b₂ * 0 - 216 * (4 * W.a₆) = -W.b₂ ^ 3 - 864 * W.a₆

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.c₆ = -W.b₂ ^ 3 - 864 * W.a₆

Tactic:
rw [c₆, b₄_of_isCharTwoJNeZeroNF, b₆_of_isCharTwoJNeZeroNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ -W.b₂ ^ 3 + 36 * W.b₂ * 0 - 216 * (4 * W.a₆) = -W.b₂ ^ 3 - 864 * W.a₆
-- Mathlib/MeasureTheory/Function/Jacobian.lean
lemma _root_.MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul
    (hs : MeasurableSet s) (f : E ≃ᵐ E)
    {g : E → ℝ} (hg : ∀ᵐ x ∂μ, x ∈ f '' s → 0 ≤ g x) (hg_int : IntegrableOn g (f '' s) μ)
    (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :
    (μ.withDensity (fun x ↦ ENNReal.ofReal (g x))).map f.symm s
      = ENNReal.ofReal (∫ x in s, |(f' x).det| * g (f x) ∂μ)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
f : E ≃ᵐ E
g : E → ℝ
hg : ∀ᵐ (x : E) ∂μ, x ∈ ⇑f '' s → 0 ≤ g x
hg_int : IntegrableOn g (⇑f '' s) μ
hf' : ∀ x ∈ s, HasFDerivWithinAt (⇑f) (f' x) s x
⊢ (Measure.map (⇑f.symm) (μ.withDensity fun x => ENNReal.ofReal (g x))) s =
    ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)

Tactic:
rw [MeasurableEquiv.map_symm,
  MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul μ hs
    f.measurableEmbedding hg hg_int hf']

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean
lemma IsPushout.of_iso {sq₁ sq₂ : Square C} (h : sq₁.IsPushout)
    (e : sq₁ ≅ sq₂) : sq₂.IsPushout

Proof state:
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₂.IsPushout

Tactic:
refine CategoryTheory.IsPushout.of_iso h
  (evaluation₁.mapIso e) (evaluation₂.mapIso e)
  (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_

Result:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₁₂ ≫ (evaluation₂.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₂

case refine_2
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₁₃ ≫ (evaluation₃.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₃

case refine_3
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₂₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₂.mapIso e).hom ≫ sq₂.f₂₄

case refine_4
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₃₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₃.mapIso e).hom ≫ sq₂.f₃₄

Proof state:
case refine_4
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₃₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₃.mapIso e).hom ≫ sq₂.f₃₄

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₁₂ ≫ (evaluation₂.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₂

case refine_2
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₁₃ ≫ (evaluation₃.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₃

case refine_3
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₂₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₂.mapIso e).hom ≫ sq₂.f₂₄

case refine_4
C : Type u
inst✝ : Category.{v, u} C
sq₁ sq₂ : Square C
h : sq₁.IsPushout
e : sq₁ ≅ sq₂
⊢ sq₁.f₃₄ ≫ (evaluation₄.mapIso e).hom = (evaluation₃.mapIso e).hom ≫ sq₂.f₃₄

Tactic:
all_goals simp

Result:
no goals
-- Mathlib/Algebra/Order/Ring/WithTop.lean
lemma mul_coe_eq_bind {b : α} (hb : b ≠ 0) : ∀ a, (a * b : WithTop α) = a.bind fun a ↦ ↑(a * b)
  | ⊤ => by simp [top_mul, hb]; rfl
  | (a : α) => rfl

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊤ * ↑b = Option.bind ⊤ fun a => Option.some (a * b)

Tactic:
simp [top_mul, hb]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊤ = Option.bind ⊤ fun a => Option.some (a * b)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊤ = Option.bind ⊤ fun a => Option.some (a * b)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma snd_opProdIsoCoprod_hom : prod.snd.op ≫ (opProdIsoCoprod A B).hom = coprod.inr

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ prod.snd.op ≫ (opProdIsoCoprod A B).hom = coprod.inr

Tactic:
rw [opProdIsoCoprod, ← op_comp, prod.lift_snd, Quiver.Hom.op_unop]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem equivalence_join_red : Equivalence (Join (@Red α)) :=
  equivalence_join_reflTransGen fun _ b c hab hac =>
    match b, c, Red.Step.diamond hab hac rfl with
    | b, _, Or.inl rfl => ⟨b, by rfl, by rfl⟩
    | _, _, Or.inr ⟨d, hbd, hcd⟩ => ⟨d, ReflGen.single hbd, ReflTransGen.single hcd⟩

Proof state:
α : Type u
x✝ b✝ c b : List (α × Bool)
hab hac : Red.Step x✝ b
⊢ ReflGen Red.Step b b

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
x✝ b✝ c b : List (α × Bool)
hab hac : Red.Step x✝ b
⊢ ReflTransGen Red.Step b b

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Prod.lean
theorem swap_inj {p q : α × β} : swap p = swap q ↔ p = q

Proof state:
case mk
α : Type u_1
β : Type u_2
q : α × β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝).swap = q.swap ↔ (fst✝, snd✝) = q

Tactic:
cases q

Result:
case mk.mk
α : Type u_1
β : Type u_2
fst✝¹ : α
snd✝¹ : β
fst✝ : α
snd✝ : β
⊢ (fst✝¹, snd✝¹).swap = (fst✝, snd✝).swap ↔ (fst✝¹, snd✝¹) = (fst✝, snd✝)

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
fst✝¹ : α
snd✝¹ : β
fst✝ : α
snd✝ : β
⊢ (fst✝¹, snd✝¹).swap = (fst✝, snd✝).swap ↔ (fst✝¹, snd✝¹) = (fst✝, snd✝)

Tactic:
simp [and_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p q : α × β
⊢ p.swap = q.swap ↔ p = q

Tactic:
cases p

Result:
case mk
α : Type u_1
β : Type u_2
q : α × β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝).swap = q.swap ↔ (fst✝, snd✝) = q
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem type_eq_one_of_unique (r) [IsWellOrder α r] [Nonempty α] [Subsingleton α] : type r = 1

Proof state:
α : Type u
r : α → α → Prop
inst✝² : IsWellOrder α r
inst✝¹ : Nonempty α
inst✝ : Subsingleton α
⊢ type r = 1

Tactic:
cases nonempty_unique α

Result:
case intro
α : Type u
r : α → α → Prop
inst✝² : IsWellOrder α r
inst✝¹ : Nonempty α
inst✝ : Subsingleton α
val✝ : Unique α
⊢ type r = 1

Proof state:
case intro
α : Type u
r : α → α → Prop
inst✝² : IsWellOrder α r
inst✝¹ : Nonempty α
inst✝ : Subsingleton α
val✝ : Unique α
⊢ type r = 1

Tactic:
exact (RelIso.ofUniqueOfIrrefl r _).ordinal_type_eq

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem multichoose_zero_succ (k : ℕ) : multichoose 0 (k + 1) = 0

Proof state:
k : ℕ
⊢ multichoose 0 (k + 1) = 0

Tactic:
simp [multichoose]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_X_pow_add_C {n : ℕ} (hn : 0 < n) {r : R} :
    (X ^ n + C r).leadingCoeff = 1

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (X ^ n + C r).leadingCoeff = 1

Tactic:
rw [leadingCoeff, natDegree_X_pow_add_C, coeff_add, coeff_X_pow_self, coeff_C,
  if_neg (pos_iff_ne_zero.mp hn), add_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
⊢ (X ^ n + C r).leadingCoeff = 1

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (X ^ n + C r).leadingCoeff = 1
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem cos_oangle_left_mul_dist_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P}
    (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) : Real.Angle.cos (∡ p₃ p₁ p₂) * dist p₁ p₃ = dist 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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).sign = 1

Tactic:
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).cos * dist p₁ p₃ = dist p₁ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.cos_coe, dist_comm p₁ p₃,
  cos_angle_mul_dist_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).cos * dist p₁ p₃ = dist p₁ p₂

Tactic:
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).cos * dist p₁ p₃ = dist p₁ p₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_map (g : β → γ) (f : α → β) (l : List α) :
  map g (map f l) = map (g ∘ f) l

Proof state:
β : Type u_1
γ : Type u_2
α : Type u_3
g : β → γ
f : α → β
l : List α
⊢ map g (map f l) = map (g ∘ f) l

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem subset_union_elim {s : Finset α} {t₁ t₂ : Set α} (h : ↑s ⊆ t₁ ∪ t₂) :
    ∃ s₁ s₂ : Finset α, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁

Proof state:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ ↑(filter (fun x => x ∉ t₁) s) → x ∈ t₂ \ t₁

Tactic:
simp only [not_not, coe_filter, Set.mem_setOf_eq, Set.mem_diff, and_imp]

Result:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ s → x ∉ t₁ → x ∈ t₂ ∧ x ∉ t₁

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x => x ∈ t₁) s) ⊆ t₁

Tactic:
intro x

Result:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ ↑(filter (fun x => x ∈ t₁) s) → x ∈ t₁

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ filter (fun x => x ∈ t₁) s ∪ filter (fun x => x ∉ t₁) s = s

Tactic:
simp [filter_union_right, em]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ ↑(filter (fun x => x ∈ t₁) s) → x ∈ t₁

Tactic:
simp

Result:
no goals

Proof state:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x => x ∉ t₁) s) ⊆ t₂ \ t₁

Tactic:
intro x

Result:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ ↑(filter (fun x => x ∉ t₁) s) → x ∈ t₂ \ t₁

Proof state:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ s → x ∉ t₁ → x ∈ t₂ ∧ x ∉ t₁

Tactic:
intro hx hx₂

Result:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
hx : x ∈ s
hx₂ : x ∉ t₁
⊢ x ∈ t₂ ∧ x ∉ t₁

Proof state:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
hx : x ∈ s
hx₂ : x ∉ t₁
⊢ x ∈ t₂ ∧ x ∉ t₁

Tactic:
exact ⟨Or.resolve_left (h hx) hx₂, hx₂⟩

Result:
no goals
-- Mathlib/Data/List/TakeDrop.lean
@[simp] lemma take_eq_self_iff (x : List α) {n : ℕ} : x.take n = x ↔ x.length ≤ n :=
  ⟨fun h ↦ by rw [← h]; simp; omega, take_of_length_le⟩

Proof state:
α : Type u
x : List α
n : ℕ
h : take n x = x
⊢ x.length ≤ n

Tactic:
rw [← h]

Result:
α : Type u
x : List α
n : ℕ
h : take n x = x
⊢ (take n x).length ≤ n

Proof state:
α : Type u
x : List α
n : ℕ
h : take n x = x
⊢ (take n x).length ≤ n

Tactic:
simp

Result:
α : Type u
x : List α
n : ℕ
h : take n x = x
⊢ min n x.length ≤ n

Proof state:
α : Type u
x : List α
n : ℕ
h : take n x = x
⊢ min n x.length ≤ n

Tactic:
omega

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem toPMF_dirac [Countable α] [h : MeasurableSingletonClass α] :
    (Measure.dirac a).toPMF = pure a

Proof state:
α : Type u_1
a : α
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
h : MeasurableSingletonClass α
⊢ (Measure.dirac a).toPMF = pure a

Tactic:
rw [toPMF_eq_iff_toMeasure_eq, toMeasure_pure]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Exact.lean
theorem Abelian.tfae_mono {X Y : C} (f : X ⟶ Y) (Z : C) :
    TFAE [Mono f, kernel.ι f = 0, (ShortComplex.mk (0 : Z ⟶ X) f zero_comp).Exact]

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
⊢ [Mono f, kernel.ι f = 0, (ShortComplex.mk 0 f ⋯).Exact].TFAE

Tactic:
tfae_have 2 → 1 := mono_of_kernel_ι_eq_zero _

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
⊢ [Mono f, kernel.ι f = 0, (ShortComplex.mk 0 f ⋯).Exact].TFAE

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
x✝ : Mono f
⊢ kernel.ι f = 0

Tactic:
rw [← cancel_mono f, kernel.condition, zero_comp]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
tfae_1_to_2 : Mono f → kernel.ι f = 0
⊢ (ShortComplex.mk 0 f ⋯).f = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
tfae_1_to_2 : Mono f → kernel.ι f = 0
tfae_3_iff_1 : (ShortComplex.mk 0 f ⋯).Exact ↔ Mono f
⊢ [Mono f, kernel.ι f = 0, (ShortComplex.mk 0 f ⋯).Exact].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
tfae_1_to_2 : Mono f → kernel.ι f = 0
⊢ [Mono f, kernel.ι f = 0, (ShortComplex.mk 0 f ⋯).Exact].TFAE

Tactic:
tfae_have 3 ↔ 1 := ShortComplex.exact_iff_mono _ (by simp)

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
tfae_1_to_2 : Mono f → kernel.ι f = 0
tfae_3_iff_1 : (ShortComplex.mk 0 f ⋯).Exact ↔ Mono f
⊢ [Mono f, kernel.ι f = 0, (ShortComplex.mk 0 f ⋯).Exact].TFAE

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
⊢ [Mono f, kernel.ι f = 0, (ShortComplex.mk 0 f ⋯).Exact].TFAE

Tactic:
tfae_have 1 → 2
| _ => by rw [← cancel_mono f, kernel.condition, zero_comp]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
tfae_1_to_2 : Mono f → kernel.ι f = 0
⊢ [Mono f, kernel.ι f = 0, (ShortComplex.mk 0 f ⋯).Exact].TFAE
-- Mathlib/Order/UpperLower/Basic.lean
lemma erase_inf_Ici (ha : a ∈ s) (has : ∀ b ∈ s, b ≤ a → b = a) : s.erase a ⊓ Ici a = s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ s.erase a ⊓ Ici a = s

Tactic:
rw [← upperClosure_singleton, ← sdiff_singleton, sdiff_inf_upperClosure] <;> simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_shiftLeft {x : BitVec w} :
    (x <<< n).toInt = (x.toNat <<< n : Int).bmod (2^w)

Proof state:
w n : Nat
x : BitVec w
⊢ (x <<< n).toInt = (↑(x.toNat <<< n)).bmod (2 ^ w)

Tactic:
rw [toInt_eq_toNat_bmod, toNat_shiftLeft, Nat.shiftLeft_eq]

Result:
w n : Nat
x : BitVec w
⊢ (↑(x.toNat * 2 ^ n % 2 ^ w)).bmod (2 ^ w) = (↑(x.toNat * 2 ^ n)).bmod (2 ^ w)

Proof state:
w n : Nat
x : BitVec w
⊢ (↑(x.toNat * 2 ^ n % 2 ^ w)).bmod (2 ^ w) = (↑(x.toNat * 2 ^ n)).bmod (2 ^ w)

Tactic:
simp

Result:
no goals