harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem isBigO_atTop_natCast_rpow_of_tendsto_div_rpow {𝕜 : Type*} [RCLike 𝕜] {g : ℕ → 𝕜}
    {a : 𝕜} {r : ℝ} (hlim : Tendsto (fun n ↦ g n / (n ^ r : ℝ)) atTop (𝓝 a)) :
    g =O[atTop] fun n ↦ (n : ℝ) ^ r

Proof state:
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n => g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ g =O[atTop] fun n => ↑n ^ r

Tactic:
refine (isBigO_of_div_tendsto_nhds ?_ ‖a‖ ?_).of_norm_left

Result:
case refine_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n => g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ ∀ᶠ (x : ℕ) in atTop, ↑x ^ r = 0 → ‖g x‖ = 0

case refine_2
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n => g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ Tendsto ((fun x => ‖g x‖) / fun n => ↑n ^ r) atTop (𝓝 ‖a‖)

Proof state:
case h
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n => g n / ↑(↑n ^ r)) atTop (𝓝 a)
a✝ : ℕ
h : a✝ ≠ 0
⊢ ↑a✝ ^ r = 0 → ‖g a✝‖ = 0

Tactic:
simp [Real.rpow_eq_zero_iff_of_nonneg, h]

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n => g n / ↑(↑n ^ r)) atTop (𝓝 a)
n : ℕ
⊢ ‖g n / ↑(↑n ^ r)‖ = ((fun x => ‖g x‖) / fun n => ↑n ^ r) n

Tactic:
simp [abs_of_nonneg, show 0 ≤ (n : ℝ) ^ r by positivity]

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n => g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ Tendsto ((fun x => ‖g x‖) / fun n => ↑n ^ r) atTop (𝓝 ‖a‖)

Tactic:
exact hlim.norm.congr fun n ↦ by simp [abs_of_nonneg, show 0 ≤ (n : ℝ) ^ r by positivity]

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n => g n / ↑(↑n ^ r)) atTop (𝓝 a)
n : ℕ
⊢ 0 ≤ ↑n ^ r

Tactic:
positivity

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n => g n / ↑(↑n ^ r)) atTop (𝓝 a)
⊢ ∀ᶠ (x : ℕ) in atTop, ↑x ^ r = 0 → ‖g x‖ = 0

Tactic:
filter_upwards [eventually_ne_atTop 0] with _ h

Result:
case h
𝕜 : Type u_2
inst✝ : RCLike 𝕜
g : ℕ → 𝕜
a : 𝕜
r : ℝ
hlim : Tendsto (fun n => g n / ↑(↑n ^ r)) atTop (𝓝 a)
a✝ : ℕ
h : a✝ ≠ 0
⊢ ↑a✝ ^ r = 0 → ‖g a✝‖ = 0
-- Mathlib/MeasureTheory/Covering/DensityTheorem.lean
theorem closedBall_mem_vitaliFamily_of_dist_le_mul {K : ℝ} {x y : α} {r : ℝ} (h : dist x y ≤ K * r)
    (rpos : 0 < r) : closedBall y r ∈ (vitaliFamily μ K).setsAt x

Proof state:
case pos.h.inr
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
⊢ μ (closedBall x (3 * (R / 4))) ≤ ↑(scalingConstantOf μ ((4 * K + 3) ⊔ 3)) * μ (closedBall y r)

Tactic:
have : closedBall x (3 * (R / 4)) ⊆ closedBall y r := by
  apply closedBall_subset_closedBall'
  have A : y ∈ closedBall y r := mem_closedBall_self rpos.le
  have B := mem_closedBall'.1 (H A)
  linarith

Result:
case pos.h.inr
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
R : ℝ := scalingScaleOf μ ((4 * K + 3) ⊔ 3)
H : closedBall y r ⊆ closedBall x (R / 4)
hr : R < r
this : closedBall x (3 * (R / 4)) ⊆ closedBall y r
⊢ μ (closedBall x (3 * (R / 4))) ≤ ↑(scalingConstantOf μ ((4 * K + 3) ⊔ 3)) * μ (closedBall y r)
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem lcm_dvd_iff [GCDMonoid α] {a b c : α} : lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Proof state:
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
have h : gcd a b ≠ 0 := fun H => h1 ((gcd_eq_zero_iff _ _).1 H).1

Result:
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h✝ : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : gcd a b ≠ 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Proof state:
case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
obtain ⟨h1, h2⟩ := not_or.1 h

Result:
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Proof state:
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : a = 0 ∨ b = 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
rcases h with (rfl | rfl) <;>
  simp +contextual only [iff_def, lcm_zero_left, lcm_zero_right,
    zero_dvd_iff, dvd_zero, eq_self_iff_true, and_true, imp_true_iff]

