harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem ENNReal.tendsto_pow_atTop_nhds_top_iff {r : ℝ≥0∞} :
    Tendsto (fun n ↦ r^n) atTop (𝓝 ∞) ↔ 1 < r

Proof state:
case refine_1.intro
r : ℝ≥0∞
r_le_one : r ≤ 1
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 1 < r ^ b
⊢ False

Tactic:
exact lt_irrefl _ <| lt_of_lt_of_le (hn n le_rfl) <| pow_le_one₀ (zero_le _) r_le_one

Result:
no goals

Proof state:
case refine_1
r : ℝ≥0∞
r_le_one : r ≤ 1
h_tends : ∃ a, ∀ (b : ℕ), a ≤ b → 1 < r ^ b
⊢ False

Tactic:
obtain ⟨n, hn⟩ := h_tends

Result:
case refine_1.intro
r : ℝ≥0∞
r_le_one : r ≤ 1
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 1 < r ^ b
⊢ False

Proof state:
case refine_1
r : ℝ≥0∞
r_le_one : r ≤ 1
h_tends : Tendsto (fun n => r ^ n) atTop (𝓝 ⊤)
⊢ False

Tactic:
specialize h_tends (Ioi_mem_nhds one_lt_top)

Result:
case refine_1
r : ℝ≥0∞
r_le_one : r ≤ 1
h_tends : Set.Ioi 1 ∈ Filter.map (fun n => r ^ n) atTop
⊢ False

Proof state:
case refine_2
r : ℝ≥0∞
r_gt_one : 1 < r
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 ⊤)

Tactic:
have obs := @Tendsto.inv ℝ≥0∞ ℕ _ _ _ (fun n ↦ (r⁻¹)^n) atTop 0

Result:
case refine_2
r : ℝ≥0∞
r_gt_one : 1 < r
obs : Tendsto (fun n => r⁻¹ ^ n) atTop (𝓝 0) → Tendsto (fun x => (r⁻¹ ^ x)⁻¹) atTop (𝓝 0⁻¹)
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 ⊤)

Proof state:
case refine_1
r : ℝ≥0∞
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 ⊤) → 1 < r

Tactic:
contrapose!

Result:
case refine_1
r : ℝ≥0∞
⊢ r ≤ 1 → ¬Tendsto (fun n => r ^ n) atTop (𝓝 ⊤)

Proof state:
case refine_1
r : ℝ≥0∞
r_le_one : r ≤ 1
h_tends : Set.Ioi 1 ∈ Filter.map (fun n => r ^ n) atTop
⊢ False

Tactic:
simp only [Filter.mem_map, mem_atTop_sets, ge_iff_le, Set.mem_preimage, Set.mem_Ioi] at h_tends

Result:
case refine_1
r : ℝ≥0∞
r_le_one : r ≤ 1
h_tends : ∃ a, ∀ (b : ℕ), a ≤ b → 1 < r ^ b
⊢ False

Proof state:
case refine_2
r : ℝ≥0∞
r_gt_one : 1 < r
obs : Tendsto (fun n => r⁻¹ ^ n) atTop (𝓝 0) → Tendsto (fun x => (r⁻¹ ^ x)⁻¹) atTop (𝓝 0⁻¹)
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 ⊤)

Tactic:
simp only [ENNReal.tendsto_pow_atTop_nhds_zero_iff, inv_zero] at obs

Result:
case refine_2
r : ℝ≥0∞
r_gt_one : 1 < r
obs : r⁻¹ < 1 → Tendsto (fun x => (r⁻¹ ^ x)⁻¹) atTop (𝓝 ⊤)
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 ⊤)

Proof state:
case refine_2
r : ℝ≥0∞
⊢ 1 < r → Tendsto (fun n => r ^ n) atTop (𝓝 ⊤)

Tactic:
intro r_gt_one

Result:
case refine_2
r : ℝ≥0∞
r_gt_one : 1 < r
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 ⊤)

Proof state:
case refine_2
r : ℝ≥0∞
r_gt_one : 1 < r
obs : r⁻¹ < 1 → Tendsto (fun x => (r⁻¹ ^ x)⁻¹) atTop (𝓝 ⊤)
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 ⊤)

Tactic:
simpa [← ENNReal.inv_pow] using obs <| ENNReal.inv_lt_one.mpr r_gt_one

Result:
no goals

Proof state:
r : ℝ≥0∞
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 ⊤) ↔ 1 < r

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
r : ℝ≥0∞
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 ⊤) → 1 < r

case refine_2
r : ℝ≥0∞
⊢ 1 < r → Tendsto (fun n => r ^ n) atTop (𝓝 ⊤)

