harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/SuccPred/LinearLocallyFinite.lean
theorem iterate_succ_toZ (i : ι) (hi : i0 ≤ i) : succ^[(toZ i0 i).toNat] i0 = i

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ succ^[(toZ i0 i).toNat] i0 = i

Tactic:
rw [toZ_of_ge hi, Int.toNat_natCast]

Result:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ succ^[Nat.find ⋯] i0 = i

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ succ^[Nat.find ⋯] i0 = i

Tactic:
exact Nat.find_spec (exists_succ_iterate_of_le hi)

Result:
no goals
-- Mathlib/Algebra/Ring/Basic.lean
theorem pred_ne_self {α : Type*} [NonAssocRing α] [Nontrivial α] (a : α) : a - 1 ≠ a := fun h ↦
  one_ne_zero (neg_injective ((add_right_inj a).mp (by simp [← sub_eq_add_neg, h])))

Proof state:
α : Type u_2
inst✝¹ : NonAssocRing α
inst✝ : Nontrivial α
a : α
h : a - 1 = a
⊢ a + -1 = a + -0

Tactic:
simp [← sub_eq_add_neg, h]

Result:
no goals
-- Mathlib/NumberTheory/Dioph.lean
theorem eq_dioph : Dioph fun v => f v = g v :=
  dioph_comp2 df dg <|
    of_no_dummies _ (Poly.proj &0 - Poly.proj &1) fun v => by
      exact Int.ofNat_inj.symm.trans ⟨@sub_eq_zero_of_eq ℤ _ (v &0) (v &1), eq_of_sub_eq_zero⟩

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
v : Fin2 2 → ℕ
⊢ v &0 = v &1 ↔ (Poly.proj &0 - Poly.proj &1) v = 0

Tactic:
exact Int.ofNat_inj.symm.trans ⟨@sub_eq_zero_of_eq ℤ _ (v &0) (v &1), eq_of_sub_eq_zero⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem norm_deriv_eq_norm_fderiv : ‖deriv f x‖ = ‖fderiv 𝕜 f x‖

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
⊢ ‖deriv f x‖ = ‖fderiv 𝕜 f x‖

Tactic:
simp [← deriv_fderiv]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.isoProduct_hom {f : J → C} [HasBiproduct f] :
    (biproduct.isoProduct f).hom = Pi.lift (biproduct.π f) :=
  limit.hom_ext fun j => by simp [biproduct.isoProduct]

Proof state:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : Discrete J
⊢ (isoProduct f).hom ≫ limit.π (Discrete.functor f) j = Pi.lift (π f) ≫ limit.π (Discrete.functor f) j

Tactic:
simp [biproduct.isoProduct]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
@[to_additive]
lemma eq_bot_iff_card : S = ⊥ ↔ card S = 1 :=
  ⟨by rintro rfl; exact card_bot, eq_bot_of_card_eq⟩

Proof state:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Fintype ↥⊥
⊢ card ↥⊥ = 1

Tactic:
exact card_bot

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : Monoid M
S : Submonoid M
inst✝ : Fintype ↥S
⊢ S = ⊥ → card ↥S = 1

Tactic:
rintro rfl