Result:
no goals

Proof state:
case neg.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h✝ : ¬(a = 0 ∨ b = 0)
h1 : ¬a = 0
h2 : ¬b = 0
h : gcd a b ≠ 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
rw [← mul_dvd_mul_iff_left h, (gcd_mul_lcm a b).dvd_iff_dvd_left, ←
  (gcd_mul_right' c a b).dvd_iff_dvd_right, dvd_gcd_iff, mul_comm b c, mul_dvd_mul_iff_left h1,
  mul_dvd_mul_iff_right h2, and_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

Tactic:
by_cases h : a = 0 ∨ b = 0

Result:
case pos
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : a = 0 ∨ b = 0
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c

case neg
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
h : ¬(a = 0 ∨ b = 0)
⊢ lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem ih_0 : ih 0 a :=
  ⟨rfl, by simp [T_def, mul_div_cancel₀ _ (ne_of_gt (deriv_sq_norm_pos hnorm))]⟩

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
⊢ ‖Polynomial.eval a F‖ ≤ ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ 0

Tactic:
simp [T_def, mul_div_cancel₀ _ (ne_of_gt (deriv_sq_norm_pos hnorm))]

Result:
no goals
-- Mathlib/RingTheory/Flat/Basic.lean
/-- A `R`-module linearly equivalent to a flat `R`-module is flat. -/
lemma of_linearEquiv [Flat R M] (e : N ≃ₗ[R] M) : Flat R N :=
  of_retract e.toLinearMap e.symm (by simp)

Proof state:
R : Type u
M : Type v
N : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Flat R M
e : N ≃ₗ[R] M
⊢ ↑e.symm ∘ₗ ↑e = LinearMap.id

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_sq_le_one : cos x ^ 2 ≤ 1

Proof state:
x : ℝ
⊢ cos x ^ 2 ≤ 1

Tactic:
rw [← sin_sq_add_cos_sq x]

Result:
x : ℝ
⊢ cos x ^ 2 ≤ sin x ^ 2 + cos x ^ 2

Proof state:
x : ℝ
⊢ cos x ^ 2 ≤ sin x ^ 2 + cos x ^ 2

Tactic:
exact le_add_of_nonneg_left (sq_nonneg _)

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma polyCharpoly_coeff_nilRankAux_ne_zero [Nontrivial R] :
    (polyCharpoly φ b).coeff (nilRankAux φ b) ≠ 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : Nontrivial R
⊢ (φ.polyCharpoly b).coeff (φ.nilRankAux b) ≠ 0

Tactic:
apply Polynomial.trailingCoeff_nonzero_iff_nonzero.mpr

Result:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : Nontrivial R
⊢ φ.polyCharpoly b ≠ 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup L
inst✝⁷ : Module R L
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
φ : L →ₗ[R] End R M
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : Free R M
inst✝¹ : Module.Finite R M
b : Basis ι R L
inst✝ : Nontrivial R
⊢ φ.polyCharpoly b ≠ 0

Tactic:
apply polyCharpoly_ne_zero

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderIso.lean
theorem preimage_Ioi (e : α ≃o β) (b : β) : e ⁻¹' Ioi b = Ioi (e.symm b)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ⇑e ⁻¹' Ioi b ↔ x ∈ Ioi (e.symm b)

Tactic:
simp [← e.lt_iff_lt]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
⊢ ⇑e ⁻¹' Ioi b = Ioi (e.symm b)

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ⇑e ⁻¹' Ioi b ↔ x ∈ Ioi (e.symm b)
-- Mathlib/Analysis/Convex/Mul.lean
lemma ConvexOn.smul'' [OrderedSMul 𝕜 E] (hf : ConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g)
    (hf₀ : ∀ ⦃x⦄, x ∈ s → f x ≤ 0) (hg₀ : ∀ ⦃x⦄, x ∈ s → g x ≤ 0) (hfg : AntivaryOn f g s) :
    ConcaveOn 𝕜 s (f • g)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0
hfg : AntivaryOn f g s
⊢ ConcaveOn 𝕜 s (f • g)

Tactic:
rw [← neg_smul_neg]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0
hfg : AntivaryOn f g s
⊢ ConcaveOn 𝕜 s (-f • -g)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0
hfg : AntivaryOn f g s
⊢ ConcaveOn 𝕜 s (-f • -g)

Tactic:
exact hf.neg.smul' hg.neg (fun x hx ↦ neg_nonneg.2 <| hf₀ hx) (fun x hx ↦ neg_nonneg.2 <| hg₀ hx)
  hfg.neg

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_diff_singleton_le (s : Set α) (a : α) : (s \ {a}).ncard ≤ s.ncard

Proof state:
case inr
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ (s \ {a}).ncard ≤ s.ncard

Tactic:
convert zero_le (α := ℕ) _

Result:
case h.e'_3
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ (s \ {a}).ncard = 0

Proof state:
α : Type u_1
s : Set α
a : α
⊢ (s \ {a}).ncard ≤ s.ncard

Tactic:
obtain hs | hs := s.finite_or_infinite

Result:
case inl
α : Type u_1
s : Set α
a : α
hs : s.Finite
⊢ (s \ {a}).ncard ≤ s.ncard

case inr
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ (s \ {a}).ncard ≤ s.ncard

Proof state:
case h.e'_3
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ (s \ {a}).ncard = 0

Tactic:
exact (hs.diff (by simp : Set.Finite {a})).ncard

Result:
no goals

Proof state:
case inl
α : Type u_1
s : Set α
a : α
hs : s.Finite
⊢ (s \ {a}).ncard ≤ s.ncard

Tactic:
apply ncard_le_ncard diff_subset hs

Result:
no goals

Proof state:
α : Type u_1
s : Set α
a : α
hs : s.Infinite
⊢ {a}.Finite

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_insert_right : image2 f s (insert b t) = (fun a => f a b) '' s ∪ image2 f s t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
b : β
⊢ image2 f s (insert b t) = (fun a => f a b) '' s ∪ image2 f s t

Tactic:
rw [insert_eq, image2_union_right, image2_singleton_right]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
theorem StrongMono.iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
    (e : Arrow.mk f ≅ Arrow.mk g) : StrongMono f ↔ StrongMono g

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
a✝ : StrongMono f
⊢ StrongMono g

case mpr
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
a✝ : StrongMono g
⊢ StrongMono f

Tactic:
exacts [StrongMono.of_arrow_iso e, StrongMono.of_arrow_iso e.symm]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongMono f ↔ StrongMono g

Tactic:
constructor <;> intro

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
a✝ : StrongMono f
⊢ StrongMono g

case mpr
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
a✝ : StrongMono g
⊢ StrongMono f
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendsto_comp_of_locally_uniform_limit (h : ContinuousAt f x) (hg : Tendsto g p (𝓝 x))
    (hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u) :
    Tendsto (fun n => F n (g n)) p (𝓝 (f x))

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝[univ] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n => F n (g n)) p (𝓝 (f x))

Tactic:
exact tendsto_comp_of_locally_uniform_limit_within h hg hunif

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousAt f x
hg : Tendsto g p (𝓝 x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n => F n (g n)) p (𝓝 (f x))

Tactic:
rw [← continuousWithinAt_univ] at h

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝 x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n => F n (g n)) p (𝓝 (f x))

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝 x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n => F n (g n)) p (𝓝 (f x))

