harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem cmp_div_one' [MulRightMono α] (a b : α) :
    cmp (a / b) 1 = cmp a b

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulRightMono α
a b : α
⊢ cmp (a / b) 1 = cmp a b

Tactic:
rw [← cmp_mul_right' _ _ b, one_mul, div_mul_cancel]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem DistinctKeys.eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} :
    DistinctKeys l → DistinctKeys (eraseKey k l)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
⊢ (keys (List.eraseKey k l)).Sublist (keys l)

Tactic:
simpa using erase_sublist _ _

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
⊢ DistinctKeys l → DistinctKeys (List.eraseKey k l)

Tactic:
apply distinctKeys_of_sublist_keys (by simpa using erase_sublist _ _)

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ico_add_one_add_one_eq_Ioc (a b : α) : Ico (a + 1) (b + 1) = Ioc a b

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

Tactic:
simpa [succ_eq_add_one] using Ico_succ_succ_eq_Ioc a b

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_int_add (m : ℤ) (a : α) : fract (↑m + a) = fract a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
m : ℤ
a : α
⊢ fract (↑m + a) = fract a

Tactic:
rw [add_comm, fract_add_int]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_push {l : Array α} {a : α} :
    mapIdx f (l.push a) = (mapIdx f l).push (f l.size a)

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : Array α
a : α
⊢ mapIdx f (l.push a) = (mapIdx f l).push (f l.size a)

Tactic:
simp [← append_singleton, mapIdx_append]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem le_neg {a b : EReal} : a ≤ -b ↔ b ≤ -a

Proof state:
a b : EReal
⊢ a ≤ -b ↔ b ≤ -a

Tactic:
rw [← neg_le_neg_iff, neg_neg]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem modEq_zero_iff_dvd : a ≡ 0 [MOD n] ↔ n ∣ a

Proof state:
n a : ℕ
⊢ a ≡ 0 [MOD n] ↔ n ∣ a

Tactic:
rw [ModEq, zero_mod, dvd_iff_mod_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `inv_le_iff_one_le_mul₀` for a version with multiplication on the other side. -/
lemma inv_le_iff_one_le_mul₀' (ha : 0 < a) : a⁻¹ ≤ b ↔ 1 ≤ a * b

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulMono G₀
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b

Tactic:
rw [← inv_mul_le_iff₀ ha, mul_one]

Result:
no goals
-- Mathlib/Algebra/Homology/ComplexShapeSigns.lean
lemma ε_add (p q : I) : c.ε (p + q) = c.ε p * c.ε q

Proof state:
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
p q : I
⊢ c.ε (p + q) = c.ε p * c.ε q

Tactic:
apply MonoidHom.map_mul

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem or_none : or o none = o

Proof state:
α✝ : Type u_1
o : Option α✝
⊢ o.or none = o

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
theorem sign_mul_self_eq_abs (a : ℤ) : sign a * a = |a|

Proof state:
a : ℤ
⊢ a.sign * a = |a|

Tactic:
rw [abs_eq_natAbs, sign_mul_self_eq_natAbs]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_natCast (n : ℕ) : ⌈(n : α)⌉₊ = n :=
  eq_of_forall_ge_iff fun a => by rw [ceil_le, cast_le]

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
n a : ℕ
⊢ ⌈↑n⌉₊ ≤ a ↔ n ≤ a

Tactic:
rw [ceil_le, cast_le]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lTensor_id_apply (x : M ⊗[R] N) : (LinearMap.id : N →ₗ[R] N).lTensor M x = x

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
⊢ (lTensor M id) x = x

Tactic:
rw [lTensor_id, id_coe, _root_.id]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem bihimp_bihimp_cancel_right : b ⇔ a ⇔ a = b

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ b ⇔ a ⇔ a = b

Tactic:
simp [bihimp_assoc]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem Commute.mul_geom_sum₂ [Ring α] {x y : α} (h : Commute x y) (n : ℕ) :
    ((x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = x ^ n - y ^ n

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n

Tactic:
rw [← neg_sub (y ^ n), ← h.mul_neg_geom_sum₂, ← neg_mul, neg_sub]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem invRev_invRev : invRev (invRev L₁) = L₁

Proof state:
α : Type u
L₁ : List (α × Bool)
⊢ invRev (invRev L₁) = L₁

Tactic:
simp [invRev, List.map_reverse, Function.comp_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem length_take_le' (n) (l : List α) : length (take n l) ≤ l.length :=
  by simp [Nat.min_le_right]

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ (take n l).length ≤ l.length

Tactic:
simp [Nat.min_le_right]

Result:
no goals
-- Mathlib/CategoryTheory/PUnit.lean
theorem punit_ext' (F G : C ⥤ Discrete PUnit.{w + 1}) : F = G :=
  Functor.ext fun X => by simp only [eq_iff_true_of_subsingleton]

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Discrete PUnit.{w + 1}
X : C
⊢ F.obj X = G.obj X

Tactic:
simp only [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma baseChange_negY :
    (W'.baseChange B).toAffine.negY (f x) (f y) = f ((W'.baseChange A).toAffine.negY x y)

Proof state:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
x y : A
⊢ (baseChange W' B).toAffine.negY (f x) (f y) = f ((baseChange W' A).toAffine.negY x y)

Tactic:
rw [← RingHom.coe_coe, ← map_negY, map_baseChange]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
lemma iIndep_iff_iIndepSets (m : ι → MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : Measure Ω) :
    iIndep m μ ↔ iIndepSets (fun x ↦ {s | MeasurableSet[m x] s}) μ

Proof state:
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
_mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ iIndep m μ ↔ iIndepSets (fun x => {s | MeasurableSet s}) μ

Tactic:
simp only [iIndep, iIndepSets, Kernel.iIndep]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem abs_mul_sign (x : EReal) : (x.abs * sign x : EReal) = x

Proof state:
x : EReal
⊢ ↑x.abs * ↑(sign x) = x

Tactic:
rw [EReal.mul_comm, EReal.sign_mul_abs]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem evalWhiskerLeft_of_cons
    {f : a ⟶ b} {g h i j : b ⟶ c}
    (α : g ≅ h) (η : h ⟶ i) {ηs : i ⟶ j} {θ : f ≫ i ⟶ f ≫ j} (e_θ : f ◁ ηs = θ) :
    f ◁ (α.hom ≫ η ≫ ηs) = (whiskerLeftIso f α).hom ≫ f ◁ η ≫ θ

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h i j : b ⟶ c
α : g ≅ h
η : h ⟶ i
ηs : i ⟶ j
θ : f ≫ i ⟶ f ≫ j
e_θ : f ◁ ηs = θ
⊢ f ◁ (α.hom ≫ η ≫ ηs) = (whiskerLeftIso f α).hom ≫ f ◁ η ≫ θ

Tactic:
simp [e_θ]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_liminf_le' {f : ℕ → α → ℝ≥0∞} (h_meas : ∀ n, AEMeasurable (f n) μ) :
    ∫⁻ a, liminf (fun n => f n a) atTop ∂μ ≤ liminf (fun n => ∫⁻ a, f n a ∂μ) atTop :=
  calc
    ∫⁻ a, liminf (fun n => f n a) atTop ∂μ = ∫⁻ a, ⨆ n : ℕ, ⨅ i ≥ n, f i a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
⊢ ∫⁻ (a : α), liminf (fun n => f n a) atTop ∂μ = ∫⁻ (a : α), ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i a ∂μ

Tactic:
simp only [liminf_eq_iSup_iInf_of_nat]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem cons_mulVec [Fintype n'] (v : n' → α) (A : Fin m → n' → α) (w : n' → α) :
    (of <| vecCons v A) *ᵥ w = vecCons (dotProduct v w) (of A *ᵥ w)

Proof state:
α : Type u
m : ℕ
n' : Type uₙ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
⊢ of (vecCons v A) *ᵥ w = vecCons (v ⬝ᵥ w) (of A *ᵥ w)

Tactic:
ext i

Result:
case h
α : Type u
m : ℕ
n' : Type uₙ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin m.succ
⊢ (of (vecCons v A) *ᵥ w) i = vecCons (v ⬝ᵥ w) (of A *ᵥ w) i

Proof state:
case h
α : Type u
m : ℕ
n' : Type uₙ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
w : n' → α
i : Fin m.succ
⊢ (of (vecCons v A) *ᵥ w) i = vecCons (v ⬝ᵥ w) (of A *ᵥ w) i

Tactic:
refine Fin.cases ?_ ?_ i <;> simp [mulVec]

Result:
no goals
-- Mathlib/FieldTheory/Fixed.lean
theorem isIntegral [Finite G] (x : F) : IsIntegral (FixedPoints.subfield G F) x

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
x : F
⊢ IsIntegral (↥(subfield G F)) x

Tactic:
cases nonempty_fintype G

Result:
case intro
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ IsIntegral (↥(subfield G F)) x

Proof state:
case intro
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Finite G
x : F
val✝ : Fintype G
⊢ IsIntegral (↥(subfield G F)) x

Tactic:
exact ⟨minpoly G F x, minpoly.monic G F x, minpoly.eval₂ G F x⟩

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_div_cancel_left (a b : G) : a / b / a = b⁻¹

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a / b / a = b⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem one_lt_encard_iff : 1 < s.encard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Proof state:
α : Type u_1
s : Set α
⊢ 1 < s.encard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
rw [← not_iff_not, not_exists, not_lt, encard_le_one_iff]

Result:
α : Type u_1
s : Set α
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ (x : α), ¬∃ b, x ∈ s ∧ b ∈ s ∧ x ≠ b

Proof state:
α : Type u_1
s : Set α
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ (x : α), ¬∃ b, x ∈ s ∧ b ∈ s ∧ x ≠ b

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Int.lean
lemma isCompl_even_odd : IsCompl { n : ℤ | Even n } { n | Odd n }

Proof state:
⊢ IsCompl {n | Even n} {n | Odd n}

Tactic:
simp [← not_even_iff_odd, ← Set.compl_setOf, isCompl_compl]

Result:
no goals
-- Mathlib/Order/Fin/Tuple.lean
lemma preimage_insertNth_Icc_of_mem {i : Fin (n + 1)} {x : α i} {q₁ q₂ : ∀ j, α j}
    (hx : x ∈ Icc (q₁ i) (q₂ i)) :
    i.insertNth x ⁻¹' Icc q₁ q₂ = Icc (fun j ↦ q₁ (i.succAbove j)) fun j ↦ q₂ (i.succAbove j) :=
  Set.ext fun p ↦ by simp only [mem_preimage, insertNth_mem_Icc, hx, true_and]

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
i : Fin (n + 1)
x : α i
q₁ q₂ : (j : Fin (n + 1)) → α j
hx : x ∈ Icc (q₁ i) (q₂ i)
p : (j : Fin n) → α (i.succAbove j)
⊢ p ∈ i.insertNth x ⁻¹' Icc q₁ q₂ ↔ p ∈ Icc (fun j => q₁ (i.succAbove j)) fun j => q₂ (i.succAbove j)

Tactic:
simp only [mem_preimage, insertNth_mem_Icc, hx, true_and]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma neg_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.neg P = P z • ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.neg P = P z • ![P x / P z ^ 2, (toAffine W).negY (P x / P z ^ 2) (P y / P z ^ 3), 1]

Tactic:
erw [neg, smul_fin3, mul_div_cancel₀ _ <| pow_ne_zero 2 hPz, ← negY_of_Z_ne_zero hPz,
  mul_div_cancel₀ _ <| pow_ne_zero 3 hPz, mul_one]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractRight_one : (1 : CliffordAlgebra Q)⌊d = 0

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
⊢ (contractRight 1) d = 0

Tactic:
simpa only [map_one] using contractRight_algebraMap Q d 1

Result:
no goals
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem mem_perpBisector_iff_dist_eq' : c ∈ perpBisector p₁ p₂ ↔ dist p₁ c = dist p₂ c

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ c ∈ perpBisector p₁ p₂ ↔ dist p₁ c = dist p₂ c

Tactic:
simp only [mem_perpBisector_iff_dist_eq, dist_comm]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem succ_aleph0 : succ ℵ₀ = ℵ₁

Proof state:
⊢ succ ℵ₀ = ℵ_ 1

Tactic:
rw [← aleph_zero, ← aleph_succ, Ordinal.succ_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem degree_quadratic_lt_degree_C_mul_X_cb (ha : a ≠ 0) :
    degree (C b * X ^ 2 + C c * X + C d) < degree (C a * X ^ 3)

Proof state:
R : Type u
a b c d : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C b * X ^ 2 + C c * X + C d).degree < (C a * X ^ 3).degree

Tactic:
simpa only [degree_C_mul_X_pow 3 ha] using degree_quadratic_lt

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem one_lt_aleph0 : 1 < ℵ₀

Proof state:
⊢ 1 < ℵ₀

Tactic:
simpa using nat_lt_aleph0 1

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma one_lt_pow (hn : n ≠ 0) (ha : 1 < a) : 1 < a ^ n

Proof state:
a n : ℕ
hn : n ≠ 0
ha : 1 < a
⊢ 1 < a ^ n

Tactic:
simpa using Nat.pow_lt_pow_left ha hn

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean
theorem singletonFinsubgraph_le_adj_right {u v : V} {e : G.Adj u v} :
    singletonFinsubgraph v ≤ finsubgraphOfAdj e

Proof state:
V : Type u
G : SimpleGraph V
u v : V
e : G.Adj u v
⊢ singletonFinsubgraph v ≤ finsubgraphOfAdj e

Tactic:
simp [singletonFinsubgraph, finsubgraphOfAdj]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem Basis.equivFun_symm_apply [Fintype ι] (b : Basis ι R M) (x : ι → R) :
    b.equivFun.symm x = ∑ i, x i • b i

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
x : ι → R
⊢ b.equivFun.symm x = ∑ i : ι, x i • b i

Tactic:
simp [Basis.equivFun, Finsupp.linearCombination_apply, sum_fintype, equivFunOnFinite]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem smul_of [MulOneClass G] (g : G) (r : k) : r • of k G g = single g r

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : MulOneClass G
g : G
r : k
⊢ r • (of k G) g = single g r

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem mk_cons_eq_insert (c : Sigma β) (l : List (Sigma β)) (h : (c :: l).NodupKeys) :
    (⟨c :: l, h⟩ : AList β) = insert c.1 c.2 ⟨l, nodupKeys_of_nodupKeys_cons h⟩

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
c : Sigma β
l : List (Sigma β)
h : (c :: l).NodupKeys
⊢ { entries := c :: l, nodupKeys := h } = insert c.fst c.snd { entries := l, nodupKeys := ⋯ }

Tactic:
simpa [insert] using (kerase_of_not_mem_keys <| not_mem_keys_of_nodupKeys_cons h).symm

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_inter_Ioo_of_right_le (h : b₂ ≤ b₁) : Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (max a₁ a₂) b₂ :=
  ext fun x => by
    simp [and_assoc, @and_left_comm (x ≤ _),
      and_iff_right_iff_imp.2 fun h' => (le_of_lt h').trans h]

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₂ ≤ b₁
x : α
⊢ x ∈ Ioc a₁ b₁ ∩ Ioo a₂ b₂ ↔ x ∈ Ioo (a₁ ⊔ a₂) b₂

Tactic:
simp [and_assoc, @and_left_comm (x ≤ _),
  and_iff_right_iff_imp.2 fun h' => (le_of_lt h').trans h]

Result:
no goals
-- Mathlib/RingTheory/Presentation.lean
lemma ofBijectiveAlgebraMap_dimension (h : Function.Bijective (algebraMap R S)) :
    (ofBijectiveAlgebraMap h).dimension = 0

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Bijective ⇑(algebraMap R S)
⊢ (ofBijectiveAlgebraMap h).dimension = 0

Tactic:
simp_rw [dimension, ofBijectiveAlgebraMap, Generators.ofSurjectiveAlgebraMap,
  Generators.ofSurjective, Nat.card_eq_fintype_card, Fintype.card_ofIsEmpty]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioi_inter_Ioo : Set.Ioi a ∩ Set.Ioo b c = Set.Ioo (max a b) c

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioi a ∩ Ioo b c = Ioo (a ⊔ b) c

Tactic:
rw [inter_comm, Ioo_inter_Ioi, max_comm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem compl_apply_diag [Zero α] [One α] (i : V) : A.compl i i = 0

Proof state:
V : Type u_1
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
i : V
⊢ A.compl i i = 0

Tactic:
simp [compl]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/DotProduct.lean
lemma mul_self_mul_conjTranspose_eq_zero {p} (A : Matrix m n R) (B : Matrix p m R) :
    B * (A * Aᴴ) = 0 ↔ B * A = 0

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix p m R
⊢ B * (A * Aᴴ) = 0 ↔ B * A = 0

Tactic:
rw [← conjTranspose_eq_zero, conjTranspose_mul, conjTranspose_mul, conjTranspose_conjTranspose,
  self_mul_conjTranspose_mul_eq_zero, ← conjTranspose_mul, conjTranspose_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_singleton_self (a : α) : a ∈ #[a]

Proof state:
α : Type u_1
a : α
⊢ a ∈ #[a]

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem Finset.centerMass_smul : (t.centerMass w fun i => c • z i) = c • t.centerMass w z

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
c : R
t : Finset ι
w : ι → R
z : ι → E
⊢ (t.centerMass w fun i => c • z i) = c • t.centerMass w z

Tactic:
simp only [Finset.centerMass, Finset.smul_sum, (mul_smul _ _ _).symm, mul_comm c, mul_assoc]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem getD_default_eq_iget [Inhabited α] (o : Option α) :
    o.getD default = o.iget

Proof state:
α : Type u_1
inst✝ : Inhabited α
o : Option α
⊢ o.getD default = o.iget

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem dvd_trans : ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c
  | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => Exists.intro (d * e) (by rw [Int.mul_assoc])

Proof state:
a✝ d e : Int
⊢ a✝ * d * e = a✝ * (d * e)

Tactic:
rw [Int.mul_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_unitOfList_le [EquivBEq α] [LawfulHashable α]
    {l : List α} :
    (unitOfList l).size ≤ l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
⊢ (unitOfList l).size ≤ l.length

Tactic:
simp_to_raw using Raw₀.Const.size_insertManyIfNewUnit_empty_list_le

Result:
no goals
-- Mathlib/Topology/ContinuousMap/CompactlySupported.lean
theorem sum_apply [AddCommMonoid β] [ContinuousAdd β] {ι : Type*} (s : Finset ι) (f : ι → C_c(α, β))
    (a : α) : (∑ i ∈ s, f i) a = ∑ i ∈ s, f i a

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : ContinuousAdd β
ι : Type u_5
s : Finset ι
f : ι → α →C_c β
a : α
⊢ (∑ i ∈ s, f i) a = ∑ i ∈ s, (f i) a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
theorem exists_lt_card_finite_nth_eq (hf : (setOf p).Finite) {x} (h : p x) :
    ∃ n, n < #hf.toFinset ∧ nth p n = x

Proof state:
p : ℕ → Prop
hf : (setOf p).Finite
x : ℕ
h : p x
⊢ ∃ n < #hf.toFinset, nth p n = x

Tactic:
rwa [← @Set.mem_setOf_eq _ _ p, ← image_nth_Iio_card hf] at h

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinaryHeap.lean
theorem size_insert (self : BinaryHeap α lt) (x : α) :
    (self.insert x).size = self.size + 1

Proof state:
α : Type u_1
lt : α → α → Bool
self : BinaryHeap α lt
x : α
⊢ (self.insert x).size = self.size + 1

Tactic:
simp [size, insert]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
@[to_additive (attr := simp)]
lemma inv_Icc (a b : α) : (Icc a b)⁻¹ = Icc b⁻¹ a⁻¹

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
a b : α
⊢ (Icc a b)⁻¹ = Icc b⁻¹ a⁻¹

Tactic:
simp [← Ici_inter_Iic, inter_comm]

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem pow_log_le_add_one (b : ℕ) : ∀ x, b ^ log b x ≤ x + 1
  | 0 => by rw [log_zero_right, Nat.pow_zero]
  | x + 1 => (pow_log_le_self b x.succ_ne_zero).trans (x + 1).le_succ

Proof state:
b : ℕ
⊢ b ^ log b 0 ≤ 0 + 1

Tactic:
rw [log_zero_right, Nat.pow_zero]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive (attr := simp) mod_card_nsmul]
lemma pow_mod_card (a : G) (n : ℕ) : a ^ (n % card G) = a ^ n

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
a : G
n : ℕ
⊢ a ^ (n % card G) = a ^ n

Tactic:
rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n orderOf_dvd_card, pow_mod_orderOf]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
@[simp] lemma neg_emod_two (i : ℤ) : -i % 2 = i % 2

Proof state:
i : ℤ
⊢ -i % 2 = i % 2

Tactic:
omega

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
lemma primesBelow_succ (n : ℕ) :
    primesBelow n.succ = if n.Prime then insert n (primesBelow n) else primesBelow n

Proof state:
n : ℕ
⊢ n.succ.primesBelow = if Prime n then insert n n.primesBelow else n.primesBelow

Tactic:
rw [primesBelow, primesBelow, Finset.range_succ, Finset.filter_insert]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_range' {start size step : Nat} {i : Nat}
    (h : i < (Array.range' start size step).size) :
    (Array.range' start size step)[i] = start + step * i

Proof state:
start size step i : Nat
h : i < (range' start size step).size
⊢ (range' start size step)[i] = start + step * i

Tactic:
simp [← getElem_toList]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Opposite.lean
theorem cokernel.π_unop :
    (cokernel.π g.unop).op =
      (cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom (Opposite.op_unop _).symm

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π g.unop).op = (cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
lemma Ico_map_sectL : (Ico a b).map (.sectL _ c) = Ico (a, c) (b, c)

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : Preorder α
inst✝³ : PartialOrder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
c : β
⊢ map (Embedding.sectL α c) (Ico a b) = Ico (a, c) (b, c)

Tactic:
aesop (add safe forward [le_antisymm, le_of_lt])

Result:
no goals
-- Mathlib/Data/Fintype/BigOperators.lean
theorem card_vector [Fintype α] (n : ℕ) :
    Fintype.card (List.Vector α n) = Fintype.card α ^ n

Proof state:
α : Type u_1
inst✝ : Fintype α
n : ℕ
⊢ Fintype.card (List.Vector α n) = Fintype.card α ^ n

Tactic:
rw [Fintype.ofEquiv_card]

Result:
α : Type u_1
inst✝ : Fintype α
n : ℕ
⊢ Fintype.card (Fin n → α) = Fintype.card α ^ n

Proof state:
α : Type u_1
inst✝ : Fintype α
n : ℕ
⊢ Fintype.card (Fin n → α) = Fintype.card α ^ n

Tactic:
simp

Result:
no goals