Proof state:
case refine_1
r : ℝ≥0∞
⊢ r ≤ 1 → ¬Tendsto (fun n => r ^ n) atTop (𝓝 ⊤)

Tactic:
intro r_le_one h_tends

Result:
case refine_1
r : ℝ≥0∞
r_le_one : r ≤ 1
h_tends : Tendsto (fun n => r ^ n) atTop (𝓝 ⊤)
⊢ False
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_smul_nonzero {x : F} (hx : x ≠ 0) :
    (x • f).natSepDegree = f.natSepDegree

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
x : F
hx : x ≠ 0
⊢ (x • f).natSepDegree = f.natSepDegree

Tactic:
simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_smul_nonzero _ hx]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
x : F
hx : x ≠ 0
⊢ (x • f).natSepDegree = f.natSepDegree

Tactic:
classical
simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_smul_nonzero _ hx]

Result:
no goals
-- Mathlib/Algebra/BigOperators/WithTop.lean
/-- A sum is finite iff all terms are finite. -/
@[simp] lemma sum_lt_top : ∑ i ∈ s, f i < ⊤ ↔ ∀ i ∈ s, f i < ⊤

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : AddCommMonoid α
s : Finset ι
f : ι → WithTop α
inst✝ : LT α
⊢ ∑ i ∈ s, f i < ⊤ ↔ ∀ i ∈ s, f i < ⊤

Tactic:
simp [WithTop.lt_top_iff_ne_top]

Result:
no goals
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem sub (hf : UnifIntegrable f p μ) (hg : UnifIntegrable g p μ) (hp : 1 ≤ p)
    (hf_meas : ∀ i, AEStronglyMeasurable (f i) μ) (hg_meas : ∀ i, AEStronglyMeasurable (g i) μ) :
    UnifIntegrable (f - g) p μ

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
⊢ UnifIntegrable (f + -g) p μ

Tactic:
exact hf.add hg.neg hp hf_meas fun i => (hg_meas i).neg

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
⊢ UnifIntegrable (f - g) p μ

Tactic:
rw [sub_eq_add_neg]

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
⊢ UnifIntegrable (f + -g) p μ
-- Mathlib/Algebra/Lie/Submodule.lean
lemma isCompactElement_lieSpan_singleton (m : M) :
    CompleteLattice.IsCompactElement (lieSpan R L {m})

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : m ∈ ↑(sSup s)
this : ↑(sSup s) = ⋃ N ∈ s, ↑N
⊢ ?m.340010

Tactic:
simp_rw [this, Set.mem_iUnion, SetLike.mem_coe, exists_prop] at hsup

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
m : M
s : Set (LieSubmodule R L M)
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup✝ : m ∈ ↑(sSup s)
this : ↑(sSup s) = ⋃ N ∈ s, ↑N
hsup : ∃ i ∈ s, m ∈ i
⊢ ?m.340010
-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
theorem ofTensorProduct_bijective_of_finite_of_isNoetherian
    [Module.Finite R M] :
    Function.Bijective (ofTensorProduct I M)

Proof state:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
⊢ Function.Bijective ⇑(ofTensorProduct I M)

Tactic:
obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M

Result:
case intro.intro
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective ⇑f
⊢ Function.Bijective ⇑(ofTensorProduct I M)

Proof state:
case intro.intro
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf : Function.Surjective ⇑f
⊢ Function.Bijective ⇑(ofTensorProduct I M)

Tactic:
exact ofTensorProduct_bijective_of_map_from_fin I M f hf

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem _root_.Acc.of_fibration (fib : Fibration rα rβ f) {a} (ha : Acc rα a) : Acc rβ (f a)

Proof state:
case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
b : β
hr : rβ b (f a)
⊢ Acc rβ b

