harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem essSup_measure_zero {m : MeasurableSpace α} {f : α → β} : essSup f (0 : Measure α) = ⊥ :=
  le_bot_iff.mp (sInf_le (by simp [Set.mem_setOf_eq, EventuallyLE, ae_iff]))

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
m : MeasurableSpace α
f : α → β
⊢ ⊥ ∈ {a | ∀ᶠ (n : β) in map f (ae 0), n ≤ a}

Tactic:
simp [Set.mem_setOf_eq, EventuallyLE, ae_iff]

Result:
no goals
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem T_pos : T > 0

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
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 > 0

Tactic:
exact div_pos (norm_pos_iff.2 hnsol) (deriv_sq_norm_pos hnorm)

Result:
no goals

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
hnsol : Polynomial.eval a F ≠ 0
⊢ T_gen p F a > 0

Tactic:
rw [T_def]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2 > 0
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma inl_opProdIsoCoprod_inv : coprod.inl ≫ (opProdIsoCoprod A B).inv = prod.fst.op

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

Tactic:
rw [Iso.comp_inv_eq, fst_opProdIsoCoprod_hom]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
theorem map_id_c_app (F : J ⥤ PresheafedSpace.{_, _, v} C) (j) (U) :
    (F.map (𝟙 j)).c.app U =
      (Pushforward.id (F.obj j).presheaf).inv.app U ≫
        (pushforwardEq (by simp) (F.obj j).presheaf).hom.app U

Proof state:
J : Type u'
inst✝¹ : Category.{v', u'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ PresheafedSpace C
j : J
U : (Opens ↑↑(F.obj j))ᵒᵖ
⊢ 𝟙 ↑(F.obj j) = (F.map (𝟙 j)).base

Tactic:
simp

Result:
no goals

Proof state:
J : Type u'
inst✝¹ : Category.{v', u'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ PresheafedSpace C
j : J
U : (Opens ↑↑(F.obj j))ᵒᵖ
⊢ (F.map (𝟙 j)).c.app U = (Pushforward.id (F.obj j).presheaf).inv.app U ≫ (pushforwardEq ⋯ (F.obj j).presheaf).hom.app U

Tactic:
simp [PresheafedSpace.congr_app (F.map_id j)]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Finite.lean
theorem eq_top_of_card_eq [Finite H] (h : Nat.card H = Nat.card G) : H = ⊤

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↥H
h : Nat.card ↥H = Nat.card G
this : Finite G
⊢ H = ⊤

Tactic:
exact eq_top_of_le_card _ (Nat.le_of_eq h.symm)

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↥H
h : Nat.card ↥H = Nat.card G
⊢ H = ⊤

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero (h ▸ Nat.card_pos.ne')

Result:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↥H
h : Nat.card ↥H = Nat.card G
this : Finite G
⊢ H = ⊤
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem _root_.Submodule.map_comap_eq [RingHomSurjective τ₁₂] (f : F) (q : Submodule R₂ M₂) :
    map f (comap f q) = range f ⊓ q :=
  le_antisymm (le_inf map_le_range (map_comap_le _ _)) <| by
    rintro _ ⟨⟨x, _, rfl⟩, hx⟩; exact ⟨x, hx, rfl⟩

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : F
q : Submodule R₂ M₂
⊢ range f ⊓ q ≤ map f (comap f q)

Tactic:
rintro _ ⟨⟨x, _, rfl⟩, hx⟩

Result:
case intro.intro.refl
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : F
q : Submodule R₂ M₂
x : M
hx : f x ∈ ↑q
⊢ f x ∈ map f (comap f q)

Proof state:
case intro.intro.refl
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : F
q : Submodule R₂ M₂
x : M
hx : f x ∈ ↑q
⊢ f x ∈ map f (comap f q)

Tactic:
exact ⟨x, hx, rfl⟩

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem closure_setOf_im_lt (a : ℝ) : closure { z : ℂ | z.im < a } = { z | z.im ≤ a }

Proof state:
a : ℝ
⊢ closure {z | z.im < a} = {z | z.im ≤ a}

Tactic:
simpa only [closure_Iio] using closure_preimage_im (Iio a)

Result:
no goals
-- Mathlib/Analysis/Analytic/IteratedFDeriv.lean
/-- If the `n`-th term in a power series is zero, then the `n`-th derivative of the corresponding
function vanishes. -/
lemma HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_zero
    (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : AnalyticOn 𝕜 f s)
    (hu : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ} (hn : p n = 0) :
    iteratedFDerivWithin 𝕜 n f s x = 0

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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : p n = 0
⊢ iteratedFDerivWithin 𝕜 n f s x = 0

Tactic:
have : iteratedFDerivWithin 𝕜 n f s x = p.iteratedFDerivSeries n 0 (fun _ ↦ 0) :=
  ((h.iteratedFDerivWithin h' n hu hx).coeff_zero _).symm

Result:
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : p n = 0
this : iteratedFDerivWithin 𝕜 n f s x = (p.iteratedFDerivSeries n 0) fun x => 0
⊢ iteratedFDerivWithin 𝕜 n f s x = 0

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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : p n = 0
this : iteratedFDerivWithin 𝕜 n f s x = (p.iteratedFDerivSeries n 0) fun x => 0
⊢ iteratedFDerivWithin 𝕜 n f s x = 0

Tactic:
rw [this, p.iteratedFDerivSeries_eq_zero (p.congr_zero (Nat.zero_add n).symm hn),
  ContinuousMultilinearMap.zero_apply]

Result:
no goals
-- Mathlib/Data/List/EditDistance/Defs.lean
theorem impl_cons (w' : 0 < List.length ds) :
    impl C (x :: xs) y ⟨d :: ds, w⟩ =
      let ⟨r, w⟩ := impl C xs y ⟨ds, w'⟩
      ⟨min (C.delete x + r[0]) (min (C.insert y + d) (C.substitute x y + ds[0])) :: r, by simp⟩ :=
  match ds, w' with | _ :: _, _ => rfl

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
inst✝¹ : AddZeroClass δ
inst✝ : Min δ
C : Cost α β δ
x : α
xs : List α
y : β
d : δ
ds : List δ
w✝ : 0 < (d :: ds).length
w' : 0 < ds.length
r : List δ
w : 0 < r.length
⊢ 0 < (min (C.delete x + r[0]) (min (C.insert y + d) (C.substitute x y + ds[0])) :: r).length

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem findSomeRev?_eq_findSome?_reverse (f : α → Option β) (as : Array α) :
    as.findSomeRev? f = as.reverse.findSome? f

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ findSomeRev? f { toList := toList✝ } = findSome? f { toList := toList✝ }.reverse

Tactic:
simp [findSomeRev?, Id.run]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
as : Array α
⊢ findSomeRev? f as = findSome? f as.reverse

Tactic:
cases as

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ findSomeRev? f { toList := toList✝ } = findSome? f { toList := toList✝ }.reverse
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem _root_.List.length_toAssocList (l : List (α × β)) :
    l.toAssocList.length = l.length

Proof state:
α : Type u_1
β : Type u_2
l : List (α × β)
⊢ l.toAssocList.length = l.length

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.mapsTo_lineMap (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
    MapsTo (AffineMap.lineMap x y) (Icc (0 : 𝕜) 1) s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
⊢ MapsTo (⇑(AffineMap.lineMap x y)) (Icc 0 1) s

Tactic:
simpa only [mapsTo', segment_eq_image_lineMap] using h.segment_subset hx hy

Result:
no goals
-- Mathlib/Data/Fintype/Powerset.lean
@[simp] lemma powerset_univ : (univ : Finset α).powerset = univ :=
  coe_injective <| by simp [-coe_eq_univ]

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ ↑univ.powerset = ↑univ

Tactic:
simp [-coe_eq_univ]

Result:
no goals
-- Mathlib/Analysis/Convex/Strict.lean
theorem StrictConvex.add_right (hs : StrictConvex 𝕜 s) (z : E) :
    StrictConvex 𝕜 ((fun x => x + z) '' s)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s : Set E
hs : StrictConvex 𝕜 s
z : E
⊢ StrictConvex 𝕜 ((fun x => x + z) '' s)

Tactic:
simpa only [add_comm] using hs.add_left z

Result:
no goals
-- Mathlib/Data/PNat/Prime.lean
theorem exists_prime_and_dvd {n : ℕ+} (hn : n ≠ 1) : ∃ p : ℕ+, p.Prime ∧ p ∣ n

Proof state:
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime ⟨p, ⋯⟩ ∧ ↑⟨p, ⋯⟩ ∣ ↑n

Tactic:
apply hp

Result:
no goals

Proof state:
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ ∃ p, p.Prime ∧ p ∣ n

Tactic:
exists (⟨p, Nat.Prime.pos hp.left⟩ : ℕ+)

Result:
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime ⟨p, ⋯⟩ ∧ ⟨p, ⋯⟩ ∣ n

Proof state:
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime ⟨p, ⋯⟩ ∧ ⟨p, ⋯⟩ ∣ n

Tactic:
rw [dvd_iff]

Result:
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ Prime ⟨p, ⋯⟩ ∧ ↑⟨p, ⋯⟩ ∣ ↑n

Proof state:
n : ℕ+
hn : n ≠ 1
⊢ ∃ p, p.Prime ∧ p ∣ n

Tactic:
obtain ⟨p, hp⟩ := Nat.exists_prime_and_dvd (mt coe_eq_one_iff.mp hn)

Result:
case intro
n : ℕ+
hn : n ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ ↑n
⊢ ∃ p, p.Prime ∧ p ∣ n
-- Mathlib/Data/List/InsertIdx.lean
theorem sublist_insertIdx (l : List α) (n : ℕ) (a : α) : l <+ (l.insertIdx n a)

Proof state:
α : Type u
l : List α
n : ℕ
a : α
⊢ l <+ insertIdx n a l

Tactic:
simpa only [eraseIdx_insertIdx] using eraseIdx_sublist (l.insertIdx n a) n

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_pi_div_three : sin (π / 3) = √3 / 2

Proof state:
case e_x

⊢ π / 2 - π / 3 = π / 6

Tactic:
ring

Result:
no goals

Proof state:
⊢ cos (π / 2 - π / 3) = cos (π / 6)

Tactic:
congr

Result:
case e_x

⊢ π / 2 - π / 3 = π / 6

Proof state:
⊢ sin (π / 3) = √3 / 2

Tactic:
rw [← cos_pi_div_two_sub, ← cos_pi_div_six]

Result:
⊢ cos (π / 2 - π / 3) = cos (π / 6)
-- Mathlib/Data/Nat/Multiplicity.lean
theorem sub_one_mul_multiplicity_factorial {n p : ℕ} (hp : p.Prime) :
     (p - 1) * multiplicity p n ! =
     n - (p.digits n).sum

Proof state:
n p : ℕ
hp : Prime p
⊢ (p - 1) * multiplicity p n ! = n - (p.digits n).sum

Tactic:
simp only [multiplicity_eq_of_emultiplicity_eq_some <|
    emultiplicity_factorial hp <| lt_succ_of_lt <| lt.base (log p n),
  ← Finset.sum_Ico_add' _ 0 _ 1, Ico_zero_eq_range, ←
  sub_one_mul_sum_log_div_pow_eq_sub_sum_digits]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem interedges_biUnion_right (s : Finset α) (t : Finset ι) (f : ι → Finset β) :
    interedges r s (t.biUnion f) = t.biUnion fun b ↦ interedges r s (f b)

Proof state:
case h
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
a : α × β
⊢ a ∈ interedges r s (t.biUnion f) ↔ a ∈ t.biUnion fun b => interedges r s (f b)

Tactic:
simp only [mem_interedges_iff, mem_biUnion]

Result:
case h
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
a : α × β
⊢ a.1 ∈ s ∧ (∃ a_1 ∈ t, a.2 ∈ f a_1) ∧ r a.1 a.2 ↔ ∃ a_1 ∈ t, a.1 ∈ s ∧ a.2 ∈ f a_1 ∧ r a.1 a.2

Proof state:
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
⊢ interedges r s (t.biUnion f) = t.biUnion fun b => interedges r s (f b)

Tactic:
ext a

Result:
case h
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
a : α × β
⊢ a ∈ interedges r s (t.biUnion f) ↔ a ∈ t.biUnion fun b => interedges r s (f b)

Proof state:
case h
ι : Type u_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset α
t : Finset ι
f : ι → Finset β
a : α × β
⊢ a.1 ∈ s ∧ (∃ a_1 ∈ t, a.2 ∈ f a_1) ∧ r a.1 a.2 ↔ ∃ a_1 ∈ t, a.1 ∈ s ∧ a.2 ∈ f a_1 ∧ r a.1 a.2

Tactic:
exact ⟨fun ⟨x₁, ⟨x₂, x₃, x₄⟩, x₅⟩ ↦ ⟨x₂, x₃, x₁, x₄, x₅⟩,
  fun ⟨x₂, x₃, x₁, x₄, x₅⟩ ↦ ⟨x₁, ⟨x₂, x₃, x₄⟩, x₅⟩⟩

Result:
no goals
-- Mathlib/RingTheory/Flat/Basic.lean
theorem tensorProduct_mapIncl_injective_of_left
    [Flat R p] [Flat R N] : Function.Injective (mapIncl p q)

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
p : Submodule R M
q : Submodule R N
inst✝¹ : Flat R ↥p
inst✝ : Flat R N
⊢ Function.Injective ⇑(mapIncl p q)

Tactic:
rw [mapIncl, ← rTensor_comp_lTensor]

Result:
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
p : Submodule R M
q : Submodule R N
inst✝¹ : Flat R ↥p
inst✝ : Flat R N
⊢ Function.Injective ⇑(rTensor N p.subtype ∘ₗ lTensor (↥p) q.subtype)

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
p : Submodule R M
q : Submodule R N
inst✝¹ : Flat R ↥p
inst✝ : Flat R N
⊢ Function.Injective ⇑(rTensor N p.subtype ∘ₗ lTensor (↥p) q.subtype)

Tactic:
exact (rTensor_preserves_injective_linearMap _ p.injective_subtype).comp
  (lTensor_preserves_injective_linearMap _ q.injective_subtype)

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean
lemma exact_succ (n : ℕ) :
    (ShortComplex.mk _ _ (I.cocomplex.d_comp_d n (n + 1) (n + 2))).Exact :=
  (HomologicalComplex.exactAt_iff' _ n (n + 1) (n + 2) (by simp)
    (by simp only [CochainComplex.next]; rfl)).1 (I.cocomplex_exactAt_succ n)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ n + 1 + 1 = n + 2

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ (ComplexShape.up ℕ).prev (n + 1) = n

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ (ComplexShape.up ℕ).next (n + 1) = n + 2

Tactic:
simp only [CochainComplex.next]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ n + 1 + 1 = n + 2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem?_eq_some_getElem (l : BitVec w) (i : Nat) (h : i < w) :
    (l[i]? = some l[i]) ↔ True

Proof state:
w : Nat
l : BitVec w
i : Nat
h : i < w
⊢ l[i]? = some l[i] ↔ True

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
    m.isEmpty = true → m.getKeyD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a fallback : α
⊢ m.isEmpty = true → m.getKeyD a fallback = fallback

Tactic:
simp_to_raw using Raw₀.getKeyD_of_isEmpty ⟨m, _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_modify [LawfulBEq α] {k k' : α} {fallback : β k'} {f : β k → β k} (h : m.WF) :
    (m.modify k f).getD k' fallback =
      if heq : k == k' then
        m.get? k |>.map f |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback
      else
        m.getD k' fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
fallback : β k'
f : β k → β k
h : m.WF
⊢ (m.modify k f).getD k' fallback =
    if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).getD fallback else m.getD k' fallback

Tactic:
simp_to_raw using Raw₀.getD_modify

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
    m.1.keys.length = m.1.size

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
⊢ m.val.keys.length = m.val.size

Tactic:
simp_to_model using List.length_keys_eq_length

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem getKey_eq_getKey [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    (hm : Raw.WFImp m.1) {a : α} {h : m.contains a} :
    m.getKey a h = List.getKey a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
h : m.contains a = true
⊢ m.getKey a h = List.getKey a (toListModel m.val.buckets) ⋯

Tactic:
rw [getKey_eq_getKeyₘ, getKeyₘ_eq_getKey hm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sign_nonneg : 0 ≤ sign x ↔ 0 ≤ x

Proof state:
x : Int
n✝ : Nat
⊢ 0 ≤ (ofNat (n✝ + 1)).sign ↔ 0 ≤ ofNat (n✝ + 1)

Tactic:
simp +decide only [sign, true_iff]

Result:
x : Int
n✝ : Nat
⊢ 0 ≤ ofNat (n✝ + 1)

Proof state:
x : Int
⊢ 0 ≤ sign 0 ↔ 0 ≤ 0

Tactic:
rfl

Result:
no goals

Proof state:
x : Int
⊢ 0 ≤ x.sign ↔ 0 ≤ x

Tactic:
match x with
| 0 => rfl
| .ofNat (_ + 1) =>
  simp +decide only [sign, true_iff]
  exact Int.le_add_one (ofNat_nonneg _)
| .negSucc _ => simp +decide [sign]

Result:
no goals

Proof state:
x : Int
n✝ : Nat
⊢ 0 ≤ ofNat (n✝ + 1)

Tactic:
exact Int.le_add_one (ofNat_nonneg _)

Result:
no goals

Proof state:
x : Int
a✝ : Nat
⊢ 0 ≤ -[a✝+1].sign ↔ 0 ≤ -[a✝+1]

Tactic:
simp +decide [sign]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem map_snd_add_zipIdx_eq_zipIdx (l : List α) (n k : Nat) :
    map (Prod.map id (· + n)) (zipIdx l k) = zipIdx l (n + k) :=
  ext_getElem? fun i ↦ by simp [(· ∘ ·), Nat.add_comm, Nat.add_left_comm]; rfl

Proof state:
α : Type u_1
l : List α
n k i : Nat
⊢ Option.map ((Prod.map id fun x => n + x) ∘ fun a => (a, k + i)) l[i]? = Option.map (fun a => (a, n + (k + i))) l[i]?

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem image.map_id [HasImageMap (𝟙 f)] : image.map (𝟙 f) = 𝟙 (image f.hom) :=
  show (HasImageMap.imageMap (𝟙 f)).map = (imageMapId f).map by
    congr; simp only [eq_iff_true_of_subsingleton]

Proof state:
case e_self
C : Type u
inst✝² : Category.{v, u} C
f : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImageMap (𝟙 f)
⊢ HasImageMap.imageMap (𝟙 f) = imageMapId f

Tactic:
simp only [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
f : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImageMap (𝟙 f)
⊢ (HasImageMap.imageMap (𝟙 f)).map = (imageMapId f).map

Tactic:
congr

Result:
case e_self
C : Type u
inst✝² : Category.{v, u} C
f : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImageMap (𝟙 f)
⊢ HasImageMap.imageMap (𝟙 f) = imageMapId f
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_sub_of_degree_lt (h : Polynomial.degree q < Polynomial.degree p) :
    (p - q).leadingCoeff = p.leadingCoeff

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : (-q).degree < p.degree
⊢ (p - q).leadingCoeff = p.leadingCoeff

Tactic:
rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt' h]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
h : q.degree < p.degree
⊢ (p - q).leadingCoeff = p.leadingCoeff

Tactic:
rw [← q.degree_neg] at h

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
h : (-q).degree < p.degree
⊢ (p - q).leadingCoeff = p.leadingCoeff
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem nontrivial_of_lt_top (h : p < ⊤) : Nontrivial (M ⧸ p)

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
h : p < ⊤
x : M
left✝ : x ∈ ⊤
not_mem_s : x ∉ p
⊢ Nontrivial (M ⧸ p)

Tactic:
refine ⟨⟨mk x, 0, ?_⟩⟩

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
h : p < ⊤
x : M
left✝ : x ∈ ⊤
not_mem_s : x ∉ p
⊢ mk x ≠ 0

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
h : p < ⊤
x : M
left✝ : x ∈ ⊤
not_mem_s : x ∉ p
⊢ mk x ≠ 0

Tactic:
simpa using not_mem_s

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
h : p < ⊤
⊢ Nontrivial (M ⧸ p)

Tactic:
obtain ⟨x, _, not_mem_s⟩ := SetLike.exists_of_lt h

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
h : p < ⊤
x : M
left✝ : x ∈ ⊤
not_mem_s : x ∉ p
⊢ Nontrivial (M ⧸ p)
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem natCast_comp {n : ℕ} : (n : R[X]).comp p = n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (↑n).comp p = ↑n

Tactic:
rw [← C_eq_natCast, C_comp]

Result:
no goals
-- Mathlib/Order/Heyting/Regular.lean
theorem isRegular_bot : IsRegular (⊥ : α)

Proof state:
α : Type u_1
inst✝ : HeytingAlgebra α
⊢ IsRegular ⊥

Tactic:
rw [IsRegular, compl_bot, compl_top]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem pow_smul_eq_iff_period_dvd {n : ℕ} {m : M} {a : α} :
    m ^ n • a = a ↔ period m a ∣ n

Proof state:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ n • a = a ↔ period m a ∣ n

Tactic:
rw [period_eq_minimalPeriod, ← isPeriodicPt_iff_minimalPeriod_dvd, isPeriodicPt_smul_iff]

Result:
no goals