harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Int/Init.lean
lemma mul_dvd_of_dvd_div (hcb : c ∣ b) (h : a ∣ b / c) : c * a ∣ b :=
  have ⟨d, hd⟩ := h
  ⟨d, by simpa [Int.mul_comm, Int.mul_left_comm] using Int.eq_mul_of_ediv_eq_left hcb hd⟩

Proof state:
a b c : ℤ
hcb : c ∣ b
h : a ∣ b / c
d : ℤ
hd : b / c = a * d
⊢ b = c * a * d

Tactic:
simpa [Int.mul_comm, Int.mul_left_comm] using Int.eq_mul_of_ediv_eq_left hcb hd

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem ball_zero' (x : E) (hr : 0 < r) : ball (0 : Seminorm 𝕜 E) x r = Set.univ

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
r : ℝ
x : E
hr : 0 < r
⊢ ball 0 x r = univ

Tactic:
rw [Set.eq_univ_iff_forall, ball]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
r : ℝ
x : E
hr : 0 < r
⊢ ∀ (x_1 : E), x_1 ∈ {y | 0 (y - x) < r}

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
r : ℝ
x : E
hr : 0 < r
⊢ ∀ (x_1 : E), x_1 ∈ {y | 0 (y - x) < r}

Tactic:
simp [hr]