Tactic:
obtain ⟨a', hr', rfl⟩ := fib hr

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
a' : α
hr' : rα a' a
hr : rβ (f a') (f a)
⊢ Acc rβ (f a')

Proof state:
case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
⊢ Acc rβ (f a)

Tactic:
refine Acc.intro (f a) fun b hr ↦ ?_

Result:
case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
b : β
hr : rβ b (f a)
⊢ Acc rβ b

Proof state:
case intro.intro.intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
a' : α
hr' : rα a' a
hr : rβ (f a') (f a)
⊢ Acc rβ (f a')

Tactic:
exact ih a' hr'

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a : α
ha : Acc rα a
⊢ Acc rβ (f a)

Tactic:
induction ha with | intro a _ ih => ?_

Result:
case intro
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
f : α → β
fib : Fibration rα rβ f
a✝ a : α
h✝ : ∀ (y : α), rα y a → Acc rα y
ih : ∀ (y : α), rα y a → Acc rβ (f y)
⊢ Acc rβ (f a)
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem add_le_max (a b : Cardinal) : a + b ≤ max (max a b) ℵ₀

Proof state:
case inl
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ a + b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
rw [add_eq_max ha]

Result:
case inl
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ a ⊔ b ≤ a ⊔ b ⊔ ℵ₀

Proof state:
a b : Cardinal.{u_1}
⊢ a + b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
rcases le_or_lt ℵ₀ a with ha | ha

Result:
case inl
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ a + b ≤ a ⊔ b ⊔ ℵ₀

case inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
⊢ a + b ≤ a ⊔ b ⊔ ℵ₀

Proof state:
case inr.inl
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a ⊔ b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
exact le_max_left _ _

Result:
no goals

Proof state:
case inr.inl
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a + b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
rw [add_comm, add_eq_max hb, max_comm]

Result:
case inr.inl
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a ⊔ b ≤ a ⊔ b ⊔ ℵ₀

Proof state:
case inl
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
⊢ a ⊔ b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
exact le_max_left _ _

Result:
no goals

Proof state:
case inr.inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a + b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
exact le_max_of_le_right (add_lt_aleph0 ha hb).le

Result:
no goals

Proof state:
case inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
⊢ a + b ≤ a ⊔ b ⊔ ℵ₀

Tactic:
rcases le_or_lt ℵ₀ b with hb | hb

Result:
case inr.inl
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a + b ≤ a ⊔ b ⊔ ℵ₀

case inr.inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a + b ≤ a ⊔ b ⊔ ℵ₀
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem MemLp.im (hf : MemLp f p μ) : MemLp (fun x => RCLike.im (f x)) p μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), ‖RCLike.im (f x)‖ ≤ 1 * ‖f x‖
⊢ MemLp (fun x => RCLike.im (f x)) p μ

Tactic:
refine hf.of_le_mul ?_ (Eventually.of_forall this)

Result:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), ‖RCLike.im (f x)‖ ≤ 1 * ‖f x‖
⊢ AEStronglyMeasurable (fun x => RCLike.im (f x)) μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), ‖RCLike.im (f x)‖ ≤ 1 * ‖f x‖
⊢ AEStronglyMeasurable (fun x => RCLike.im (f x)) μ

Tactic:
exact RCLike.continuous_im.comp_aestronglyMeasurable hf.1

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
⊢ MemLp (fun x => RCLike.im (f x)) p μ

Tactic:
have : ∀ x, ‖RCLike.im (f x)‖ ≤ 1 * ‖f x‖ := by
  intro x
  rw [one_mul]
  exact RCLike.norm_im_le_norm (f x)

Result:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
this : ∀ (x : α), ‖RCLike.im (f x)‖ ≤ 1 * ‖f x‖
⊢ MemLp (fun x => RCLike.im (f x)) p μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ ‖RCLike.im (f x)‖ ≤ ‖f x‖

Tactic:
exact RCLike.norm_im_le_norm (f x)

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ ‖RCLike.im (f x)‖ ≤ 1 * ‖f x‖

Tactic:
rw [one_mul]

Result:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ ‖RCLike.im (f x)‖ ≤ ‖f x‖

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
⊢ ∀ (x : α), ‖RCLike.im (f x)‖ ≤ 1 * ‖f x‖

Tactic:
intro x

Result:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f p μ
x : α
⊢ ‖RCLike.im (f x)‖ ≤ 1 * ‖f x‖
-- Mathlib/Topology/Bornology/Absorbs.lean
lemma _root_.Set.Finite.absorbs_sUnion {T : Set (Set α)} (hT : T.Finite) :
    Absorbs M s (⋃₀ T) ↔ ∀ t ∈ T, Absorbs M s t

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s : Set α
T : Set (Set α)
hT : T.Finite
⊢ Absorbs M s (⋃₀ T) ↔ ∀ t ∈ T, Absorbs M s t

Tactic:
simp [Absorbs, hT]

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem transpose_transpose (μ : YoungDiagram) : μ.transpose.transpose = μ

Proof state:
μ : YoungDiagram
⊢ μ.transpose.transpose = μ

Tactic:
ext x

Result:
case cells.h
μ : YoungDiagram
x : ℕ × ℕ
⊢ x ∈ μ.transpose.transpose.cells ↔ x ∈ μ.cells

Proof state:
case cells.h
μ : YoungDiagram
x : ℕ × ℕ
⊢ x ∈ μ.transpose.transpose.cells ↔ x ∈ μ.cells

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Smooth/Basic.lean
theorem localization_base [FormallySmooth R Sₘ] : FormallySmooth Rₘ Sₘ

Proof state:
case comp_surjective
R Rₘ Sₘ : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₘ
inst✝⁸ : CommRing Sₘ
M : Submonoid R
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
⊢ ∃ a, (Ideal.Quotient.mkₐ Rₘ I).comp a = f

Tactic:
let f : Sₘ →ₐ[Rₘ] Q := by
  refine { FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) with commutes' := ?_ }
  intro r
  change
    (RingHom.comp (FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) : Sₘ →+* Q)
          (algebraMap _ _))
        r =
      algebraMap _ _ r
  congr 1
  refine IsLocalization.ringHom_ext M ?_
  rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq,
    AlgHom.comp_algebraMap]