Tactic:
rw [← nhdsWithin_univ] at hunif hg

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
inst✝ : TopologicalSpace α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝[univ] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n => F n (g n)) p (𝓝 (f x))
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem exists_linearIsometryEquiv_eq_of_det_pos {f : V ≃ₗᵢ[ℝ] V}
    (hd : 0 < LinearMap.det (f.toLinearEquiv : V →ₗ[ℝ] V)) :
    ∃ θ : Real.Angle, f = o.rotation θ

Proof state:
case h.a.a
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
i : Fin 2
⊢ ↑(o.rotation (o.oangle x (f x))).toLinearEquiv ((o.basisRightAngleRotation x hx) i) =
    ↑f.toLinearEquiv ((o.basisRightAngleRotation x hx) i)

Tactic:
fin_cases i

Result:
case h.a.a.«0»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ↑(o.rotation (o.oangle x (f x))).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨0, ⋯⟩)) =
    ↑f.toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨0, ⋯⟩))

case h.a.a.«1»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ↑(o.rotation (o.oangle x (f x))).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨1, ⋯⟩)) =
    ↑f.toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨1, ⋯⟩))

Proof state:
case h.a.a.«0»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ↑(o.rotation (o.oangle x (f x))).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨0, ⋯⟩)) =
    ↑f.toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨0, ⋯⟩))

Tactic:
simp

Result:
no goals

Proof state:
case h.a.a.«1»
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : o.oangle (o.rightAngleRotation x) (f (o.rightAngleRotation x)) = o.oangle x (f x)
⊢ ↑(o.rotation (o.oangle x (f x))).toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨1, ⋯⟩)) =
    ↑f.toLinearEquiv ((o.basisRightAngleRotation x hx) ((fun i => i) ⟨1, ⋯⟩))

Tactic:
simp [← this]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
⊢ ∃ θ, f = o.rotation θ

Tactic:
obtain ⟨x, hx⟩ : ∃ x, x ≠ (0 : V) := exists_ne (0 : V)

