harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
/-- Transfer reflection of colimits along an equivalence in the shape. -/
lemma reflectsColimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
    [ReflectsColimitsOfShape J F] : ReflectsColimitsOfShape J' F where
  reflectsColimit :=
    { reflects := fun {c} t => ⟨by
        apply IsColimit.ofWhiskerEquivalence e
        apply isColimitOfReflects F
        apply IsColimit.ofIsoColimit _ (Functor.mapCoconeWhisker _).symm
        exact IsColimit.whiskerEquivalence t _⟩ }

Proof state:
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (F.mapCocone (Cocone.whisker e.functor c))

Tactic:
apply IsColimit.ofIsoColimit _ (Functor.mapCoconeWhisker _).symm

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (Cocone.whisker e.functor (F.mapCocone c))

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (Cocone.whisker e.functor (F.mapCocone c))

Tactic:
exact IsColimit.whiskerEquivalence t _

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit c

Tactic:
apply IsColimit.ofWhiskerEquivalence e

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (Cocone.whisker e.functor c)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (Cocone.whisker e.functor c)

Tactic:
apply isColimitOfReflects F

Result:
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (F.mapCocone (Cocone.whisker e.functor c))
-- Mathlib/Data/Nat/PSub.lean
theorem ppred_eq_none : ∀ {n : ℕ}, ppred n = none ↔ n = 0
  | 0 => by simp
  | n + 1 => by constructor <;> intro <;> contradiction

Proof state:
n : ℕ
⊢ (n + 1).ppred = none ↔ n + 1 = 0

Tactic:
constructor <;> intro <;> contradiction

Result:
no goals

Proof state:
⊢ ppred 0 = none ↔ 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
theorem lift_binop_eq (f : ℚ → ℚ → ℚ) (f₁ : ℤ → ℤ → ℤ → ℤ → ℤ) (f₂ : ℤ → ℤ → ℤ → ℤ → ℤ)
    (fv :
      ∀ {n₁ d₁ h₁ c₁ n₂ d₂ h₂ c₂},
        f ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ = f₁ n₁ d₁ n₂ d₂ /. f₂ n₁ d₁ n₂ d₂)
    (f0 : ∀ {n₁ d₁ n₂ d₂}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0) (a b c d : ℤ)
    (b0 : b ≠ 0) (d0 : d ≠ 0)
    (H :
      ∀ {n₁ d₁ n₂ d₂}, a * d₁ = n₁ * b → c * d₂ = n₂ * d →
        f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂) :
    f (a /. b) (c /. d) = f₁ a b c d /. f₂ a b c d

Proof state:
case mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
x : ℚ
hc : c /. d = x
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } x = f₁ a b c d /. f₂ a b c d

Tactic:
obtain ⟨n₂, d₂, h₂, c₂⟩ := x

Result:
case mk'.mk'
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ }
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
    f₁ a b c d /. f₂ a b c d
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem antilipschitz (h : Isometry f) : AntilipschitzWith 1 f := fun x y => by
  simp only [h x y, ENNReal.coe_one, one_mul, le_refl]

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : Isometry f
x y : α
⊢ edist x y ≤ ↑1 * edist (f x) (f y)

Tactic:
simp only [h x y, ENNReal.coe_one, one_mul, le_refl]