Result:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Fintype ↥⊥
⊢ card ↥⊥ = 1
-- Mathlib/Data/Finsupp/Defs.lean
theorem mapRange_neg [NegZeroClass G] [NegZeroClass H] {f : G → H} {hf : f 0 = 0}
    (hf' : ∀ x, f (-x) = -f x) (v : α →₀ G) : mapRange f hf (-v) = -mapRange f hf v :=
  ext fun _ => by simp only [hf', neg_apply, mapRange_apply]

Proof state:
α : Type u_1
G : Type u_9
H : Type u_10
inst✝¹ : NegZeroClass G
inst✝ : NegZeroClass H
f : G → H
hf : f 0 = 0
hf' : ∀ (x : G), f (-x) = -f x
v : α →₀ G
x✝ : α
⊢ (mapRange f hf (-v)) x✝ = (-mapRange f hf v) x✝

Tactic:
simp only [hf', neg_apply, mapRange_apply]

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem smeval_ascPochhammer_succ_neg (n : ℕ) :
    smeval (ascPochhammer ℕ (n + 1)) (-n : ℤ) = 0

Proof state:
n : ℕ
⊢ (ascPochhammer ℕ (n + 1)).smeval (-↑n) = 0

Tactic:
rw [ascPochhammer_succ_right, smeval_mul, smeval_add, smeval_X, ← C_eq_natCast, smeval_C,
  pow_zero, pow_one, Nat.cast_id, nsmul_eq_mul, mul_one, neg_add_cancel, mul_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_of_contains_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α} : as.contains a = true → a ∈ as

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
toList✝ : List α
⊢ { toList := toList✝ }.contains a = true → a ∈ { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
as : Array α
⊢ as.contains a = true → a ∈ as

Tactic:
cases as

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
toList✝ : List α
⊢ { toList := toList✝ }.contains a = true → a ∈ { toList := toList✝ }
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem and_congr_left_iff : (a ∧ c ↔ b ∧ c) ↔ c → (a ↔ b)

Proof state:
a c b : Prop
⊢ (a ∧ c ↔ b ∧ c) ↔ c → (a ↔ b)

Tactic:
rw [@and_comm _ c, @and_comm _ c, ← and_congr_right_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem not_isLeft {x : α ⊕ β} : ¬x.isLeft ↔ x.isRight

Proof state:
α : Type u_1
β : Type u_2
x : α ⊕ β
⊢ ¬x.isLeft = true ↔ x.isRight = true

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LSum.lean
theorem domLCongr_single {α₁ : Type*} {α₂ : Type*} (e : α₁ ≃ α₂) (i : α₁) (m : M) :
    (Finsupp.domLCongr e : _ ≃ₗ[R] _) (Finsupp.single i m) = Finsupp.single (e i) m

Proof state:
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α₁ : Type u_7
α₂ : Type u_8
e : α₁ ≃ α₂
i : α₁
m : M
⊢ (Finsupp.domLCongr e) (single i m) = single (e i) m

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem Matrix.toLinearMap₂'_comp (M : Matrix n m R) (P : Matrix n n' R) (Q : Matrix m m' R) :
    LinearMap.compl₁₂ (Matrix.toLinearMap₂' R M) (toLin' P) (toLin' Q) =
      toLinearMap₂' R (Pᵀ * M * Q) :=
  (LinearMap.toMatrix₂' R).injective (by simp)

Proof state:
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
R : Type u_16
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
M : Matrix n m R
P : Matrix n n' R
Q : Matrix m m' R
⊢ (toMatrix₂' R) (((toLinearMap₂' R) M).compl₁₂ (toLin' P) (toLin' Q)) = (toMatrix₂' R) ((toLinearMap₂' R) (Pᵀ * M * Q))

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zipWith_map {μ} (f : γ → δ → μ) (g : α → γ) (h : β → δ) (l₁ : List α) (l₂ : List β) :
    zipWith f (l₁.map g) (l₂.map h) = zipWith (fun a b => f (g a) (h b)) l₁ l₂

Proof state:
γ : Type u_1
δ : Type u_2
α : Type u_3
β : Type u_4
μ : Type u_5
f : γ → δ → μ
g : α → γ
h : β → δ
l₁ : List α
l₂ : List β
⊢ zipWith f (map g l₁) (map h l₂) = zipWith (fun a b => f (g a) (h b)) l₁ l₂

Tactic:
induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all

Result:
no goals
-- Mathlib/Data/List/EditDistance/Bounds.lean
theorem le_levenshtein_append (xs : List α) (ys₁ ys₂) :
    ∃ xs', xs' <:+ xs ∧ levenshtein C xs' ys₂ ≤ levenshtein C xs (ys₁ ++ ys₂)

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
C : Levenshtein.Cost α β δ
inst✝¹ : LinearOrderedAddCommMonoid δ
inst✝ : CanonicallyOrderedAdd δ
xs : List α
ys₁ ys₂ : List β
⊢ ∃ xs', xs' <:+ xs ∧ levenshtein C xs' ys₂ ≤ levenshtein C xs (ys₁ ++ ys₂)

Tactic:
simpa [suffixLevenshtein_eq_tails_map, List.minimum_le_coe_iff] using
  suffixLevenshtein_minimum_le_levenshtein_append (δ := δ) xs ys₁ ys₂

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

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

Tactic:
rintro ⟨⟩ ⟨⟩ _

Result:
case mk.mk
R : Type u
toSemiring✝¹ : Semiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toSemiring✝ : Semiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : toSemiring = toSemiring
⊢ mk mul_comm✝¹ = mk mul_comm✝

Proof state:
case mk.mk
R : Type u
toSemiring✝¹ : Semiring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toSemiring✝ : Semiring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : toSemiring = toSemiring
⊢ mk mul_comm✝¹ = mk mul_comm✝

Tactic:
congr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.not_false : (!false) = true

Proof state:
⊢ (!false) = true

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem Filter.EventuallyEq.derivWithin_eq (hs : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
    derivWithin f₁ s x = derivWithin f s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ (fderivWithin 𝕜 f₁ s x) 1 = (fderivWithin 𝕜 f s x) 1

Tactic:
rw [hs.fderivWithin_eq hx]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ derivWithin f₁ s x = derivWithin f s x

Tactic:
unfold derivWithin

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
s : Set 𝕜
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ (fderivWithin 𝕜 f₁ s x) 1 = (fderivWithin 𝕜 f s x) 1
-- Mathlib/Order/Hom/Order.lean
theorem coe_iInf {ι : Sort*} [CompleteLattice β] (f : ι → α →o β) :
    ((⨅ i, f i : α →o β) : α → β) = ⨅ i, (f i : α → β)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ (⨅ i, f i) x = (⨅ i, ⇑(f i)) x

Tactic:
simp [iInf_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
⊢ ⇑(⨅ i, f i) = ⨅ i, ⇑(f i)

Tactic:
funext x

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
ι : Sort u_3
inst✝ : CompleteLattice β
f : ι → α →o β
x : α
⊢ (⨅ i, f i) x = (⨅ i, ⇑(f i)) x
-- Mathlib/CategoryTheory/Subpresheaf/Image.lean
lemma range_comp (g : F' ⟶ F'') :
    range (f ≫ g) = (range f).image g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F F' F'' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
g : F' ⟶ F''
⊢ range (f ≫ g) = (range f).image g

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_push_of_neg (l : Vector α n) (pa : ¬p a) : countP p (l.push a) = countP p l

Proof state:
α : Type u_1
p : α → Bool
n : Nat
a : α
l : Vector α n
pa : ¬p a = true
⊢ countP p (l.push a) = countP p l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
a : α
pa : ¬p a = true
l : Array α
⊢ countP p ({ toArray := l, size_toArray := ⋯ }.push a) = countP p { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
pa : ¬p a = true
l : Array α
⊢ countP p ({ toArray := l, size_toArray := ⋯ }.push a) = countP p { toArray := l, size_toArray := ⋯ }

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_univ_one [CommMonoid β] (f : Fin 1 → β) : ∏ i, f i = f 0

Proof state:
β : Type u_2
inst✝ : CommMonoid β
f : Fin 1 → β
⊢ ∏ i : Fin 1, f i = f 0

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/Ordinal.lean
theorem toPGame_def (o : Ordinal) : o.toPGame =
    ⟨o.toType, PEmpty, fun x => ((enumIsoToType o).symm x).val.toPGame, PEmpty.elim⟩

Proof state:
o : Ordinal.{u_1}
⊢ o.toPGame = mk o.toType PEmpty.{u_1 + 1} (fun x => (↑(o.enumIsoToType.symm x)).toPGame) PEmpty.elim

Tactic:
rw [toPGame]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderivWithin_zero_of_not_differentiableWithinAt (h : ¬DifferentiableWithinAt 𝕜 f s x) :
    fderivWithin 𝕜 f s x = 0

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
F : Type u_3
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
inst✝ : TopologicalSpace F
f : E → F
x : E
s : Set E
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 f s x = 0

Tactic:
simp [fderivWithin, h]

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem clog_pos {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : 0 < clog b n

Proof state:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < clog b ((n + b - 1) / b) + 1

Tactic:
exact zero_lt_succ _

Result:
no goals

Proof state:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < clog b n

Tactic:
rw [clog_of_two_le hb hn]

Result:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < clog b ((n + b - 1) / b) + 1
-- Mathlib/RingTheory/Smooth/StandardSmoothCotangent.lean
lemma sectionCotangent_eq_iff (x : P.toExtension.CotangentSpace) (y : P.toExtension.Cotangent) :
    sectionCotangent P x = y ↔
      ∀ i : P.rels, P.cotangentSpaceBasis.repr x (P.map i) = (P.cotangentComplexAux y) i

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : P.toExtension.CotangentSpace
y : P.toExtension.Cotangent
⊢ P.sectionCotangent x = y ↔ ∀ (i : P.rels), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i

Tactic:
simp only [sectionCotangent, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : P.toExtension.CotangentSpace
y : P.toExtension.Cotangent
⊢ P.cotangentEquiv.symm
        ((Finsupp.linearEquivFunOnFinite S S P.rels) ((Finsupp.lcomapDomain P.map ⋯) (P.cotangentSpaceBasis.repr x))) =
      y ↔
    ∀ (i : P.rels), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : P.toExtension.CotangentSpace
y : P.toExtension.Cotangent
⊢ (∀ (x_1 : P.rels),
      (Finsupp.linearEquivFunOnFinite S S P.rels) ((Finsupp.lcomapDomain P.map ⋯) (P.cotangentSpaceBasis.repr x)) x_1 =
        P.cotangentEquiv y x_1) ↔
    ∀ (i : P.rels), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : P.toExtension.CotangentSpace
y : P.toExtension.Cotangent
⊢ P.cotangentEquiv.symm
        ((Finsupp.linearEquivFunOnFinite S S P.rels) ((Finsupp.lcomapDomain P.map ⋯) (P.cotangentSpaceBasis.repr x))) =
      y ↔
    ∀ (i : P.rels), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i

Tactic:
rw [← (cotangentEquiv P).injective.eq_iff, funext_iff, LinearEquiv.apply_symm_apply]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
x : P.toExtension.CotangentSpace
y : P.toExtension.Cotangent
⊢ (∀ (x_1 : P.rels),
      (Finsupp.linearEquivFunOnFinite S S P.rels) ((Finsupp.lcomapDomain P.map ⋯) (P.cotangentSpaceBasis.repr x)) x_1 =
        P.cotangentEquiv y x_1) ↔
    ∀ (i : P.rels), (P.cotangentSpaceBasis.repr x) (P.map i) = P.cotangentComplexAux y i
-- Mathlib/Tactic/CategoryTheory/Bicategory/PureCoherence.lean
theorem naturality_id {p : a ⟶ b} {f : b ⟶ c} {pf : a ⟶ c} (η_f : p ≫ f ≅ pf) :
    p ◁ Iso.refl f ≪≫ η_f = η_f :=
  Iso.ext (by simp)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f : b ⟶ c
pf : a ⟶ c
η_f : p ≫ f ≅ pf
⊢ (p ◁ Iso.refl f ≪≫ η_f).hom = η_f.hom

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem _root_.Cardinal.toENat_lt_natCast_iff {n : ℕ} {c : Cardinal} :
    toENat c < ↑n ↔ c < ↑n

Proof state:
n : ℕ
c : Cardinal.{u_3}
⊢ toENat c < ↑n ↔ c < ↑n

Tactic:
simp only [← not_le, Cardinal.natCast_le_toENat_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
theorem mapsTo_reflection_root :
    MapsTo (P.reflection i) (range P.root) (range P.root)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ MapsTo (⇑(P.reflection i)) (range ⇑P.root) (range ⇑P.root)

Tactic:
rintro - ⟨j, rfl⟩

Result:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ (P.reflection i) (P.root j) ∈ range ⇑P.root

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ (P.reflection i) (P.root j) ∈ range ⇑P.root

Tactic:
exact P.root_reflection_perm i j ▸ mem_range_self (P.reflection_perm i j)

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
@[reassoc (attr := simp)]
lemma inv_left_hom_left {f g : Over X} (e : f ≅ g) :
    e.inv.left ≫ e.hom.left = 𝟙 g.left

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f g : Over X
e : f ≅ g
⊢ e.inv.left ≫ e.hom.left = 𝟙 g.left

Tactic:
simp [← Over.comp_left]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Path.lean
theorem nil_comp {a : V} : ∀ {b} (p : Path a b), Path.nil.comp p = p
  | _, nil => rfl
  | _, cons p _ => by rw [comp_cons, nil_comp p]

Proof state:
V : Type u
inst✝ : Quiver V
a x✝ b✝ : V
p : Path a b✝
a✝ : b✝ ⟶ x✝
⊢ nil.comp (p.cons a✝) = p.cons a✝

Tactic:
rw [comp_cons, nil_comp p]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem set_eq_empty_iff {as : Array α} (n : Nat) (a : α) (h) :
     as.set n a = #[] ↔ as = #[]

Proof state:
α : Type u_1
as : Array α
n : Nat
a : α
h : n < as.size
⊢ as.set n a h = #[] ↔ as = #[]

Tactic:
cases as <;> cases n <;> simp [set]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_add_of_sub_right_lt {a b c : Int} (h : a - c < b) : a < b + c

Proof state:
a b c : Int
h✝ : a - c < b
h : a - c + c < b + c
⊢ a < b + c

Tactic:
rwa [Int.sub_add_cancel] at h

Result:
no goals

Proof state:
a b c : Int
h : a - c < b
⊢ a < b + c

Tactic:
have h := Int.add_lt_add_right h c

Result:
a b c : Int
h✝ : a - c < b
h : a - c + c < b + c
⊢ a < b + c
-- Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean
lemma Exact.moduleCat_range_eq_ker (hS : S.Exact) :
    LinearMap.range S.f.hom = LinearMap.ker S.g.hom

Proof state:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
⊢ LinearMap.range (ModuleCat.Hom.hom S.f) = LinearMap.ker (ModuleCat.Hom.hom S.g)

Tactic:
simpa only [moduleCat_exact_iff_range_eq_ker] using hS

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem zero_eq_mk {n a : Nat} {ha : a < n} [NeZero n] :
    0 = (⟨a, ha⟩ : Fin n) ↔ a = 0

Proof state:
n a : ℕ
ha : a < n
inst✝ : NeZero n
⊢ 0 = ⟨a, ha⟩ ↔ a = 0

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Localization.lean
lemma commShiftOfLocalization_iso_inv_app (a : A) (X : C) :
    letI := Functor.commShiftOfLocalization L W A F F'
    (F'.commShiftIso a).inv.app (L.obj X) =
      (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) ≫
      (F.commShiftIso a).inv.app X ≫ (Lifting.iso L W F F').inv.app (X⟦a⟧) ≫
     F'.map ((L.commShiftIso a).hom.app X)

Proof state:
C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a : A
X : C
⊢ (F'.commShiftIso a).inv.app (L.obj X) =
    (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) ≫
      (F.commShiftIso a).inv.app X ≫
        (Lifting.iso L W F F').inv.app ((shiftFunctor C a).obj X) ≫ F'.map ((L.commShiftIso a).hom.app X)

Tactic:
apply commShiftOfLocalization.iso_inv_app

Result:
no goals
-- Mathlib/Algebra/Star/Conjneg.lean
@[simp] lemma conjneg_sum (s : Finset ι) (f : ι → G → R) :
    conjneg (∑ i ∈ s, f i) = ∑ i ∈ s, conjneg (f i)

Proof state:
ι : Type u_1
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
s : Finset ι
f : ι → G → R
⊢ conjneg (∑ i ∈ s, f i) = ∑ i ∈ s, conjneg (f i)

Tactic:
ext

Result:
case h
ι : Type u_1
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
s : Finset ι
f : ι → G → R
x✝ : G
⊢ conjneg (∑ i ∈ s, f i) x✝ = (∑ i ∈ s, conjneg (f i)) x✝

Proof state:
case h
ι : Type u_1
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
s : Finset ι
f : ι → G → R
x✝ : G
⊢ conjneg (∑ i ∈ s, f i) x✝ = (∑ i ∈ s, conjneg (f i)) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Preimage.lean
@[simp]
lemma preimage_map (f : α ↪ β) (s : Finset α) : (s.map f).preimage f f.injective.injOn = s :=
  coe_injective <| by simp only [coe_preimage, coe_map, Set.preimage_image_eq _ f.injective]

Proof state:
α : Type u
β : Type v
f : α ↪ β
s : Finset α
⊢ ↑((map f s).preimage ⇑f ⋯) = ↑s

Tactic:
simp only [coe_preimage, coe_map, Set.preimage_image_eq _ f.injective]

Result:
no goals
-- Mathlib/Data/Fin/Fin2.lean
@[simp] lemma rev_last {n} : rev (@last n) = fz

Proof state:
n : ℕ
⊢ last.rev = fz

Tactic:
induction n <;> simp_all [rev, castSucc, last]

Result:
no goals
-- Mathlib/Combinatorics/Configuration.lean
theorem two_lt_pointCount [Finite P] [Finite L] (l : L) : 2 < pointCount P l

Proof state:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
l : L
⊢ 2 < pointCount P l

Tactic:
simpa only [pointCount_eq P l, Nat.succ_lt_succ_iff] using one_lt_order P L

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem toFiniteMeasure_nonzero (μ : ProbabilityMeasure Ω) : μ.toFiniteMeasure ≠ 0

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ μ.toFiniteMeasure ≠ 0

Tactic:
simp [← FiniteMeasure.mass_nonzero_iff]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
@[simp] lemma inner_zero_left {x : E} : ⟪0, x⟫ = 0

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
x : E
⊢ inner 0 x = 0

Tactic:
simp [← innerₛₗ_apply]

Result:
no goals
-- Mathlib/Data/List/Count.lean
theorem count_lt_length_iff {a : α} : l.count a < l.length ↔ ∃ b ∈ l, b ≠ a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
⊢ count a l < l.length ↔ ∃ b, b ∈ l ∧ b ≠ a

Tactic:
simp [count]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem ne_univ_iff_exists_not_mem {α : Type*} (s : Set α) : s ≠ univ ↔ ∃ a, a ∉ s

Proof state:
α : Type u_1
s : Set α
⊢ s ≠ univ ↔ ∃ a, a ∉ s

Tactic:
rw [← not_forall, ← eq_univ_iff_forall]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_lt_pred_iff : pred a < pred b ↔ a < b

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
⊢ pred a < pred b ↔ a < b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Icc_add_one_left_eq_Ioc (a b : α) : Icc (a + 1) b = Ioc a b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Icc (a + 1) b = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Icc_succ_left_eq_Ioc a b

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem set_eq_take_cons_drop (a : α) {n l} (h : n < length l) :
    set l n a = take n l ++ a :: drop (n + 1) l

Proof state:
α : Type u_1
a : α
n : Nat
l : List α
h : n < l.length
⊢ l.set n a = take n l ++ a :: drop (n + 1) l

Tactic:
rw [set_eq_modify, modify_eq_take_cons_drop h]

Result:
no goals