harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Ring/Defs.lean
lemma ite_zero_mul_ite_zero : ite P a 0 * ite Q b 0 = ite (P ∧ Q) (a * b) 0

Proof state:
α : Type u
inst✝² : MulZeroClass α
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b : α
⊢ ((if P then a else 0) * if Q then b else 0) = if P ∧ Q then a * b else 0

Tactic:
simp only [← ite_and, ite_mul, mul_ite, mul_zero, zero_mul, and_comm]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
private lemma muFun_apply (a b : α) :
    muFun 𝕜 a b = if a = b then 1 else -∑ x ∈ (Ico a b).attach, muFun 𝕜 a x

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ IncidenceAlgebra.muFun 𝕜 a b = if a = b then 1 else -∑ x ∈ (Ico a b).attach, IncidenceAlgebra.muFun 𝕜 a ↑x

Tactic:
rw [muFun]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem count_zero (hp : Irreducible p) : count p (0 : FactorSet α) = 0

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
⊢ p.count 0 = 0

Tactic:
simp only [count, dif_pos hp, bcount, Multiset.count_zero]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem oneCocycles_map_inv (f : oneCocycles A) (g : G) :
    A.ρ g (f g⁻¹) = - f g

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(oneCocycles A)
g : G
⊢ (A.ρ g) (f g⁻¹) = -f g

Tactic:
rw [← add_eq_zero_iff_eq_neg, ← oneCocycles_map_one f, ← mul_inv_cancel g,
  (mem_oneCocycles_iff f).1 f.2 g g⁻¹]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem self_mem_range_succ (n : Nat) : n ∈ range (n + 1)

Proof state:
n : Nat
⊢ n ∈ range (n + 1)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_pos_of_pos_of_dvd {a b : Int} (H1 : 0 < a) (H2 : 0 ≤ b) (H3 : b ∣ a) : 0 < a / b :=
  Int.lt_ediv_of_mul_lt H2 H3 (by rwa [Int.zero_mul])

Proof state:
a b : Int
H1 : 0 < a
H2 : 0 ≤ b
H3 : b ∣ a
⊢ 0 * b < a

Tactic:
rwa [Int.zero_mul]

Result:
no goals
-- Mathlib/Order/RelIso/Basic.lean
theorem rel_symm_apply (e : r ≃r s) {x y} : r x (e.symm y) ↔ s (e x) y

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
x : α
y : β
⊢ r x (e.symm y) ↔ s (e x) y

Tactic:
rw [← e.map_rel_iff, e.apply_symm_apply]

Result:
no goals
-- Mathlib/RingTheory/HopfAlgebra/Basic.lean
lemma sum_antipode_mul_eq_smul {a : A} (repr : Repr R a) :
    ∑ i ∈ repr.index, antipode (R := R) (repr.left i) * repr.right i =
      counit (R := R) a • 1

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
repr : Coalgebra.Repr R a
⊢ ∑ i ∈ repr.index, antipode (repr.left i) * repr.right i = counit a • 1

Tactic:
rw [sum_antipode_mul_eq, Algebra.smul_def, mul_one]