Result:
case intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
f : V ≃ₗᵢ[ℝ] V
hd : 0 < LinearMap.det ↑f.toLinearEquiv
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ∃ θ, f = o.rotation θ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Control.lean
theorem findM?_eq_findSomeM? [Monad m] [LawfulMonad m] (p : α → m Bool) (as : List α) :
    as.findM? p = as.findSomeM? fun a => return if (← p a) then some a else none

Proof state:
case cons.e_a.h
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m Bool
a : α
as : List α
ih :
  findM? p as =
    findSomeM?
      (fun a => do
        let __do_lift ← p a
        pure (if __do_lift = true then some a else none))
      as
b : Bool
⊢ (match b with
    | true => pure (some a)
    | false => findSomeM? (fun a => (fun a_1 => if a_1 = true then some a else none) <$> p a) as) =
    match if b = true then some a else none with
    | some b => pure (some b)
    | none => findSomeM? (fun a => (fun a_1 => if a_1 = true then some a else none) <$> p a) as

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem circleIntegrable_sub_zpow_iff {c w : ℂ} {R : ℝ} {n : ℤ} :
    CircleIntegrable (fun z => (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ w ∉ sphere c |R|

Proof state:
case mp.intro.intro
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ sphere c |R|
⊢ ¬IntervalIntegrable (fun θ => (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)

Tactic:
rw [← image_circleMap_Ioc] at hw

Result:
case mp.intro.intro
c w : ℂ
R : ℝ
n : ℤ
hR : R ≠ 0
hn : n < 0
hw : w ∈ circleMap c R '' Ioc 0 (2 * π)
⊢ ¬IntervalIntegrable (fun θ => (circleMap 0 R θ * I) • (circleMap c R θ - w) ^ n) volume 0 (2 * π)
-- Mathlib/Topology/Sets/Closeds.lean
theorem coe_sup (s t : Closeds α) : (↑(s ⊔ t) : Set α) = ↑s ∪ ↑t

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
s t : Closeds α
⊢ ↑(s ⊔ t) = ↑s ∪ ↑t

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Ideal.lean
theorem isProper_of_not_mem {I : Ideal P} {p : P} (nmem : p ∉ I) : IsProper I :=
  ⟨fun hp ↦ by
    have := mem_univ p
    rw [← hp] at this
    exact nmem this⟩

Proof state:
P : Type u_1
inst✝ : LE P
I : Ideal P
p : P
nmem : p ∉ I
hp : ↑I = univ
⊢ False

Tactic:
have := mem_univ p

Result:
P : Type u_1
inst✝ : LE P
I : Ideal P
p : P
nmem : p ∉ I
hp : ↑I = univ
this : p ∈ univ
⊢ False

Proof state:
P : Type u_1
inst✝ : LE P
I : Ideal P
p : P
nmem : p ∉ I
hp : ↑I = univ
this : p ∈ ↑I
⊢ False

Tactic:
exact nmem this

Result:
no goals

Proof state:
P : Type u_1
inst✝ : LE P
I : Ideal P
p : P
nmem : p ∉ I
hp : ↑I = univ
this : p ∈ univ
⊢ False

Tactic:
rw [← hp] at this

Result:
P : Type u_1
inst✝ : LE P
I : Ideal P
p : P
nmem : p ∉ I
hp : ↑I = univ
this : p ∈ ↑I
⊢ False
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma colimitsOfShape_le_of_final {J' : Type*} [Category J'] (F : J ⥤ J') [F.Final] :
    W.colimitsOfShape J' ≤ W.colimitsOfShape J

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : J' ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
this : h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = h₁'.desc { pt := c₂.pt, ι := whiskerLeft F f ≫ (Cocone.whisker F c₂).ι }
⊢ W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
rw [this]

Result:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : J' ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
this : h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = h₁'.desc { pt := c₂.pt, ι := whiskerLeft F f ≫ (Cocone.whisker F c₂).ι }
⊢ W.colimitsOfShape J (h₁'.desc { pt := c₂.pt, ι := whiskerLeft F f ≫ (Cocone.whisker F c₂).ι })

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : J' ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
this : h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = h₁'.desc { pt := c₂.pt, ι := whiskerLeft F f ≫ (Cocone.whisker F c₂).ι }
⊢ W.colimitsOfShape J (h₁'.desc { pt := c₂.pt, ι := whiskerLeft F f ≫ (Cocone.whisker F c₂).ι })

Tactic:
exact ⟨_, _, _, _, h₁', h₂', _, fun _ ↦ hf _⟩

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : J' ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
⊢ W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
have h₁' : IsColimit (c₁.whisker F) := (Functor.Final.isColimitWhiskerEquiv F c₁).symm h₁

Result:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : J' ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
⊢ W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })