harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem norm_setToSimpleFunc_le_sum_mul_norm (T : Set α → F →L[ℝ] F') {C : ℝ}
    (hT_norm : ∀ s, MeasurableSet s → ‖T s‖ ≤ C * (μ s).toReal) (f : α →ₛ F) :
    ‖f.setToSimpleFunc T‖ ≤ C * ∑ x ∈ f.range, (μ (f ⁻¹' {x})).toReal * ‖x‖ :=
  calc
    ‖f.setToSimpleFunc T‖ ≤ ∑ x ∈ f.range, ‖T (f ⁻¹' {x})‖ * ‖x‖ :=
      norm_setToSimpleFunc_le_sum_opNorm T f
    _ ≤ ∑ x ∈ f.range, C * (μ (f ⁻¹' {x})).toReal * ‖x‖

Proof state:
case h.h
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * (μ s).toReal
f : α →ₛ F
i✝ : F
a✝ : i✝ ∈ f.range
⊢ ‖T (⇑f ⁻¹' {i✝})‖ ≤ C * (μ (⇑f ⁻¹' {i✝})).toReal

Tactic:
exact hT_norm _ <| SimpleFunc.measurableSet_fiber _ _

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * (μ s).toReal
f : α →ₛ F
⊢ ∑ x ∈ f.range, ‖T (⇑f ⁻¹' {x})‖ * ‖x‖ ≤ ∑ x ∈ f.range, C * (μ (⇑f ⁻¹' {x})).toReal * ‖x‖

Tactic:
gcongr

Result:
case h.h
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * (μ s).toReal
f : α →ₛ F
i✝ : F
a✝ : i✝ ∈ f.range
⊢ ‖T (⇑f ⁻¹' {i✝})‖ ≤ C * (μ (⇑f ⁻¹' {i✝})).toReal

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * (μ s).toReal
f : α →ₛ F
⊢ ∑ x ∈ f.range, C * (μ (⇑f ⁻¹' {x})).toReal * ‖x‖ ≤ C * ∑ x ∈ f.range, (μ (⇑f ⁻¹' {x})).toReal * ‖x‖

Tactic:
simp_rw [mul_sum, ← mul_assoc]

Result:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * (μ s).toReal
f : α →ₛ F
⊢ ∑ x ∈ f.range, C * (μ (⇑f ⁻¹' {x})).toReal * ‖x‖ ≤ ∑ x ∈ f.range, C * (μ (⇑f ⁻¹' {x})).toReal * ‖x‖

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
C : ℝ
hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * (μ s).toReal
f : α →ₛ F
⊢ ∑ x ∈ f.range, C * (μ (⇑f ⁻¹' {x})).toReal * ‖x‖ ≤ ∑ x ∈ f.range, C * (μ (⇑f ⁻¹' {x})).toReal * ‖x‖

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Reflection.lean
lemma involutive_preReflection (h : f x = 2) :
    Involutive (preReflection x f) :=
  fun y ↦ by simp [map_sub, h, smul_sub, two_smul, preReflection_apply]

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
f : Dual R M
h : f x = 2
y : M
⊢ (preReflection x f) ((preReflection x f) y) = y

Tactic:
simp [map_sub, h, smul_sub, two_smul, preReflection_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem setAverage_eq' (f : α → E) (s : Set α) :
    ⨍ x in s, f x ∂μ = ∫ x, f x ∂(μ s)⁻¹ • μ.restrict s

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f : α → E
s : Set α
⊢ ⨍ (x : α) in s, f x ∂μ = ∫ (x : α), f x ∂(μ s)⁻¹ • μ.restrict s

Tactic:
simp only [average_eq', restrict_apply_univ]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem toFinset_replicate_of_ne_zero {n : ℕ} (hn : n ≠ 0) :
    (List.replicate n a).toFinset = {a}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
hn : n ≠ 0
⊢ (replicate n a).toFinset = {a}

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
hn : n ≠ 0
x : α
⊢ x ∈ (replicate n a).toFinset ↔ x ∈ {a}

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
hn : n ≠ 0
x : α
⊢ x ∈ (replicate n a).toFinset ↔ x ∈ {a}

Tactic:
simp [hn, List.mem_replicate]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem destruct_join (S : WSeq (WSeq α)) :
    destruct (join S) = (destruct S).bind destruct_join.aux

Proof state:
α : Type u
S✝ : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
S : WSeq (WSeq α)
⊢ Computation.BisimO (fun c1 c2 => c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    S.join.destruct.destruct (S.destruct.bind destruct_join.aux).destruct

Tactic:
induction' S using WSeq.recOn with s S S <;> simp

Result:
case h3
α : Type u
S✝ : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
S : WSeq (WSeq α)
⊢ S.join.destruct = S.destruct.bind destruct_join.aux ∨
    ∃ S_1, S.join.destruct = S_1.join.destruct ∧ S.destruct.bind destruct_join.aux = S_1.destruct.bind destruct_join.aux

Proof state:
α : Type u
S : WSeq (WSeq α)
⊢ Computation.IsBisimulation fun c1 c2 => c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux

Tactic:
intro c1 c2 h

Result:
α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
⊢ Computation.BisimO (fun c1 c2 => c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    c1.destruct c2.destruct

Proof state:
α : Type u
S : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
c : Computation (Option (α × WSeq α))
⊢ Computation.BisimO (fun c1 c2 => c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux)
    c.destruct c.destruct

Tactic:
cases c.destruct <;> simp

Result:
no goals

Proof state:
α : Type u
S : WSeq (WSeq α)
⊢ S.join.destruct = S.destruct.bind destruct_join.aux

Tactic:
apply
  Computation.eq_of_bisim
    (fun c1 c2 =>
      c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = (destruct S).bind destruct_join.aux)
    _ (Or.inr ⟨S, rfl, rfl⟩)

Result:
α : Type u
S : WSeq (WSeq α)
⊢ Computation.IsBisimulation fun c1 c2 => c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux

Proof state:
case h3
α : Type u
S✝ : WSeq (WSeq α)
c1 c2 : Computation (Option (α × WSeq α))
h : c1 = c2 ∨ ∃ S, c1 = S.join.destruct ∧ c2 = S.destruct.bind destruct_join.aux
S : WSeq (WSeq α)
⊢ S.join.destruct = S.destruct.bind destruct_join.aux ∨
    ∃ S_1, S.join.destruct = S_1.join.destruct ∧ S.destruct.bind destruct_join.aux = S_1.destruct.bind destruct_join.aux

Tactic:
refine Or.inr ⟨S, rfl, rfl⟩

Result:
no goals
-- Mathlib/MeasureTheory/Group/Measure.lean
@[to_additive]
lemma _root_.MeasurableSet.mul_closure_one_eq {s : Set G} (hs : MeasurableSet s) :
    s * (closure {1} : Set G) = s

Proof state:
case compl
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
ht✝ : MeasurableSet t
iht : t * closure {1} = t
⊢ tᶜ * closure {1} = tᶜ

Tactic:
exact compl_mul_closure_one_eq_iff.2 iht

Result:
no goals

Proof state:
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : MeasurableSet s
⊢ s * closure {1} = s

Tactic:
induction s, hs using MeasurableSet.induction_on_open with
| isOpen U hU => exact hU.mul_closure_one_eq
| compl t _ iht => exact compl_mul_closure_one_eq_iff.2 iht
| iUnion f _ _ ihf => simp_rw [iUnion_mul f, ihf]

Result:
no goals

Proof state:
case iUnion
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
f : ℕ → Set G
a✝ : Pairwise (Disjoint on f)
hf✝ : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), f i * closure {1} = f i
⊢ (⋃ i, f i) * closure {1} = ⋃ i, f i

Tactic:
simp_rw [iUnion_mul f, ihf]

Result:
no goals

Proof state:
case isOpen
G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s U : Set G
hU : IsOpen U
⊢ U * closure {1} = U

Tactic:
exact hU.mul_closure_one_eq

Result:
no goals
-- Mathlib/Topology/LocallyConstant/Basic.lean
@[simp]
lemma piecewise_apply_left {C₁ C₂ : Set X} (h₁ : IsClosed C₁) (h₂ : IsClosed C₂)
    (h : C₁ ∪ C₂ = Set.univ) (f : LocallyConstant C₁ Z) (g : LocallyConstant C₂ Z)
    (hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, hx.1⟩ = g ⟨x, hx.2⟩)
    [DecidablePred (· ∈ C₁)] (x : X) (hx : x ∈ C₁) :
    piecewise h₁ h₂ h f g hfg x = f ⟨x, hx⟩

Proof state:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x => x ∈ C₁
x : X
hx : x ∈ C₁
⊢ (piecewise h₁ h₂ h f g hfg) x = f ⟨x, hx⟩

Tactic:
simp only [piecewise, Set.mem_preimage, continuous_subtype_val.restrictPreimage,
  coe_comap, Function.comp_apply, coe_mk]

Result:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x => x ∈ C₁
x : X
hx : x ∈ C₁
⊢ (if hi : x ∈ C₁ then f ⟨x, hi⟩ else g ⟨x, ⋯⟩) = f ⟨x, hx⟩

Proof state:
X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed C₁
h₂ : IsClosed C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x => x ∈ C₁
x : X
hx : x ∈ C₁
⊢ (if hi : x ∈ C₁ then f ⟨x, hi⟩ else g ⟨x, ⋯⟩) = f ⟨x, hx⟩

Tactic:
rw [dif_pos hx]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
/-- Boundaryless manifolds have empty boundary. -/
lemma Boundaryless.boundary_eq_empty [BoundarylessManifold I M] : I.boundary M = ∅

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : BoundarylessManifold I M
⊢ ModelWithCorners.boundary M = ∅

Tactic:
rw [← I.compl_interior, I.interior_eq_univ, compl_empty_iff]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem coe_ne_zero {f : Polynomial F} (hf : f ≠ 0) : (↑f : F⟦X⟧) ≠ 0

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hf : f ≠ 0
⊢ ↑f ≠ 0

Tactic:
simp only [ne_eq, Polynomial.coe_eq_zero_iff, hf, not_false_eq_true]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem differentiable_neg_iff : (Differentiable 𝕜 fun y => -f y) ↔ Differentiable 𝕜 f :=
  ⟨fun h => by simpa only [neg_neg] using h.neg, fun h => h.neg⟩

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
h : Differentiable 𝕜 fun y => -f y
⊢ Differentiable 𝕜 f

Tactic:
simpa only [neg_neg] using h.neg

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem clog_eq_one {b n : ℕ} (hn : 2 ≤ n) (h : n ≤ b) : clog b n = 1

Proof state:
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ (n + b - 1) / b ≤ 1

Tactic:
rw [← Nat.lt_succ_iff, Nat.div_lt_iff_lt_mul] <;> omega

Result:
no goals

Proof state:
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ clog b n = 1

Tactic:
rw [clog_of_two_le (hn.trans h) hn, clog_of_right_le_one]

Result:
case hn
b n : ℕ
hn : 2 ≤ n
h : n ≤ b
⊢ (n + b - 1) / b ≤ 1
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem one_lt_of_lt_mul_left [MulRightReflectLT α] {a b : α}
    (h : b < a * b) :
    1 < a :=
  lt_of_mul_lt_mul_right' (a := b) <| by simpa only [one_mul]

Proof state:
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : MulRightReflectLT α
a b : α
h : b < a * b
⊢ 1 * b < a * b

Tactic:
simpa only [one_mul]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem mem_degrees {p : MvPolynomial σ R} {i : σ} :
    i ∈ p.degrees ↔ ∃ d, p.coeff d ≠ 0 ∧ i ∈ d.support

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
⊢ i ∈ p.degrees ↔ ∃ d, coeff d p ≠ 0 ∧ i ∈ d.support

Tactic:
classical
simp only [degrees_def, Multiset.mem_sup, ← mem_support_iff, Finsupp.mem_toMultiset, exists_prop]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
⊢ i ∈ p.degrees ↔ ∃ d, coeff d p ≠ 0 ∧ i ∈ d.support

Tactic:
simp only [degrees_def, Multiset.mem_sup, ← mem_support_iff, Finsupp.mem_toMultiset, exists_prop]

Result:
no goals
-- Mathlib/RingTheory/Regular/RegularSequence.lean
lemma eq_nil_of_isRegular_on_artinian [IsArtinian R M] :
    {rs : List R} → IsRegular M rs → rs = []
  | [], _ => rfl
  | r :: rs, h => by
    rw [isRegular_iff, ne_comm, ← lt_top_iff_ne_top, Ideal.ofList_cons,
      sup_smul, ideal_span_singleton_smul, isWeaklyRegular_cons_iff] at h
    refine absurd ?_ (ne_of_lt (lt_of_le_of_lt le_sup_left h.right))
    exact Eq.trans (Submodule.map_top _) <| LinearMap.range_eq_top.mpr <|
      surjective_of_injective_endomorphism (LinearMap.lsmul R M r) h.left.left

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs) ∧ r • ⊤ ⊔ Ideal.ofList rs • ⊤ < ⊤
⊢ r :: rs = []

Tactic:
refine absurd ?_ (ne_of_lt (lt_of_le_of_lt le_sup_left h.right))

Result:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs) ∧ r • ⊤ ⊔ Ideal.ofList rs • ⊤ < ⊤
⊢ r • ⊤ = ⊤

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs) ∧ r • ⊤ ⊔ Ideal.ofList rs • ⊤ < ⊤
⊢ r • ⊤ = ⊤

Tactic:
exact Eq.trans (Submodule.map_top _) <| LinearMap.range_eq_top.mpr <|
  surjective_of_injective_endomorphism (LinearMap.lsmul R M r) h.left.left

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : IsRegular M (r :: rs)
⊢ r :: rs = []

Tactic:
rw [isRegular_iff, ne_comm, ← lt_top_iff_ne_top, Ideal.ofList_cons,
  sup_smul, ideal_span_singleton_smul, isWeaklyRegular_cons_iff] at h

Result:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsArtinian R M
r : R
rs : List R
h : (IsSMulRegular M r ∧ IsWeaklyRegular (QuotSMulTop r M) rs) ∧ r • ⊤ ⊔ Ideal.ofList rs • ⊤ < ⊤
⊢ r :: rs = []
-- Mathlib/CategoryTheory/Abelian/Basic.lean
theorem epi_fst_of_isLimit [Epi g] {s : PullbackCone f g} (hs : IsLimit s) : Epi s.fst

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
s : PullbackCone f g
hs : IsLimit s
⊢ Epi s.fst

Tactic:
haveI : Epi (NatTrans.app (limit.cone (cospan f g)).π WalkingCospan.left) :=
  Abelian.epi_pullback_of_epi_g f g

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
s : PullbackCone f g
hs : IsLimit s
this : Epi ((limit.cone (cospan f g)).π.app WalkingCospan.left)
⊢ Epi s.fst

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
s : PullbackCone f g
hs : IsLimit s
this : Epi ((limit.cone (cospan f g)).π.app WalkingCospan.left)
⊢ Epi s.fst

Tactic:
apply epi_of_epi_fac (IsLimit.conePointUniqueUpToIso_hom_comp (limit.isLimit _) hs _)

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma smul_finset_univ₀ [Fintype β] (ha : a ≠ 0) : a • (univ : Finset β) = univ :=
  coe_injective <| by push_cast; exact Set.smul_set_univ₀ ha

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
a : α
inst✝ : Fintype β
ha : a ≠ 0
⊢ ↑(a • univ) = ↑univ

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
a : α
inst✝ : Fintype β
ha : a ≠ 0
⊢ a • Set.univ = Set.univ

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
a : α
inst✝ : Fintype β
ha : a ≠ 0
⊢ a • Set.univ = Set.univ

Tactic:
exact Set.smul_set_univ₀ ha

Result:
no goals
-- Mathlib/Data/Part.lean
theorem assert_neg {p : Prop} {f : p → Part α} (h : ¬p) : assert p f = none

Proof state:
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ { Dom := ∃ (h : p), (f h).Dom, get := fun ha => (f ⋯).get ⋯ } =
    { Dom := False, get := fun t => False.rec (fun x => α) t }

Tactic:
congr

Result:
case h.e_2
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ (∃ (h : p), (f h).Dom) = False

case h.e_3
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ HEq (fun ha => (f ⋯).get ⋯) fun t => False.rec (fun x => α) t

Proof state:
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ assert p f = none

Tactic:
dsimp [assert, none]

Result:
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ { Dom := ∃ (h : p), (f h).Dom, get := fun ha => (f ⋯).get ⋯ } =
    { Dom := False, get := fun t => False.rec (fun x => α) t }

Proof state:
case h.e_2
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ (∃ (h : p), (f h).Dom) = False

Tactic:
simp only [h, not_false_iff, exists_prop_of_false]

Result:
no goals

Proof state:
case h.e_3.h
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ ∀ (a : ∃ (h : p), (f h).Dom) (a' : False), HEq a a' → HEq ((f ⋯).get ⋯) (False.rec (fun x => α) a')

Tactic:
simp at *

Result:
no goals

Proof state:
case h.e_3
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ HEq (fun ha => (f ⋯).get ⋯) fun t => False.rec (fun x => α) t

Tactic:
apply Function.hfunext

Result:
case h.e_3.hα
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ (∃ (h : p), (f h).Dom) = False

case h.e_3.h
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ ∀ (a : ∃ (h : p), (f h).Dom) (a' : False), HEq a a' → HEq ((f ⋯).get ⋯) (False.rec (fun x => α) a')

Proof state:
case h.e_3.hα
α : Type u_1
p : Prop
f : p → Part α
h : ¬p
⊢ (∃ (h : p), (f h).Dom) = False

Tactic:
simp only [h, not_false_iff, exists_prop_of_false]

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
lemma testTrueHelper (p : ℕ) (hp : Nat.blt 1 p = true) (h : sModNatTR (2 ^ p - 1) (p - 2) = 0) :
    LucasLehmerTest p

Proof state:
p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) = 0
⊢ LucasLehmerTest p

Tactic:
rw [LucasLehmerTest, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero p hp, ← sModNat_eq_sMod p _ hp,
  ← sModNatTR_eq_sModNat, h]

Result:
p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) = 0
⊢ ↑0 = 0

Proof state:
p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) = 0
⊢ ↑0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
p : ℕ
hp : Nat.blt 1 p = true
h : sModNatTR (2 ^ p - 1) (p - 2) = 0
⊢ LucasLehmerTest p

Tactic:
rw [Nat.blt_eq] at hp

Result:
p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) = 0
⊢ LucasLehmerTest p
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem iff_id_eq_zero (X : C) : IsZero X ↔ 𝟙 X = 0 :=
  ⟨fun h => h.eq_of_src _ _, fun h =>
    ⟨fun Y => ⟨⟨⟨0⟩, fun f => by
        rw [← id_comp f, ← id_comp (0 : X ⟶ Y), h, zero_comp, zero_comp]; simp only⟩⟩,
    fun Y => ⟨⟨⟨0⟩, fun f => by
        rw [← comp_id f, ← comp_id (0 : Y ⟶ X), h, comp_zero, comp_zero]; simp only ⟩⟩⟩⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : Y ⟶ X
⊢ 0 = default

Tactic:
simp only

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ 0 = default

Tactic:
simp only

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : Y ⟶ X
⊢ f = default

Tactic:
rw [← comp_id f, ← comp_id (0 : Y ⟶ X), h, comp_zero, comp_zero]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : Y ⟶ X
⊢ 0 = default

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ f = default

Tactic:
rw [← id_comp f, ← id_comp (0 : X ⟶ Y), h, zero_comp, zero_comp]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ 0 = default
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem reduce.min (H : Red (reduce L₁) L₂) : reduce L₁ = L₂

Proof state:
case tail
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
L1 L' : List (α × Bool)
L2 : Relation.ReflTransGen Red.Step (reduce L₁) L1
H1 : Red.Step L1 L'
H2 : reduce L₁ = L1
⊢ reduce L₁ = L'

Tactic:
obtain ⟨L4, L5, x, b⟩ := H1

Result:
case tail.not
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
L2 : Relation.ReflTransGen Red.Step (reduce L₁) (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝)
H2 : reduce L₁ = L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
⊢ reduce L₁ = L₁✝ ++ L₂✝

Proof state:
case tail.not
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
L2 : Relation.ReflTransGen Red.Step (reduce L₁) (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝)
H2 : reduce L₁ = L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
⊢ reduce L₁ = L₁✝ ++ L₂✝

Tactic:
exact reduce.not H2

Result:
no goals

Proof state:
case refl
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce L₁ = reduce L₁

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
H : Red (reduce L₁) L₂
⊢ reduce L₁ = L₂

Tactic:
induction' H with L1 L' L2 H1 H2 ih

Result:
case refl
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce L₁ = reduce L₁

case tail
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
L1 L' : List (α × Bool)
L2 : Relation.ReflTransGen Red.Step (reduce L₁) L1
H1 : Red.Step L1 L'
H2 : reduce L₁ = L1
⊢ reduce L₁ = L'
-- Mathlib/Algebra/BigOperators/Ring/Multiset.lean
lemma sum_map_mul_right : sum (s.map fun i ↦ f i * a) = sum (s.map f) * a :=
  Multiset.induction_on s (by simp) fun a s ih => by simp [ih, add_mul]

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
a✝ : α
s✝ : Multiset ι
f : ι → α
a : ι
s : Multiset ι
ih : (map (fun i => f i * a✝) s).sum = (map f s).sum * a✝
⊢ (map (fun i => f i * a✝) (a ::ₘ s)).sum = (map f (a ::ₘ s)).sum * a✝

Tactic:
simp [ih, add_mul]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
a : α
s : Multiset ι
f : ι → α
⊢ (map (fun i => f i * a) 0).sum = (map f 0).sum * a

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Germ/Basic.lean
lemma isConstant_comp_tendsto {lc : Filter γ} {g : γ → α}
    (hf : (f : Germ l β).IsConstant) (hg : Tendsto g lc l) : IsConstant (f ∘ g : Germ lc β)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
lc : Filter γ
g : γ → α
hf : (↑f).IsConstant
hg : Tendsto g lc l
⊢ (↑(f ∘ g)).IsConstant

Tactic:
rcases hf with ⟨b, hb⟩

Result:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
lc : Filter γ
g : γ → α
hg : Tendsto g lc l
b : β
hb : f =ᶠ[l] fun x => b
⊢ (↑(f ∘ g)).IsConstant

Proof state:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
lc : Filter γ
g : γ → α
hg : Tendsto g lc l
b : β
hb : f =ᶠ[l] fun x => b
⊢ (↑(f ∘ g)).IsConstant

Tactic:
exact ⟨b, hb.comp_tendsto hg⟩

Result:
no goals