Result:
no goals
-- Mathlib/Algebra/Ring/Identities.lean
theorem pow_four_add_four_mul_pow_four :
    a ^ 4 + 4 * b ^ 4 = ((a - b) ^ 2 + b ^ 2) * ((a + b) ^ 2 + b ^ 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R
⊢ a ^ 4 + 4 * b ^ 4 = ((a - b) ^ 2 + b ^ 2) * ((a + b) ^ 2 + b ^ 2)

Tactic:
ring

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_mono_on (hs : MeasurableSet s) (h : ∀ x ∈ s, f x ≤ g x) :
    ∫ x in s, f x ∂μ ≤ ∫ x in s, g x ∂μ :=
  setIntegral_mono_ae_restrict hf hg
    (by simp [hs, EventuallyLE, eventually_inf_principal, ae_of_all _ h])

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f g : X → ℝ
s : Set X
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : MeasurableSet s
h : ∀ x ∈ s, f x ≤ g x
⊢ f ≤ᶠ[ae (μ.restrict s)] g

Tactic:
simp [hs, EventuallyLE, eventually_inf_principal, ae_of_all _ h]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem infinitesimal_iff_infinite_inv {x : ℝ*} (h : x ≠ 0) : Infinitesimal x ↔ Infinite x⁻¹ :=
  Iff.trans (by rw [inv_inv]) (infinite_iff_infinitesimal_inv (inv_ne_zero h)).symm

Proof state:
x : ℝ*
h : x ≠ 0
⊢ x.Infinitesimal ↔ x⁻¹⁻¹.Infinitesimal

Tactic:
rw [inv_inv]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem blimsup_eq_limsup_subtype {f : Filter β} {u : β → α} {p : β → Prop} :
    blimsup u f p = limsup (u ∘ ((↑) : { x | p x } → β)) (comap (↑) f)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ blimsup u f p = limsup (u ∘ Subtype.val) (comap Subtype.val f)

Tactic:
rw [blimsup_eq_limsup, limsup, limsup, ← map_map, map_comap_setCoe_val]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem restrictScalars_adjoin (K : IntermediateField F E) (S : Set E) :
    restrictScalars F (adjoin K S) = adjoin F (K ∪ S)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
S : Set E
⊢ restrictScalars F (adjoin (↥K) S) = adjoin F (↑K ∪ S)

Tactic:
rw [← adjoin_self _ K, adjoin_adjoin_left, adjoin_self _ K]

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

Proof state:
b : Bool
⊢ (b == false) = !b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ico_inter_Iio : Ico a b ∩ Iio c = Ico a (min b c) :=
  ext <| by simp +contextual [iff_def]

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ∀ (x : α), x ∈ Ico a b ∩ Iio c ↔ x ∈ Ico a (b ⊓ c)

Tactic:
simp +contextual [iff_def]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem exp_eq_exp_iff_exists_int {x y : ℂ} : exp x = exp y ↔ ∃ n : ℤ, x = y + n * (2 * π * I)

Proof state:
x y : ℂ
⊢ cexp x = cexp y ↔ ∃ n, x = y + ↑n * (2 * ↑π * I)

Tactic:
simp only [exp_eq_exp_iff_exp_sub_eq_one, exp_eq_one_iff, sub_eq_iff_eq_add']

Result:
no goals
-- Mathlib/Order/JordanHolder.lean
theorem length_eq {s₁ s₂ : CompositionSeries X} (h : Equivalent s₁ s₂) : s₁.length = s₂.length

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : s₁.Equivalent s₂
⊢ s₁.length = s₂.length

Tactic:
simpa using Fintype.card_congr h.choose

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
theorem isConjRoot_algHom_iff_of_injective {x y : A} {f : A →ₐ[R] B}
    (hf : Function.Injective f) : IsConjRoot R (f x) (f y) ↔ IsConjRoot R x y

Proof state:
R : Type u_1
A : Type u_5
B : Type u_6
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x y : A
f : A →ₐ[R] B
hf : Function.Injective ⇑f
⊢ IsConjRoot R (f x) (f y) ↔ IsConjRoot R x y

Tactic:
rw [isConjRoot_def, isConjRoot_def, algHom_eq f hf, algHom_eq f hf]

Result:
no goals
-- Mathlib/Logic/Equiv/Fin.lean
theorem finSuccEquiv'_below {i : Fin (n + 1)} {m : Fin n} (h : Fin.castSucc m < i) :
    (finSuccEquiv' i) (Fin.castSucc m) = m

Proof state:
n : ℕ
i : Fin (n + 1)
m : Fin n
h : m.castSucc < i
⊢ (finSuccEquiv' i) m.castSucc = some m

Tactic:
rw [← Fin.succAbove_of_castSucc_lt _ _ h, finSuccEquiv'_succAbove]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean
@[reassoc (attr := simp)]
lemma map_condition : G.map c.ι ≫ G.map f = 0

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ G.map (Fork.ι c) ≫ G.map f = 0

Tactic:
rw [← G.map_comp, c.condition, G.map_zero]

Result:
no goals
-- Mathlib/Order/Filter/Cofinite.lean
theorem frequently_cofinite_iff_infinite {p : α → Prop} :
    (∃ᶠ x in cofinite, p x) ↔ Set.Infinite { x | p x }

Proof state:
α : Type u_2
p : α → Prop
⊢ (∃ᶠ (x : α) in cofinite, p x) ↔ {x | p x}.Infinite

Tactic:
simp only [Filter.Frequently, eventually_cofinite, not_not, Set.Infinite]

Result:
no goals
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem nndist_div_right [DivInvMonoid M] [PseudoMetricSpace M] [IsometricSMul Mᵐᵒᵖ M]
    (a b c : M) : nndist (a / c) (b / c) = nndist a b

Proof state:
M : Type u
inst✝² : DivInvMonoid M
inst✝¹ : PseudoMetricSpace M
inst✝ : IsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ nndist (a / c) (b / c) = nndist a b

Tactic:
simp only [div_eq_mul_inv, nndist_mul_right]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem isRegular_aleph'_succ {o : Ordinal} (h : ω ≤ o) : IsRegular (aleph' (succ o))

Proof state:
o : Ordinal.{u_1}
h : ω ≤ o
⊢ (aleph' (succ o)).IsRegular

Tactic:
rw [aleph'_succ]

Result:
o : Ordinal.{u_1}
h : ω ≤ o
⊢ (succ (aleph' o)).IsRegular

Proof state:
o : Ordinal.{u_1}
h : ω ≤ o
⊢ (succ (aleph' o)).IsRegular

Tactic:
exact isRegular_succ (aleph0_le_aleph'.2 h)

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem sSup_image {s : Set β} {f : β → α} : sSup (f '' s) = ⨆ a ∈ s, f a

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
s : Set β
f : β → α
⊢ sSup (f '' s) = ⨆ a ∈ s, f a

Tactic:
rw [← iSup_subtype'', sSup_image']

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem trim_eq_trim_iff {m₁ m₂ : OuterMeasure α} :
    m₁.trim = m₂.trim ↔ ∀ s, MeasurableSet s → m₁ s = m₂ s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ : OuterMeasure α
⊢ m₁.trim = m₂.trim ↔ ∀ (s : Set α), MeasurableSet s → m₁ s = m₂ s

Tactic:
simp only [le_antisymm_iff, trim_le_trim_iff, forall_and]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorPower/Basic.lean
lemma zeroEquiv_naturality (f : M →ₗ[R] N) :
    (zeroEquiv R N).comp (map 0 f) = zeroEquiv R M

Proof state:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ ↑(zeroEquiv R N) ∘ₗ map 0 f = ↑(zeroEquiv R M)

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem le_div_iff_mul_le : a ≤ c / b ↔ a * b ≤ c

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
rw [← mul_le_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Ring/CharZero.lean
@[simp] lemma Nat.cast_pow_eq_one {a : ℕ} (hn : n ≠ 0) : (a : R) ^ n = 1 ↔ a = 1

Proof state:
R : Type u_2
n : ℕ
inst✝¹ : Semiring R
inst✝ : CharZero R
a : ℕ
hn : n ≠ 0
⊢ ↑a ^ n = 1 ↔ a = 1

Tactic:
simp [← cast_pow, cast_eq_one, hn]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubOfPoint_apply_const (w : ι → k) (p : P) (b : P) :
    s.weightedVSubOfPoint (fun _ => p) b w = (∑ i ∈ s, w i) • (p -ᵥ b)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p b : P
⊢ (s.weightedVSubOfPoint (fun x => p) b) w = (∑ i ∈ s, w i) • (p -ᵥ b)

Tactic:
rw [weightedVSubOfPoint_apply, sum_smul]

Result:
no goals
-- Mathlib/Tactic/Abel.lean
theorem const_add_term {α} [AddCommMonoid α] (k n x a a') (h : k + a = a') :
    k + @term α _ n x a = term n x a'

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
k : α
n : ℕ
x a a' : α
h : k + a = a'
⊢ k + term n x a = term n x a'

Tactic:
simp [h.symm, term, add_comm, add_assoc]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Tendsto.lean
theorem tendsto_atTop_mono' [Preorder β] (l : Filter α) ⦃f₁ f₂ : α → β⦄ (h : f₁ ≤ᶠ[l] f₂)
    (h₁ : Tendsto f₁ l atTop) : Tendsto f₂ l atTop :=
  tendsto_atTop.2 fun b => by filter_upwards [tendsto_atTop.1 h₁ b, h] with x using le_trans

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Preorder β
l : Filter α
f₁ f₂ : α → β
h : f₁ ≤ᶠ[l] f₂
h₁ : Tendsto f₁ l atTop
b : β
⊢ ∀ᶠ (a : α) in l, b ≤ f₂ a

Tactic:
filter_upwards [tendsto_atTop.1 h₁ b, h] with x using le_trans

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Real.lean
theorem dist_le_tsum_dist_of_tendsto₀ (h : Summable fun n ↦ dist (f n) (f n.succ))
    (ha : Tendsto f atTop (𝓝 a)) : dist (f 0) a ≤ ∑' n, dist (f n) (f n.succ)

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
h : Summable fun n => dist (f n) (f n.succ)
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ ∑' (n : ℕ), dist (f n) (f n.succ)

Tactic:
simpa only [zero_add] using dist_le_tsum_dist_of_tendsto h ha 0

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem IsBasis.cardinalMk_eq (hIX : M.IsBasis I X) (hJX : M.IsBasis J X) : #I = #J

Proof state:
α : Type u
M : Matroid α
I J X : Set α
inst✝ : M.InvariantCardinalRank
hIX : M.IsBasis I X
hJX : M.IsBasis J X
⊢ #↑I = #↑J

Tactic:
rw [← diff_union_inter I J,
  mk_union_of_disjoint (disjoint_sdiff_left.mono_right inter_subset_right),
  hIX.cardinalMk_diff_comm hJX,
  ← mk_union_of_disjoint (disjoint_sdiff_left.mono_right inter_subset_left),
  inter_comm, diff_union_inter]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem bot_prod_bot : (⊥ : Subgroup G).prod (⊥ : Subgroup N) = ⊥ :=
  SetLike.coe_injective <| by simp [coe_prod]

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
⊢ ↑(⊥.prod ⊥) = ↑⊥

Tactic:
simp [coe_prod]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem inner_orthogonalProjection_left_eq_right [HasOrthogonalProjection K] (u v : E) :
    ⟪↑(orthogonalProjection K u), v⟫ = ⟪u, orthogonalProjection K v⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
u v : E
⊢ ⟪↑((orthogonalProjection K) u), v⟫_𝕜 = ⟪u, ↑((orthogonalProjection K) v)⟫_𝕜

Tactic:
rw [← inner_orthogonalProjection_eq_of_mem_left, inner_orthogonalProjection_eq_of_mem_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_eraseIdx (a : Vector α n) (i) (h) :
    (a.eraseIdx i h).toList = a.toList.eraseIdx i

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
h : i < n
⊢ (a.eraseIdx i h).toList = a.toList.eraseIdx i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem infinite_univ_iff : (@univ α).Infinite ↔ Infinite α

Proof state:
α : Type u
⊢ univ.Infinite ↔ Infinite α

Tactic:
rw [Set.Infinite, finite_univ_iff, not_finite_iff_infinite]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isLittleO_of_subsingleton [Subsingleton E'] : f' =o[l] g' :=
  IsLittleO.of_bound fun c hc => by simp [Subsingleton.elim (f' _) 0, mul_nonneg hc.le]

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
inst✝ : Subsingleton E'
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c * ‖g' x‖

Tactic:
simp [Subsingleton.elim (f' _) 0, mul_nonneg hc.le]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem nonneg_iff_zero_le {a : ℤ√d} : Nonneg a ↔ 0 ≤ a :=
  show _ ↔ Nonneg _ by simp

Proof state:
d : ℕ
a : ℤ√↑d
⊢ a.Nonneg ↔ (a - 0).Nonneg

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem measurable_inv_iff {G : Type*} [Group G] [MeasurableSpace G] [MeasurableInv G]
    {f : α → G} : (Measurable fun x => (f x)⁻¹) ↔ Measurable f :=
  ⟨fun h => by simpa only [inv_inv] using h.inv, fun h => h.inv⟩

Proof state:
α : Type u_3
m : MeasurableSpace α
G : Type u_4
inst✝² : Group G
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableInv G
f : α → G
h : Measurable fun x => (f x)⁻¹
⊢ Measurable f

Tactic:
simpa only [inv_inv] using h.inv

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem pow_sub_one_eq [IsDomain R] {ζ : R} (hζ : IsPrimitiveRoot ζ k) (hk : 1 < k) :
    ζ ^ k.pred = -∑ i ∈ range k.pred, ζ ^ i

Proof state:
R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
hζ : IsPrimitiveRoot ζ k
hk : 1 < k
⊢ ζ ^ k.pred = -∑ i ∈ range k.pred, ζ ^ i

Tactic:
rw [eq_neg_iff_add_eq_zero, add_comm, ← sum_range_succ, ← Nat.succ_eq_add_one,
  Nat.succ_pred_eq_of_pos (pos_of_gt hk), hζ.geom_sum_eq_zero hk]

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem mul_right_apply_same (i : m) (j : n) (a : l) (M : Matrix l m α) :
    (M * stdBasisMatrix i j c) a j = M a i * c

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : m
j : n
a : l
M : Matrix l m α
⊢ (M * stdBasisMatrix i j c) a j = M a i * c

Tactic:
simp [mul_apply, stdBasisMatrix, mul_comm]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Slope.lean
theorem hasDerivWithinAt_iff_tendsto_slope' (hs : x ∉ s) :
    HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s] x) (𝓝 f')

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
hs : x ∉ s
⊢ HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s] x) (𝓝 f')

Tactic:
rw [hasDerivWithinAt_iff_tendsto_slope, diff_singleton_eq_self hs]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LSum.lean
theorem mulLeftMap_apply_single {M N : Submodule R S} {ι : Type*} (m : ι → M) (i : ι) (n : N) :
    mulLeftMap N m (Finsupp.single i n) = (m i).1 * n.1

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
S : Type u_4
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : SMulCommClass R R S
inst✝ : SMulCommClass R S S
M N : Submodule R S
ι : Type u_5
m : ι → ↥M
i : ι
n : ↥N
⊢ (mulLeftMap N m) (single i n) = ↑(m i) * ↑n

Tactic:
simp [mulLeftMap]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma le_untopD_iff (hy : y = ⊤ → a ≤ b) : a ≤ y.untopD b ↔ a ≤ y

Proof state:
α : Type u_1
a b : α
inst✝ : LE α
y : WithTop α
hy : y = ⊤ → a ≤ b
⊢ a ≤ untopD b y ↔ ↑a ≤ y

Tactic:
cases y <;> simp [hy]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem map_comm (H : ψ ∘ φ = ρ ∘ θ) (F : Filter α) :
    map ψ (map φ F) = map ρ (map θ F)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
F : Filter α
⊢ map ψ (map φ F) = map ρ (map θ F)

Tactic:
rw [Filter.map_map, H, ← Filter.map_map]

Result:
no goals
-- Mathlib/Order/Category/Frm.lean
lemma comp_apply {X Y Z : Frm} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y Z : Frm
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem satAssignment_inl : (cnfSatAssignment aig assign1) (.inl x) = assign1 x

Proof state:
aig : AIG Nat
assign1 : Nat → Bool
x : Nat
⊢ cnfSatAssignment aig assign1 (Sum.inl x) = assign1 x

Tactic:
simp [cnfSatAssignment, mixAssigns]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
lemma le_chromaticNumber_iff_forall_surjective :
    n ≤ G.chromaticNumber ↔ ∀ C : G.Coloring (Fin n), Surjective C

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ ↑n ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring (Fin n)), Surjective ⇑C

Tactic:
simp [← card_le_chromaticNumber_iff_forall_surjective]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
    Const.get? (m.erase k) a = if k == a then none else get? m a

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
⊢ get? (m.erase k) a = if (k == a) = true then none else get? m a

Tactic:
simp_to_raw using Raw₀.Const.get?_erase

Result:
no goals
-- Mathlib/Data/Int/CardIntervalMod.lean
theorem Ico_filter_modEq_card (v : ℕ) :
    #{x ∈ Ico a b | x ≡ v [MOD r]} = max (⌈(b - v) / (r : ℚ)⌉ - ⌈(a - v) / (r : ℚ)⌉) 0

Proof state:
a b r : ℕ
hr : 0 < r
v : ℕ
⊢ ↑(#(filter (fun x => x ≡ v [MOD r]) (Ico a b))) = (⌈(↑b - ↑v) / ↑r⌉ - ⌈(↑a - ↑v) / ↑r⌉) ⊔ 0

Tactic:
simp_rw [← Ico_filter_modEq_cast _ _ ▸ card_map _,
  Int.Ico_filter_modEq_card _ _ (cast_lt.mpr hr), Int.cast_natCast]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem lt_iff_exists_rat_btwn (a b : ℝ≥0) :
    a < b ↔ ∃ q : ℚ, 0 ≤ q ∧ a < Real.toNNReal q ∧ Real.toNNReal q < b :=
  Iff.intro
    (fun h : (↑a : ℝ) < (↑b : ℝ) =>
      let ⟨q, haq, hqb⟩ := exists_rat_btwn h
      have : 0 ≤ (q : ℝ) := le_trans a.2 <| le_of_lt haq
      ⟨q, Rat.cast_nonneg.1 this, by
        simp [Real.coe_toNNReal _ this, NNReal.coe_lt_coe.symm, haq, hqb]⟩)
    fun ⟨_, _, haq, hqb⟩ => lt_trans haq hqb

Proof state:
a b : ℝ≥0
h : ↑a < ↑b
q : ℚ
haq : ↑a < ↑q
hqb : ↑q < ↑b
this : 0 ≤ ↑q
⊢ a < (↑q).toNNReal ∧ (↑q).toNNReal < b

Tactic:
simp [Real.coe_toNNReal _ this, NNReal.coe_lt_coe.symm, haq, hqb]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
theorem ι_eq_zero_iff (x : M) : ι R x = 0 ↔ x = 0

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ (ι R) x = 0 ↔ x = 0

Tactic:
rw [← ι_inj R x 0, LinearMap.map_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem allOnes_shiftLeft_and_shiftLeft {x : BitVec w} {n : Nat} :
    BitVec.allOnes w <<< n &&& x <<< n = x <<< n

Proof state:
w : Nat
x : BitVec w
n : Nat
⊢ allOnes w <<< n &&& x <<< n = x <<< n

Tactic:
simp [← BitVec.shiftLeft_and_distrib]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem toNNReal_le_toNNReal_iff {r p : ℝ} (hp : 0 ≤ p) :
    toNNReal r ≤ toNNReal p ↔ r ≤ p

Proof state:
r p : ℝ
hp : 0 ≤ p
⊢ r.toNNReal ≤ p.toNNReal ↔ r ≤ p

Tactic:
simp [← NNReal.coe_le_coe, hp]

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem AffineSubspace.convex (Q : AffineSubspace 𝕜 E) : Convex 𝕜 (Q : Set E) :=
  fun x hx y hy a b _ _ hab ↦ by simpa [Convex.combo_eq_smul_sub_add hab] using Q.2 _ hy hx hx

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
Q : AffineSubspace 𝕜 E
x : E
hx : x ∈ ↑Q
y : E
hy : y ∈ ↑Q
a b : 𝕜
x✝¹ : 0 ≤ a
x✝ : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ↑Q

Tactic:
simpa [Convex.combo_eq_smul_sub_add hab] using Q.2 _ hy hx hx

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Hasse.lean
theorem hasse_preconnected_of_succ [SuccOrder α] [IsSuccArchimedean α] : (hasse α).Preconnected :=
  fun a b => by
  rw [reachable_iff_reflTransGen]
  exact
    reflTransGen_of_succ _ (fun c hc => Or.inl <| covBy_succ_of_not_isMax hc.2.not_isMax)
      fun c hc => Or.inr <| covBy_succ_of_not_isMax hc.2.not_isMax

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ (hasse α).Reachable a b

Tactic:
rw [reachable_iff_reflTransGen]

Result:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ ReflTransGen (hasse α).Adj a b

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
a b : α
⊢ ReflTransGen (hasse α).Adj a b

Tactic:
exact
  reflTransGen_of_succ _ (fun c hc => Or.inl <| covBy_succ_of_not_isMax hc.2.not_isMax)
    fun c hc => Or.inr <| covBy_succ_of_not_isMax hc.2.not_isMax

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
/-- If `m` and `n` are equal mod `k`, `m - n` is zero mod `k`. -/
lemma sub_mod_eq_zero_of_mod_eq (h : m % k = n % k) : (m - n) % k = 0

Proof state:
m n k : ℕ
h : m % k = n % k
⊢ (m - n) % k = 0

Tactic:
rw [← Nat.mod_add_div m k, ← Nat.mod_add_div n k, ← h, ← Nat.sub_sub,
  Nat.add_sub_cancel_left, ← k.mul_sub, Nat.mul_mod_right]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Basic.lean
theorem map_neg_one : f (-1) = 1 :=
  (pow_eq_one_iff (Nat.succ_ne_zero 1)).1 <| by rw [← map_pow, neg_one_sq, map_one]

Proof state:
M : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : MulLeftMono M
f : R →* M
⊢ f (-1) ^ Nat.succ 1 = 1

Tactic:
rw [← map_pow, neg_one_sq, map_one]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
@[simp] lemma _root_.isCauSeq_neg : IsCauSeq abv (-f) ↔ IsCauSeq abv f

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
⊢ IsCauSeq abv (-f) ↔ IsCauSeq abv f

Tactic:
simp only [IsCauSeq, Pi.neg_apply, ← neg_sub', abv_neg]

Result:
no goals