Result:
case comp_surjective
R Rₘ Sₘ : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing Rₘ
inst✝⁸ : CommRing Sₘ
M : Submonoid R
inst✝⁷ : Algebra R Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsLocalization M Rₘ
inst✝² : FormallySmooth R Sₘ
Q : Type u
inst✝¹ : CommRing Q
inst✝ : Algebra Rₘ Q
I : Ideal Q
e : I ^ 2 = ⊥
f✝ : Sₘ →ₐ[Rₘ] Q ⧸ I
this✝ : Algebra R Q := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
this : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
f : Sₘ →ₐ[Rₘ] Q :=
  let __src := lift I ⋯ (AlgHom.restrictScalars R f✝);
  { toRingHom := __src.toRingHom, commutes' := ⋯ }
⊢ ∃ a, (Ideal.Quotient.mkₐ Rₘ I).comp a = f✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_one_eq_ofBool_getLsb_zero (x : BitVec w) :
    x.setWidth 1 = BitVec.ofBool (x.getLsbD 0)

Proof state:
w : Nat
x : BitVec w
⊢ setWidth 1 x = ofBool (x.getLsbD 0)

Tactic:
ext i h

Result:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < 1
⊢ (setWidth 1 x).getLsbD i = (ofBool (x.getLsbD 0)).getLsbD i

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
h : i = 0
⊢ (setWidth 1 x).getLsbD i = (ofBool (x.getLsbD 0)).getLsbD i

Tactic:
simp [getLsbD_setWidth, h]

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < 1
⊢ (setWidth 1 x).getLsbD i = (ofBool (x.getLsbD 0)).getLsbD i

Tactic:
simp at h

Result:
case pred
w : Nat
x : BitVec w
i : Nat
h : i = 0
⊢ (setWidth 1 x).getLsbD i = (ofBool (x.getLsbD 0)).getLsbD i
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_mul_right : ∑' i, f i * a = (∑' i, f i) * a

Proof state:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
⊢ ∑' (i : α), f i * a = (∑' (i : α), f i) * a

Tactic:
simp [mul_comm, ENNReal.tsum_mul_left]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem span_le_degreeLE_of_finite {s : Set R[X]} (s_fin : s.Finite) :
    ∃ n : ℕ, Submodule.span R s ≤ degreeLE R n

Proof state:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s = ∅
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Tactic:
rw [s_emp, Submodule.span_empty]

Result:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s = ∅
⊢ ∃ n, ⊥ ≤ degreeLE R ↑n

Proof state:
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Tactic:
by_cases s_emp : s.Nonempty

Result:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : ¬s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Proof state:
case pos.intro.intro
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s.Nonempty
p' : R[X]
left✝ : p' ∈ s
hp'max : ∀ p ∈ Submodule.span R s, p.degree ≤ p'.degree
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Tactic:
exact ⟨natDegree p', fun p hp => mem_degreeLE.mpr ((hp'max _ hp).trans degree_le_natDegree)⟩

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Tactic:
rcases exists_degree_le_of_mem_span_of_finite s_fin s_emp with ⟨p', _, hp'max⟩

Result:
case pos.intro.intro
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s.Nonempty
p' : R[X]
left✝ : p' ∈ s
hp'max : ∀ p ∈ Submodule.span R s, p.degree ≤ p'.degree
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Proof state:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s = ∅
⊢ ∃ n, ⊥ ≤ degreeLE R ↑n

Tactic:
exact ⟨0, bot_le⟩

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : ¬s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Tactic:
rw [Set.not_nonempty_iff_eq_empty] at s_emp