Result:
no goals
-- Mathlib/Data/Finset/CastCard.lean
lemma cast_card_union [AddGroupWithOne R] :
    (#(s ∪ t) : R) = #s + #t - #(s ∩ t)

Proof state:
α : Type u_1
R : Type u_3
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
⊢ ↑(#(s ∪ t)) = ↑(#s) + ↑(#t) - ↑(#(s ∩ t))

Tactic:
rw [eq_sub_iff_add_eq, ← cast_add, card_union_add_card_inter, cast_add]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem ker_eq_bot : f.ker = ⊥ ↔ Function.Injective f

Proof state:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ f.ker = ⊥ ↔ Function.Injective ⇑f

Tactic:
rw [← LieSubmodule.toSubmodule_inj, ker_toSubmodule, LieSubmodule.bot_toSubmodule,
  LinearMap.ker_eq_bot, coe_toLinearMap]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem inner_rightAngleRotation_right (x y : E) : ⟪x, J y⟫ = -ω x y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner x (o.rightAngleRotation y) = -(o.areaForm x) y

Tactic:
rw [rightAngleRotation]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner x ((LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯) y) =
    -(o.areaForm x) y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner x ((LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯) y) =
    -(o.areaForm x) y

Tactic:
exact o.inner_rightAngleRotationAux₁_right x y

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem nhds_inf (l₁ l₂ : Filter α) : 𝓝 (l₁ ⊓ l₂) = 𝓝 l₁ ⊓ 𝓝 l₂

Proof state:
α : Type u_2
l₁ l₂ : Filter α
⊢ 𝓝 (l₁ ⊓ l₂) = 𝓝 l₁ ⊓ 𝓝 l₂

Tactic:
simpa only [iInf_bool_eq] using Filter.nhds_iInf fun b => cond b l₁ l₂

Result:
no goals
-- Mathlib/Order/Filter/Partial.lean
theorem tendsto_iff_rtendsto' (l₁ : Filter α) (l₂ : Filter β) (f : α → β) :
    Tendsto f l₁ l₂ ↔ RTendsto' (Function.graph f) l₁ l₂

Proof state:
α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ RTendsto' (Function.graph f) l₁ l₂

Tactic:
simp [tendsto_def, Function.graph, rtendsto'_def, Rel.preimage_def, Set.preimage]

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem t2_iff_ultrafilter :
    T2Space X ↔ ∀ {x y : X} (f : Ultrafilter X), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y :=
  t2_iff_nhds.trans <| by simp only [← exists_ultrafilter_iff, and_imp, le_inf_iff, exists_imp]

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ {x y : X}, (𝓝 x ⊓ 𝓝 y).NeBot → x = y) ↔ ∀ {x y : X} (f : Ultrafilter X), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y

Tactic:
simp only [← exists_ultrafilter_iff, and_imp, le_inf_iff, exists_imp]

Result:
no goals
-- Mathlib/Data/Finset/Interval.lean
/-- A function `f` from `Finset α` is strictly monotone if and only if `f s < f (insert a s)` for
all `s` and `a ∉ s`. -/
lemma strictMono_iff_forall_lt_insert : StrictMono f ↔ ∀ s ⦃a⦄, a ∉ s → f s < f (insert a s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
f : Finset α → β
inst✝ : DecidableEq α
⊢ StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄, a ∉ s → f s < f (insert a s)

Tactic:
simp [strictMono_iff_forall_lt_cons]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
lemma prod_apply (s : Set (α × β)) (s_mble : MeasurableSet s) :
    μ.prod ν s = ENNReal.toNNReal (∫⁻ x, ν.toMeasure (Prod.mk x ⁻¹' s) ∂μ)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
s : Set (α × β)
s_mble : MeasurableSet s
⊢ (μ.prod ν) s = (∫⁻ (x : α), ↑ν (Prod.mk x ⁻¹' s) ∂↑μ).toNNReal

Tactic:
simp [coeFn_def, Measure.prod_apply s_mble]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem getRight?_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
    (x.map f g).getRight? = x.getRight?.map g

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
x : α ⊕ γ
⊢ (Sum.map f g x).getRight? = Option.map g x.getRight?

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem card_support_binomial {k m : ℕ} (h : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) :
    #(support (C x * X ^ k + C y * X ^ m)) = 2

Proof state:
R : Type u
inst✝ : Semiring R
k m : ℕ
h : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ #(C x * X ^ k + C y * X ^ m).support = 2

Tactic:
rw [support_binomial h hx hy, card_insert_of_not_mem (mt mem_singleton.mp h), card_singleton]

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem div {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x / y)

Proof state:
R : Type u_1
inst✝¹ : Semifield R
inst✝ : StarRing R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x / y)

Tactic:
simp only [isSelfAdjoint_iff, star_div₀, hx.star_eq, hy.star_eq]

Result:
no goals
-- Mathlib/NumberTheory/EulerProduct/Basic.lean
/-- We relate a finite product over primes to an infinite sum over smooth numbers. -/
lemma summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum
    (hsum : ∀ {p : ℕ}, p.Prime → Summable (fun n : ℕ ↦ ‖f (p ^ n)‖)) (N : ℕ) :
    Summable (fun m : N.smoothNumbers ↦ ‖f m‖) ∧
      HasSum (fun m : N.smoothNumbers ↦ f m) (∏ p ∈ N.primesBelow, ∑' n : ℕ, f (p ^ n))

Proof state:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
N : ℕ
⊢ (Summable fun m => ‖f ↑m‖) ∧
    HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) (range N), ∑' (n : ℕ), f (p ^ n))

Tactic:
exact summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum hf₁ hmul hsum _

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
N : ℕ
⊢ (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ N.primesBelow, ∑' (n : ℕ), f (p ^ n))

Tactic:
rw [smoothNumbers_eq_factoredNumbers, primesBelow]

Result:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖
N : ℕ
⊢ (Summable fun m => ‖f ↑m‖) ∧
    HasSum (fun m => f ↑m) (∏ p ∈ filter (fun p => Nat.Prime p) (range N), ∑' (n : ℕ), f (p ^ n))
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractRight_contractRight (x : CliffordAlgebra Q) : x⌊d⌊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
x : CliffordAlgebra Q
⊢ (contractRight ((contractRight x) d)) d = 0

Tactic:
rw [contractRight_eq, contractRight_eq, reverse_reverse, contractLeft_contractLeft, map_zero]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem natCast_mod (m n : ℕ) : ((m % n : ℕ) : Ordinal) = m % n

Proof state:
m n : ℕ
⊢ ↑(m % n) = ↑m % ↑n

Tactic:
rw [← add_left_cancel_iff, div_add_mod, ← natCast_div, ← natCast_mul, ← Nat.cast_add,
  Nat.div_add_mod]

Result:
no goals
-- Mathlib/RingTheory/DividedPowers/Basic.lean
theorem dpow_eval_zero {n : ℕ} (hn : n ≠ 0) : hI.dpow n 0 = 0

Proof state:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n 0 = 0

Tactic:
rw [← MulZeroClass.mul_zero (0 : A), hI.dpow_mul I.zero_mem,
  zero_pow hn, zero_mul, zero_mul]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
@[to_additive]
lemma isPeriodicPt_smul_iff {m : M} {a : α} {n : ℕ} :
    IsPeriodicPt (m • ·) n a ↔ m ^ n • a = a

Proof state:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
n : ℕ
⊢ IsPeriodicPt (fun x => m • x) n a ↔ m ^ n • a = a

Tactic:
rw [← smul_iterate_apply, IsPeriodicPt, IsFixedPt]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/ConformalLinearMap.lean
theorem injective {f : M' →L[R] N} (h : IsConformalMap f) : Function.Injective f

Proof state:
case intro.intro.intro
R : Type u_1
N : Type u_3
M' : Type u_5
inst✝⁴ : NormedField R
inst✝³ : SeminormedAddCommGroup N
inst✝² : NormedSpace R N
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
c : R
hc : c ≠ 0
li : M' →ₗᵢ[R] N
⊢ Injective ⇑(c • li.toContinuousLinearMap)

Tactic:
exact (smul_right_injective _ hc).comp li.injective

Result:
no goals

Proof state:
R : Type u_1
N : Type u_3
M' : Type u_5
inst✝⁴ : NormedField R
inst✝³ : SeminormedAddCommGroup N
inst✝² : NormedSpace R N
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
f : M' →L[R] N
h : IsConformalMap f
⊢ Injective ⇑f

Tactic:
rcases h with ⟨c, hc, li, rfl⟩

Result:
case intro.intro.intro
R : Type u_1
N : Type u_3
M' : Type u_5
inst✝⁴ : NormedField R
inst✝³ : SeminormedAddCommGroup N
inst✝² : NormedSpace R N
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
c : R
hc : c ≠ 0
li : M' →ₗᵢ[R] N
⊢ Injective ⇑(c • li.toContinuousLinearMap)
-- Mathlib/Data/Rat/Defs.lean
theorem zero_iff_num_zero {q : ℚ} : q = 0 ↔ q.num = 0 :=
  ⟨fun _ => by simp [*], zero_of_num_zero⟩

Proof state:
q : ℚ
x✝ : q = 0
⊢ q.num = 0

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem symm_constVSub (p : P) :
    (constVSub 𝕜 p).symm =
      (LinearIsometryEquiv.neg 𝕜).toAffineIsometryEquiv.trans (vaddConst 𝕜 p)

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p : P
⊢ (constVSub 𝕜 p).symm = (LinearIsometryEquiv.neg 𝕜).toAffineIsometryEquiv.trans (vaddConst 𝕜 p)

Tactic:
ext

Result:
case h
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p : P
x✝ : V
⊢ (constVSub 𝕜 p).symm x✝ = ((LinearIsometryEquiv.neg 𝕜).toAffineIsometryEquiv.trans (vaddConst 𝕜 p)) x✝

Proof state:
case h
𝕜 : Type u_1
V : Type u_2
P : Type u_10
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
p : P
x✝ : V
⊢ (constVSub 𝕜 p).symm x✝ = ((LinearIsometryEquiv.neg 𝕜).toAffineIsometryEquiv.trans (vaddConst 𝕜 p)) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/WittVector/Frobenius.lean
theorem map_frobeniusPoly.key₁ (n j : ℕ) (hj : j < p ^ n) :
    p ^ (n - v p (j + 1)) ∣ (p ^ n).choose (j + 1)

Proof state:
case hk
p : ℕ
hp : Fact (Nat.Prime p)
n j : ℕ
hj : j < p ^ n
⊢ ↑(n - v p (j + 1)) ≤ emultiplicity p ((p ^ n).choose (j + 1))

Tactic:
rw [hp.out.emultiplicity_choose_prime_pow hj j.succ_ne_zero]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n j : ℕ
hj : j < p ^ n
⊢ p ^ (n - v p (j + 1)) ∣ (p ^ n).choose (j + 1)

Tactic:
apply pow_dvd_of_le_emultiplicity

Result:
case hk
p : ℕ
hp : Fact (Nat.Prime p)
n j : ℕ
hj : j < p ^ n
⊢ ↑(n - v p (j + 1)) ≤ emultiplicity p ((p ^ n).choose (j + 1))
-- Mathlib/Analysis/InnerProductSpace/OfNorm.lean
theorem add_left_aux4 (y z : E) :
    ‖y‖ * ‖y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpaceable E
y z : E
⊢ ‖y‖ * ‖y‖ + ‖y - 2 • z‖ * ‖y - 2 • z‖ = 2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖)

Tactic:
convert parallelogram_identity (y - z) z using 4 <;> abel

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Bell.lean
theorem uniformBell_zero_left (n : ℕ) : uniformBell 0 n = 1

Proof state:
n : ℕ
⊢ uniformBell 0 n = 1

Tactic:
simp [uniformBell_eq]

Result:
no goals
-- Mathlib/Data/List/Iterate.lean
theorem range_map_iterate (n : ℕ) (f : α → α) (a : α) :
    (List.range n).map (f^[·] a) = List.iterate f a n

Proof state:
α : Type u_1
n : ℕ
f : α → α
a : α
⊢ map (fun x => f^[x] a) (range n) = iterate f a n

Tactic:
apply List.ext_getElem <;> simp

Result:
no goals
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.closedCell_zero_eq_singleton [RelCWComplex C D] {j : cell C 0} :
    closedCell 0 j = {map 0 j ![]}

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
j : cell C 0
⊢ closedCell 0 j = {↑(map 0 j) ![]}

Tactic:
simp [closedCell, Matrix.empty_eq]

Result:
no goals
-- Mathlib/Data/String/Lemmas.lean
lemma leftpad_prefix (n : ℕ) (c : Char) : ∀ s, IsPrefix (replicate (n - length s) c) (leftpad n c s)
  | ⟨l⟩ => by simp only [IsPrefix, replicate, leftpad, String.length, List.leftpad_prefix]

Proof state:
n : ℕ
c : Char
l : List Char
⊢ (replicate (n - { data := l }.length) c).IsPrefix (leftpad n c { data := l })

Tactic:
simp only [IsPrefix, replicate, leftpad, String.length, List.leftpad_prefix]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem natAbs_mul_natAbs_eq {a b : Int} {c : Nat}
    (h : a * b = (c : Int)) : a.natAbs * b.natAbs = c

Proof state:
a b : Int
c : Nat
h : a * b = ↑c
⊢ a.natAbs * b.natAbs = c

Tactic:
rw [← natAbs_mul, h, natAbs.eq_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem zipIdx_eq_zip_range' (l : Array α) {n : Nat} : l.zipIdx n = l.zip (range' n l.size)

Proof state:
α : Type u_1
l : Array α
n : Nat
⊢ l.zipIdx n = l.zip (range' n l.size)

Tactic:
simp [zip_of_prod (zipIdx_map_fst _ _) (zipIdx_map_snd _ _)]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Covering.lean
theorem Prefunctor.IsCovering.symmetrify (hφ : φ.IsCovering) :
    φ.symmetrify.IsCovering

Proof state:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
⊢ φ.symmetrify.IsCovering

Tactic:
refine ⟨fun u => ?_, fun u => ?_⟩ <;>
  simp only [φ.symmetrifyStar, φ.symmetrifyCostar] <;>
  erw [EquivLike.comp_bijective, EquivLike.bijective_comp] <;>
  simp [hφ.star_bijective u, hφ.costar_bijective u]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem vectorSpan_eq_span_vsub_set_right_ne {s : Set P} {p : P} (hp : p ∈ s) :
    vectorSpan k s = Submodule.span k ((· -ᵥ p) '' (s \ {p}))

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (insert (p -ᵥ p) ((fun x => x -ᵥ p) '' (s \ {p}))) =
    Submodule.span k ((fun x => x -ᵥ p) '' (s \ {p}))

Tactic:
simp [Submodule.span_insert_eq_span]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
⊢ vectorSpan k s = Submodule.span k ((fun x => x -ᵥ p) '' (s \ {p}))

Tactic:
conv_lhs =>
  rw [vectorSpan_eq_span_vsub_set_right k hp, ← Set.insert_eq_of_mem hp, ←
    Set.insert_diff_singleton, Set.image_insert_eq]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
hp : p ∈ s
⊢ Submodule.span k (insert (p -ᵥ p) ((fun x => x -ᵥ p) '' (s \ {p}))) =
    Submodule.span k ((fun x => x -ᵥ p) '' (s \ {p}))
-- Mathlib/LinearAlgebra/Prod.lean
theorem range_fst : range (fst R M M₂) = ⊤

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ range (fst R M M₂) = ⊤

Tactic:
rw [range_eq_map, ← prod_top, prod_map_fst]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_le_length_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
    l.length ≤ (insertEntryIfNew k v l).length

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ l.length ≤ if containsKey k l = true then l.length else l.length + 1

Tactic:
split <;> omega

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ l.length ≤ (insertEntryIfNew k v l).length

Tactic:
rw [length_insertEntryIfNew]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ l.length ≤ if containsKey k l = true then l.length else l.length + 1
-- Mathlib/Algebra/Order/Antidiag/Finsupp.lean
@[simp] lemma mem_finsuppAntidiag : f ∈ finsuppAntidiag s n ↔ s.sum f = n ∧ f.support ⊆ s

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι →₀ μ
⊢ f ∈ s.finsuppAntidiag n ↔ s.sum ⇑f = n ∧ f.support ⊆ s

Tactic:
simp [finsuppAntidiag, ← DFunLike.coe_fn_eq, subset_iff]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem card_fintypeIoo : Fintype.card (Set.Ioo a b) = b - a - 1

Proof state:
n : ℕ
a b : Fin n
⊢ Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1

Tactic:
rw [← card_Ioo, Fintype.card_ofFinset]

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
lemma adjoin_eq_span (s : Set A) :
    Subalgebra.toSubmodule (adjoin R s).toSubalgebra = span R (Submonoid.closure (s ∪ star s))

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
⊢ Subalgebra.toSubmodule (adjoin R s).toSubalgebra = span R ↑(Submonoid.closure (s ∪ star s))

Tactic:
rw [adjoin_toSubalgebra, Algebra.adjoin_eq_span]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem isLUB_biSup {s : Set β} {f : β → α} : IsLUB (f '' s) (⨆ x ∈ s, f x)

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

Tactic:
simpa only [range_comp, Subtype.range_coe, iSup_subtype'] using
  @isLUB_iSup α s _ (f ∘ fun x => (x : β))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_emod_right (a b : Int) : (a * b) % a = 0

Proof state:
a b : Int
⊢ a * b % a = 0

Tactic:
rw [Int.mul_comm, mul_emod_left]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem norm_div_cos_oangle_sub_left_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : ‖x‖ / Real.Angle.cos (o.oangle (x - y) x) = ‖x - y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖x‖ / ((-o).oangle x (x - y)).cos = ‖x - y‖

Tactic:
exact (-o).norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two h

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ ‖x‖ / (o.oangle (x - y) x).cos = ‖x - y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖x‖ / ((-o).oangle x (x - y)).cos = ‖x - y‖
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Lemmas.lean
theorem div_eq_iff (h : 0 < k) : x / k = y ↔ x ≤ y * k + k - 1 ∧ y * k ≤ x

Proof state:
k x y : Nat
h : 0 < k
⊢ x / k = y ↔ x ≤ y * k + k - 1 ∧ y * k ≤ x

Tactic:
rw [Nat.eq_iff_le_and_ge, le_div_iff_mul_le h, Nat.div_le_iff_le_mul h]

Result:
no goals
-- Mathlib/Computability/ContextFreeGrammar.lean
@[simp] lemma generates_reverse_comm : g.reverse.Generates u ↔ g.Generates u.reverse

Proof state:
T : Type u_1
g : ContextFreeGrammar T
u : List (Symbol T g.NT)
⊢ g.reverse.Generates u ↔ g.Generates u.reverse

Tactic:
simp [Generates]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem smul_integral_comp_sub_mul (c d) :
    (c • ∫ x in a..b, f (d - c * x)) = ∫ x in d - c * b..d - c * a, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
⊢ c • ∫ (x : ℝ) in a..b, f (d - c * x) = ∫ (x : ℝ) in d - c * b..d - c * a, f x

Tactic:
by_cases hc : c = 0 <;> simp [hc, integral_comp_sub_mul]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem AlgebraicIndependent.image {ι} {s : Set ι} {f : ι → A}
    (hs : AlgebraicIndependent R fun x : s => f x) :
    AlgebraicIndependent R fun x : f '' s => (x : A)

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_7
s : Set ι
f : ι → A
hs : AlgebraicIndependent R fun x => f ↑x
⊢ AlgebraicIndependent R fun x => ↑x

Tactic:
convert AlgebraicIndependent.image_of_comp s f id hs

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem isLindelof_singleton {x : X} : IsLindelof ({x} : Set X) := fun _ hf _ hfa ↦
  ⟨x, rfl, ClusterPt.of_le_nhds'
    (hfa.trans <| by simpa only [principal_singleton] using pure_le_nhds x) hf⟩

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
x✝¹ : Filter X
hf : x✝¹.NeBot
x✝ : CountableInterFilter x✝¹
hfa : x✝¹ ≤ 𝓟 {x}
⊢ 𝓟 {x} ≤ 𝓝 x

Tactic:
simpa only [principal_singleton] using pure_le_nhds x

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_eq_getKey! [BEq α] [Inhabited α] {l : List ((a : α) × β a)} {a : α}
    (h : containsKey a l = true) : getKey a l h = getKey! a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Inhabited α
l : List ((a : α) × β a)
a : α
h : containsKey a l = true
⊢ getKey a l h = getKey! a l

Tactic:
rw [getKey!_eq_getKey?, getKey, Option.get_eq_get!]

Result:
no goals
-- Mathlib/Probability/Kernel/WithDensity.lean
theorem withDensity_apply' (κ : Kernel α β) [IsSFiniteKernel κ]
    (hf : Measurable (Function.uncurry f)) (a : α) (s : Set β) :
    withDensity κ f a s = ∫⁻ b in s, f a b ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
s : Set β
⊢ ((κ.withDensity f) a) s = ∫⁻ (b : β) in s, f a b ∂κ a

Tactic:
rw [Kernel.withDensity_apply κ hf, withDensity_apply' _ s]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mk_add_mem_zipIdx_iff_getElem? {k i : Nat} {x : α} {l : List α} :
    (x, k + i) ∈ zipIdx l k ↔ l[i]? = some x

Proof state:
α : Type u_1
k i : Nat
x : α
l : List α
⊢ (x, k + i) ∈ l.zipIdx k ↔ l[i]? = some x

Tactic:
simp [mem_iff_getElem?, and_left_comm]

Result:
no goals