Result:
no goals
-- Mathlib/Analysis/Complex/RealDeriv.lean
theorem HasDerivWithinAt.complexToReal_fderiv {f : ℂ → ℂ} {s : Set ℂ} {f' x : ℂ}
    (h : HasDerivWithinAt f f' s x) : HasFDerivWithinAt f (f' • (1 : ℂ →L[ℝ] ℂ)) s x

Proof state:
f : ℂ → ℂ
s : Set ℂ
f' x : ℂ
h : HasDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f (f' • 1) s x

Tactic:
simpa only [Complex.restrictScalars_one_smulRight] using h.hasFDerivWithinAt.restrictScalars ℝ

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean
/-- The **Schwartz-Zippel lemma**

For a nonzero multivariable polynomial `p` over an integral domain, the probability that `p`
evaluates to zero at points drawn at random from a product of finite subsets `S i` of the integral
domain is bounded by the sum of `degᵢ p / #(S i)`. -/
lemma schwartz_zippel_sum_degreeOf {n} {p : MvPolynomial (Fin n) R} (hp : p ≠ 0)
    (S : Fin n → Finset R) :
    #{x ∈ S ^^ n | eval x p = 0} / ∏ i, (#(S i) : ℚ≥0) ≤ ∑ i, (p.degreeOf i / #(S i) : ℚ≥0)

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Fin n → Finset R
s : Fin n →₀ ℕ
hs : s ∈ p.support
⊢ ∑ i : Fin n, ↑(s i) / ↑(#(S i)) ≤ ∑ i : Fin n, ↑(degreeOf i p) / ↑(#(S i))

Tactic:
gcongr with i

Result:
case h.hab.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Fin n → Finset R
s : Fin n →₀ ℕ
hs : s ∈ p.support
i : Fin n
a✝ : i ∈ univ
⊢ s i ≤ degreeOf i p

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Fin n → Finset R
⊢ ↑(#(filter (fun x => (eval x) p = 0) (piFinset fun i => S i))) / ∏ i : Fin n, ↑(#(S i)) ≤
    ∑ i : Fin n, ↑(degreeOf i p) / ↑(#(S i))

Tactic:
calc
  _ ≤ p.support.sup fun s ↦ ∑ i, (s i / #(S i) : ℚ≥0) := schwartz_zippel_sup_sum hp S
  _ ≤ ∑ i, (p.degreeOf i / #(S i) : ℚ≥0) := Finset.sup_le fun s hs ↦ by
    gcongr with i; exact monomial_le_degreeOf i hs

Result:
no goals

Proof state:
case h.hab.h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Fin n → Finset R
s : Fin n →₀ ℕ
hs : s ∈ p.support
i : Fin n
a✝ : i ∈ univ
⊢ s i ≤ degreeOf i p

Tactic:
exact monomial_le_degreeOf i hs

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem any (f) : ∀ {s}, ValidFor l m r s → s.any f = m.any f
  | _, ⟨⟩ => by simp [-List.append_assoc, Substring.any, anyAux_of_valid]

Proof state:
l m r : List Char
f : Char → Bool
⊢ { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
          stopPos := { byteIdx := utf8Len l + utf8Len m } }.any
      f =
    m.any f

Tactic:
simp [-List.append_assoc, Substring.any, anyAux_of_valid]

Result:
no goals
-- Mathlib/RingTheory/RingHom/Integral.lean
theorem isIntegral_stableUnderComposition : StableUnderComposition fun f => f.IsIntegral

Proof state:
⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral

Tactic:
introv R hf hg

Result:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.IsIntegral
hg : g.IsIntegral
⊢ (g.comp f).IsIntegral

Proof state:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.IsIntegral
hg : g.IsIntegral
⊢ (g.comp f).IsIntegral

Tactic:
exact hf.trans _ _ hg

Result:
no goals
-- Mathlib/Order/Filter/Subsingleton.lean
theorem subsingleton_iff_exists_le_pure [Nonempty α] : l.Subsingleton ↔ ∃ a, l ≤ pure a

Proof state:
case inl
α : Type u_1
inst✝ : Nonempty α
⊢ ⊥.Subsingleton ↔ ∃ a, ⊥ ≤ pure a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : Filter α
inst✝ : Nonempty α
⊢ l.Subsingleton ↔ ∃ a, l ≤ pure a

Tactic:
rcases eq_or_neBot l with rfl | hbot

Result:
case inl
α : Type u_1
inst✝ : Nonempty α
⊢ ⊥.Subsingleton ↔ ∃ a, ⊥ ≤ pure a

case inr
α : Type u_1
l : Filter α
inst✝ : Nonempty α
hbot : l.NeBot
⊢ l.Subsingleton ↔ ∃ a, l ≤ pure a

Proof state:
case inr
α : Type u_1
l : Filter α
inst✝ : Nonempty α
hbot : l.NeBot
⊢ l.Subsingleton ↔ ∃ a, l ≤ pure a

Tactic:
simp [subsingleton_iff_bot_or_pure, ← hbot.le_pure_iff, hbot.ne]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem rotateLeft_zero (l : List α) : rotateLeft l 0 = l

Proof state:
α : Type u_1
l : List α
⊢ l.rotateLeft 0 = l

Tactic:
simp [rotateLeft]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem monic_one [AddZeroClass A] (hD : D.Injective) : (1 : R[A]).Monic D

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : AddZeroClass A
hD : Function.Injective D
⊢ Monic D 1

Tactic:
rw [Monic, one_def, leadingCoeff_single hD]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma tendsto_defaultRatCDF_atBot : Tendsto defaultRatCDF atBot (𝓝 0)

Proof state:
q : ℚ
hq : q ≤ -1
⊢ -1 < 0

Tactic:
linarith

Result:
no goals

Proof state:
⊢ Tendsto defaultRatCDF atBot (𝓝 0)

Tactic:
refine (tendsto_congr' ?_).mp tendsto_const_nhds

Result:
⊢ (fun x => 0) =ᶠ[atBot] defaultRatCDF

Proof state:
⊢ ∃ a, ∀ b ≤ a, 0 = defaultRatCDF b

Tactic:
refine ⟨-1, fun q hq => (if_pos (hq.trans_lt ?_)).symm⟩

Result:
q : ℚ
hq : q ≤ -1
⊢ -1 < 0

Proof state:
⊢ (fun x => 0) =ᶠ[atBot] defaultRatCDF

Tactic:
rw [EventuallyEq, eventually_atBot]

Result:
⊢ ∃ a, ∀ b ≤ a, 0 = defaultRatCDF b
-- Mathlib/Data/Set/Prod.lean
theorem piCongrLeft_preimage_pi (f : ι' ≃ ι) (s : Set ι') (t : ∀ i, Set (α i)) :
    f.piCongrLeft α ⁻¹' (f '' s).pi t = s.pi fun i => t (f i)

Proof state:
case h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ ∀ (a : (b : ι) → α b),
    (piCongrLeft α f).symm a ∈ ⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t ↔ (piCongrLeft α f).symm a ∈ s.pi fun i => t (f i)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ ⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t = s.pi fun i => t (f i)

Tactic:
apply Set.ext

Result:
case h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ ∀ (x : (a : ι') → α (f a)), x ∈ ⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t ↔ x ∈ s.pi fun i => t (f i)

Proof state:
case h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ ∀ (x : (a : ι') → α (f a)), x ∈ ⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t ↔ x ∈ s.pi fun i => t (f i)

Tactic:
rw [← (f.piCongrLeft α).symm.forall_congr_right]

Result:
case h
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
f : ι' ≃ ι
s : Set ι'
t : (i : ι) → Set (α i)
⊢ ∀ (a : (b : ι) → α b),
    (piCongrLeft α f).symm a ∈ ⇑(piCongrLeft α f) ⁻¹' (⇑f '' s).pi t ↔ (piCongrLeft α f).symm a ∈ s.pi fun i => t (f i)
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tan_mul_cos {x : ℝ} (hx : cos x ≠ 0) : tan x * cos x = sin x

Proof state:
x : ℝ
hx : cos x ≠ 0
⊢ tan x * cos x = sin x

Tactic:
rw [tan_eq_sin_div_cos, div_mul_cancel₀ _ hx]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/CommRing.lean
theorem totalDegree_sub (a b : MvPolynomial σ R) :
    (a - b).totalDegree ≤ max a.totalDegree b.totalDegree :=
  calc
    (a - b).totalDegree = (a + -b).totalDegree

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
a b : MvPolynomial σ R
⊢ (a - b).totalDegree = (a + -b).totalDegree

Tactic:
rw [sub_eq_add_neg]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
a b : MvPolynomial σ R
⊢ a.totalDegree ⊔ (-b).totalDegree = a.totalDegree ⊔ b.totalDegree

Tactic:
rw [totalDegree_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem toList_attach {α : Type _} {l : Array α} :
    l.attach.toList = l.toList.attachWith (· ∈ l) (by simp [mem_toList])

Proof state:
α : Type u_1
l : Array α
⊢ l.attach.toList = l.toList.attachWith (fun x => x ∈ l) ⋯

Tactic:
simp [attach]

Result:
no goals

Proof state:
α : Type ?u.3235
l : Array α
⊢ ∀ (x : α), x ∈ l.toList → (fun x => x ∈ l) x

Tactic:
simp [mem_toList]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem degree_C_mul_T_le (n : ℤ) (a : R) : degree (C a * T n) ≤ n

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ (C a * T n).degree ≤ ↑n

Tactic:
by_cases a0 : a = 0

Result:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a = 0
⊢ (C a * T n).degree ≤ ↑n

case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : ¬a = 0
⊢ (C a * T n).degree ≤ ↑n

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : ¬a = 0
⊢ (C a * T n).degree ≤ ↑n

Tactic:
exact (degree_C_mul_T n a a0).le

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a = 0
⊢ (C a * T n).degree ≤ ↑n

Tactic:
simp only [a0, map_zero, zero_mul, degree_zero, bot_le]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem mul_le_iff_le_inv {a b r : ℝ≥0∞} (hr₀ : r ≠ 0) (hr₁ : r ≠ ∞) : r * a ≤ b ↔ a ≤ r⁻¹ * b

Proof state:
a b r : ℝ≥0∞
hr₀ : r ≠ 0
hr₁ : r ≠ ⊤
⊢ r * a ≤ b ↔ a ≤ r⁻¹ * b

Tactic:
rw [← @ENNReal.mul_le_mul_left _ a _ hr₀ hr₁, ← mul_assoc, ENNReal.mul_inv_cancel hr₀ hr₁,
  one_mul]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iInf_emptyset {f : β → α} : ⨅ x ∈ (∅ : Set β), f x = ⊤

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
⊢ ⨅ x ∈ ∅, f x = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/NoncommCoprod.lean
theorem noncommCoprod_comp_inl : (f.noncommCoprod g comm).comp (inl M N) = f :=
  ext fun x => by simp

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : Monoid P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
x : M
⊢ ((f.noncommCoprod g comm).comp (inl M N)) x = f x

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Trace/Basic.lean
theorem Algebra.traceForm_toMatrix_powerBasis (h : PowerBasis R S) :
    BilinForm.toMatrix h.basis (traceForm R S) = of fun i j => trace R S (h.gen ^ (i.1 + j.1))

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : PowerBasis R S
⊢ (BilinForm.toMatrix h.basis) (traceForm R S) = of fun i j => (trace R S) (h.gen ^ (↑i + ↑j))

Tactic:
ext

Result:
case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : PowerBasis R S
i✝ j✝ : Fin h.dim
⊢ (BilinForm.toMatrix h.basis) (traceForm R S) i✝ j✝ = of (fun i j => (trace R S) (h.gen ^ (↑i + ↑j))) i✝ j✝

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : PowerBasis R S
i✝ j✝ : Fin h.dim
⊢ (BilinForm.toMatrix h.basis) (traceForm R S) i✝ j✝ = of (fun i j => (trace R S) (h.gen ^ (↑i + ↑j))) i✝ j✝

Tactic:
rw [traceForm_toMatrix, of_apply, pow_add, h.basis_eq_pow, h.basis_eq_pow]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem map_id : map (LinearMap.id : M →ₗ[R] M) p = p :=
  Submodule.ext fun a => by simp

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : M
⊢ a ∈ map LinearMap.id p ↔ a ∈ p

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem affinity_unitClosedBall {r : ℝ} (hr : 0 ≤ r) (x : E) :
    x +ᵥ r • closedBall (0 : E) 1 = closedBall x r

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
⊢ x +ᵥ r • closedBall 0 1 = closedBall x r

Tactic:
rw [smul_unitClosedBall, Real.norm_of_nonneg hr, vadd_closedBall_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem and_assoc (x y z : Nat) : (x &&& y) &&& z = x &&& (y &&& z)

Proof state:
x y z : Nat
⊢ x &&& y &&& z = x &&& (y &&& z)

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
x y z : Nat
⊢ ∀ (i : Nat), (x &&& y &&& z).testBit i = (x &&& (y &&& z)).testBit i

Proof state:
case pred
x y z : Nat
⊢ ∀ (i : Nat), (x &&& y &&& z).testBit i = (x &&& (y &&& z)).testBit i

Tactic:
simp [Bool.and_assoc]

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem isImage_source_target_of_disjoint (e' : PartialEquiv α β) (hs : Disjoint e.source e'.source)
    (ht : Disjoint e.target e'.target) : e.IsImage e'.source e'.target :=
  IsImage.of_image_eq <| by rw [hs.inter_eq, ht.inter_eq, image_empty]

Proof state:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
⊢ ↑e '' (e.source ∩ e'.source) = e.target ∩ e'.target

Tactic:
rw [hs.inter_eq, ht.inter_eq, image_empty]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem self_mem_cylinder (x : ∀ n, E n) (n : ℕ) : x ∈ cylinder x n

Proof state:
E : ℕ → Type u_1
x : (n : ℕ) → E n
n : ℕ
⊢ x ∈ cylinder x n

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.continuousOn (hf : HasFPowerSeriesOnBall f p x r) :
    ContinuousOn f (EMetric.ball x r)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ ContinuousOn f (EMetric.ball x r)

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ ContinuousOn f (EMetric.ball x r)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ ContinuousOn f (EMetric.ball x r)

Tactic:
simpa using hf.continuousOn

Result:
no goals
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_zero : birthday 0 = 0

Proof state:
⊢ birthday 0 ≤ PGame.birthday 0

Tactic:
exact birthday_quot_le_pGameBirthday  _

Result:
no goals

Proof state:
⊢ birthday 0 = 0

Tactic:
rw [← Ordinal.le_zero, ← PGame.birthday_zero]

Result:
⊢ birthday 0 ≤ PGame.birthday 0
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem hasSum_cauchyPowerSeries_integral {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ}
    (hf : CircleIntegrable f c R) (hw : ‖w‖ < R) :
    HasSum (fun n => cauchyPowerSeries f c R n fun _ => w)
      ((2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - (c + w))⁻¹ • f z)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
⊢ HasSum (fun n => (cauchyPowerSeries f c R n) fun x => w)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

Tactic:
simp only [cauchyPowerSeries_apply]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
⊢ HasSum (fun n => (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R : ℝ
w : ℂ
hf : CircleIntegrable f c R
hw : ‖w‖ < R
⊢ HasSum (fun n => (2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
    ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

Tactic:
exact (hasSum_two_pi_I_cauchyPowerSeries_integral hf hw).const_smul _

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem image_update_Ico (f : ∀ i, α i) (i : ι) (a b : α i) :
    update f i '' Ico a b = Ico (update f i a) (update f i b)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ico a b = Ico (update f i a) (update f i b)

Tactic:
rw [← Icc_diff_right, ← Icc_diff_right, image_diff (update_injective _ _), image_singleton,
  image_update_Icc]

Result:
no goals
-- Mathlib/Order/CompleteLattice/SetLike.lean
@[simp] lemma mem_top : x ∈ (⊤ : L)

Proof state:
X : Type u_1
L : CompleteSublattice (Set X)
x : X
⊢ x ∈ ⊤

Tactic:
simp [← mem_subtype]

Result:
no goals
-- Mathlib/Topology/Compactness/SigmaCompact.lean
theorem mem_diff_shiftr_find (x : X) : x ∈ K.shiftr (K.find x + 1) \ K.shiftr (K.find x) :=
  ⟨K.mem_find _,
    mt K.shiftr.mem_iff_find_le.1 <| by simp only [find_shiftr, not_le, Nat.lt_succ_self]⟩

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ ¬K.shiftr.find x ≤ K.find x

Tactic:
simp only [find_shiftr, not_le, Nat.lt_succ_self]

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonUnitalRing_injective :
    Function.Injective (@toNonUnitalRing R)

Proof state:
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Result:
case h_add.h.h
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
x y : R
⊢ x + y = x + y

case h_mul.h.h
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
x y : R
⊢ x * y = x * y

Proof state:
R : Type u
⊢ Function.Injective (@toNonUnitalRing R)

Tactic:
intro _ _ h

Result:
R : Type u
a₁✝ a₂✝ : Ring R
h : toNonUnitalRing = toNonUnitalRing
⊢ a₁✝ = a₂✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem any_zero {f : (i : Nat) → i < 0 → Bool} : any 0 f = false

Proof state:
f : (i : Nat) → i < 0 → Bool
⊢ any 0 f = false

Tactic:
simp [any]

Result:
no goals