Result:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s = ∅
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem foldlM_subtype [Monad m] {p : α → Prop} {l : Array { x // p x }}
    {f : β → { x // p x } → m β} {g : β → α → m β} {x : β}
    (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) (w : stop = l.size) :
    l.foldlM f x 0 stop = l.unattach.foldlM g x 0 stop

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
stop : Nat
inst✝ : Monad m
p : α → Prop
l : Array { x // p x }
f : β → { x // p x } → m β
g : β → α → m β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
w : stop = l.size
⊢ foldlM f x l 0 stop = foldlM g x l.unattach 0 stop

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
p : α → Prop
l : Array { x // p x }
f : β → { x // p x } → m β
g : β → α → m β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
⊢ foldlM f x l = foldlM g x l.unattach 0 l.size

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
p : α → Prop
l : Array { x // p x }
f : β → { x // p x } → m β
g : β → α → m β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
⊢ foldlM f x l = foldlM g x l.unattach 0 l.size

Tactic:
rcases l with ⟨l⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
p : α → Prop
f : β → { x // p x } → m β
g : β → α → m β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
l : List { x // p x }
⊢ foldlM f x { toList := l } = foldlM g x { toList := l }.unattach 0 { toList := l }.size

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
p : α → Prop
f : β → { x // p x } → m β
g : β → α → m β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
l : List { x // p x }
⊢ foldlM f x { toList := l } = foldlM g x { toList := l }.unattach 0 { toList := l }.size

Tactic:
simp

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
p : α → Prop
f : β → { x // p x } → m β
g : β → α → m β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
l : List { x // p x }
⊢ List.foldlM (fun x y => f x y) x l = List.foldlM (fun x y => g x y) x l.unattach

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
p : α → Prop
f : β → { x // p x } → m β
g : β → α → m β
x : β
hf : ∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x
l : List { x // p x }
⊢ List.foldlM (fun x y => f x y) x l = List.foldlM (fun x y => g x y) x l.unattach

Tactic:
rw [List.foldlM_subtype hf]

Result:
no goals
-- Mathlib/Order/WellFounded.lean
theorem lt_succ {r : α → α → Prop} (wf : WellFounded r) {x : α} (h : ∃ y, r x y) :
    r x (wf.succ x)

Proof state:
α : Type u_1
r : α → α → Prop
wf : WellFounded r
x : α
h : ∃ y, r x y
⊢ r x (wf.succ x)

Tactic:
rw [WellFounded.succ, dif_pos h]

Result:
α : Type u_1
r : α → α → Prop
wf : WellFounded r
x : α
h : ∃ y, r x y
⊢ r x (wf.min {y | r x y} h)

Proof state:
α : Type u_1
r : α → α → Prop
wf : WellFounded r
x : α
h : ∃ y, r x y
⊢ r x (wf.min {y | r x y} h)

Tactic:
apply min_mem

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Basic.lean
@[to_additive]
lemma MonoidHom.tendsto_coe_cofinite_of_discrete [T2Space G] {H : Type*} [Group H] {f : H →* G}
    (hf : Function.Injective f) (hf' : DiscreteTopology f.range) :
    Tendsto f cofinite (cocompact _)

Proof state:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Type u_2
inst✝ : Group H
f : H →* G
hf : Function.Injective ⇑f
hf' : DiscreteTopology ↥f.range
⊢ Function.Injective ⇑f.rangeRestrict

Tactic:
simpa

Result:
no goals

Proof state:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Type u_2
inst✝ : Group H
f : H →* G
hf : Function.Injective ⇑f
hf' : DiscreteTopology ↥f.range
⊢ Tendsto (⇑f) cofinite (cocompact G)

Tactic:
replace hf : Function.Injective f.rangeRestrict := by simpa

Result:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Type u_2
inst✝ : Group H
f : H →* G
hf' : DiscreteTopology ↥f.range
hf : Function.Injective ⇑f.rangeRestrict
⊢ Tendsto (⇑f) cofinite (cocompact G)

Proof state:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Type u_2
inst✝ : Group H
f : H →* G
hf' : DiscreteTopology ↥f.range
hf : Function.Injective ⇑f.rangeRestrict
⊢ Tendsto (⇑f) cofinite (cocompact G)

Tactic:
exact f.range.tendsto_coe_cofinite_of_discrete.comp hf.tendsto_cofinite

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem functorPullback_id (R : Sieve X) : R.functorPullback (𝟭 _) = R

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Sieve X
⊢ functorPullback (𝟭 C) R = R

Tactic:
ext

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (functorPullback (𝟭 C) R).arrows f✝ ↔ R.arrows f✝

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (functorPullback (𝟭 C) R).arrows f✝ ↔ R.arrows f✝

Tactic:
rfl

Result:
no goals