harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem toAddMonoidHom_injective :
    Function.Injective (@NormedAddGroupHom.toAddMonoidHom V₁ V₂ _ _) := fun f g h =>
  coe_inj <| by rw [← coe_toAddMonoidHom f, ← coe_toAddMonoidHom g, h]

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
h : f.toAddMonoidHom = g.toAddMonoidHom
⊢ ⇑f = ⇑g

Tactic:
rw [← coe_toAddMonoidHom f, ← coe_toAddMonoidHom g, h]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem orthonormal_empty : Orthonormal 𝕜 (fun x => x : (∅ : Set E) → E)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ Orthonormal 𝕜 fun x => ↑x

Tactic:
simp [orthonormal_subtype_iff_ite]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ Orthonormal 𝕜 fun x => ↑x

Tactic:
classical
simp [orthonormal_subtype_iff_ite]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem boundedBy_eq (s : Set α) (m_empty : m ∅ = 0) (m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t)
    (m_subadd : ∀ s : ℕ → Set α, m (⋃ i, s i) ≤ ∑' i, m (s i)) : boundedBy m s = m s

Proof state:
α : Type u_1
m : Set α → ℝ≥0∞
s : Set α
m_empty : m ∅ = 0
m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t
m_subadd : ∀ (s : ℕ → Set α), m (⋃ i, s i) ≤ ∑' (i : ℕ), m (s i)
⊢ (boundedBy m) s = m s

Tactic:
rw [boundedBy_eq_ofFunction m_empty, ofFunction_eq s m_mono m_subadd]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
lemma isRoot_comp {R} [CommSemiring R] {p q : R[X]} {r : R} :
    (p.comp q).IsRoot r ↔ p.IsRoot (q.eval r)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ (p.comp q).IsRoot r ↔ p.IsRoot (eval r q)

Tactic:
simp_rw [IsRoot, eval_comp]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem bind_decode_iff {f : α → β → Option σ} :
    (Primrec₂ fun a n => (@decode β _ n).bind (f a)) ↔ Primrec₂ f :=
  ⟨fun h => by simpa [encodek] using h.comp fst ((@Primrec.encode β _).comp snd), fun h =>
    option_bind (Primrec.decode.comp snd) <| h.comp (fst.comp fst) snd⟩

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → Option σ
h : Primrec₂ fun a n => (decode n).bind (f a)
⊢ Primrec₂ f

Tactic:
simpa [encodek] using h.comp fst ((@Primrec.encode β _).comp snd)

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem Rel.neg {R : Type uR} [Ring R] {r : R → R → Prop} ⦃a b : R⦄ (h : Rel r a b) :
    Rel r (-a) (-b)

Proof state:
R : Type uR
inst✝ : Ring R
r : R → R → Prop
a b : R
h : Rel r a b
⊢ Rel r (-a) (-b)

Tactic:
simp only [neg_eq_neg_one_mul a, neg_eq_neg_one_mul b, Rel.mul_right h]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
@[simp]
lemma trailingDegree_X_pow (n : ℕ) :
    (X ^ n : R[X]).trailingDegree = n

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).trailingDegree = ↑n

Tactic:
rw [X_pow_eq_monomial, trailingDegree_monomial one_ne_zero]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleFactorsFinset_one : cycleFactorsFinset (1 : Perm α) = ∅

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ cycleFactorsFinset 1 = ∅

Tactic:
simp [cycleFactorsFinset_eq_empty_iff]

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem not_lt_zero : ¬a < 0

Proof state:
a : ℝ≥0∞
⊢ ¬a < 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem order_monomial_of_ne_zero {d : σ →₀ ℕ} {a : R} (h : a ≠ 0) :
    order (monomial R d a) = degree d

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
d : σ →₀ ℕ
a : R
h : a ≠ 0
⊢ ((monomial R d) a).order = ↑d.degree

Tactic:
rw [degree_eq_weight_one]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
d : σ →₀ ℕ
a : R
h : a ≠ 0
⊢ ((monomial R d) a).order = ↑((weight fun x => 1) d)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
d : σ →₀ ℕ
a : R
h : a ≠ 0
⊢ ((monomial R d) a).order = ↑((weight fun x => 1) d)

Tactic:
exact weightedOrder_monomial_of_ne_zero _ h

Result:
no goals
-- Mathlib/Analysis/Calculus/Monotone.lean
theorem Monotone.ae_differentiableAt {f : ℝ → ℝ} (hf : Monotone f) :
    ∀ᵐ x, DifferentiableAt ℝ f x

Proof state:
f : ℝ → ℝ
hf : Monotone f
⊢ ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x

Tactic:
filter_upwards [hf.ae_hasDerivAt] with x hx using hx.differentiableAt

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem exists_of_mem_mapFinIdx {b : β} {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β}
    (h : b ∈ l.mapFinIdx f) : ∃ (i : Nat) (h : i < l.size), f i l[i] h = b

Proof state:
case mk
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
h : b ∈ { toList := l }.mapFinIdx f
⊢ ∃ i h, f i { toList := l }[i] h = b

Tactic:
exact List.exists_of_mem_mapFinIdx (by simpa using h)

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
b : β
l : Array α
f : (i : Nat) → α → i < l.size → β
h : b ∈ l.mapFinIdx f
⊢ ∃ i h, f i l[i] h = b

Tactic:
rcases l with ⟨l⟩

Result:
case mk
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
h : b ∈ { toList := l }.mapFinIdx f
⊢ ∃ i h, f i { toList := l }[i] h = b

Proof state:
β : Type u_1
α : Type u_2
b : β
l : List α
f : (i : Nat) → α → i < { toList := l }.size → β
h : b ∈ { toList := l }.mapFinIdx f
⊢ b ∈ { toList := l }.toList.mapFinIdx f

Tactic:
simpa using h

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem coeFn_mk (f : α → β) (hf) : (mk f hf : α →ₘ[μ] β) =ᵐ[μ] f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ↑(mk f hf) =ᶠ[ae μ] f

Tactic:
rw [← mk_eq_mk, mk_coeFn]

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem isSeparable_closure : IsSeparable (closure s) ↔ IsSeparable s

Proof state:
α : Type u
t : TopologicalSpace α
s : Set α
⊢ IsSeparable (closure s) ↔ IsSeparable s

Tactic:
simp only [IsSeparable, isClosed_closure.closure_subset_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem continuousOn_mul [LocallyCompactSpace X] [T2Space X] [NormedRing R]
    [SecondCountableTopologyEither X R] {f g : X → R} {s : Set X} (hf : LocallyIntegrableOn f s μ)
    (hg : ContinuousOn g s) (hs : IsLocallyClosed s) :
    LocallyIntegrableOn (fun x => g x * f x) s μ

Proof state:
X : Type u_1
R : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn (fun x => g x * f x) k μ

Tactic:
exact fun k hk_sub hk_c => (hf k hk_sub hk_c).continuousOn_mul (hg.mono hk_sub) hk_c

Result:
no goals

Proof state:
X : Type u_1
R : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ LocallyIntegrableOn (fun x => g x * f x) s μ

Tactic:
rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢

Result:
X : Type u_1
R : Type u_5
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
μ : Measure X
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : LocallyCompactSpace X
inst✝² : T2Space X
inst✝¹ : NormedRing R
inst✝ : SecondCountableTopologyEither X R
f g : X → R
s : Set X
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
hs : IsLocallyClosed s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn (fun x => g x * f x) k μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_of_forall_getElem_not {l : Array α} (h : ∀ i, (h : i < l.size) → ¬p l[i]) : l.eraseP p = l :=
  eraseP_of_forall_mem_not fun a m => by
    rw [mem_iff_getElem] at m
    obtain ⟨i, w, rfl⟩ := m
    exact h i w

Proof state:
α : Type u_1
p : α → Bool
l : Array α
h : ∀ (i : Nat) (h : i < l.size), ¬p l[i] = true
a : α
m : a ∈ l
⊢ ¬p a = true

Tactic:
rw [mem_iff_getElem] at m

Result:
α : Type u_1
p : α → Bool
l : Array α
h : ∀ (i : Nat) (h : i < l.size), ¬p l[i] = true
a : α
m : ∃ i h, l[i] = a
⊢ ¬p a = true

Proof state:
case intro.intro
α : Type u_1
p : α → Bool
l : Array α
h : ∀ (i : Nat) (h : i < l.size), ¬p l[i] = true
i : Nat
w : i < l.size
⊢ ¬p l[i] = true

Tactic:
exact h i w

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : Array α
h : ∀ (i : Nat) (h : i < l.size), ¬p l[i] = true
a : α
m : ∃ i h, l[i] = a
⊢ ¬p a = true

Tactic:
obtain ⟨i, w, rfl⟩ := m

Result:
case intro.intro
α : Type u_1
p : α → Bool
l : Array α
h : ∀ (i : Nat) (h : i < l.size), ¬p l[i] = true
i : Nat
w : i < l.size
⊢ ¬p l[i] = true
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem coeff_one [Nontrivial S] (h : IsAdjoinRootMonic S f) : h.coeff 1 = Pi.single 0 1

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
h : IsAdjoinRootMonic S f
⊢ h.coeff 1 = Pi.single 0 1

Tactic:
rw [← h.coeff_root_pow h.deg_pos, pow_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem modify_eq [BEq α] [LawfulBEq α] [Hashable α] {m : Raw α β} (h : m.WF) {k : α} {f : β k → β k} :
    m.modify k f = Raw₀.modify ⟨m, h.size_buckets_pos⟩ k f

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
k : α
f : β k → β k
⊢ m.modify k f = (Raw₀.modify ⟨m, ⋯⟩ k f).val

Tactic:
simp [Raw.modify, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem inf_eq_left : a ⊓ b = a ↔ a ≤ b :=
  le_antisymm_iff.trans <| by simp [le_rfl]

Proof state:
α : Type u
inst✝ : SemilatticeInf α
a b : α
⊢ a ⊓ b ≤ a ∧ a ≤ a ⊓ b ↔ a ≤ b

Tactic:
simp [le_rfl]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem mul_limZero_right (f : CauSeq β abv) {g} (hg : LimZero g) : LimZero (f * g)
  | ε, ε0 =>
    let ⟨F, F0, hF⟩ := f.bounded' 0
    (hg _ <| div_pos ε0 F0).imp fun _ H j ij => by
      have := mul_lt_mul' (le_of_lt <| hF j) (H _ ij) (abv_nonneg abv _) F0
      rwa [mul_comm F, div_mul_cancel₀ _ (ne_of_gt F0), ← abv_mul] at this

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : g.LimZero
ε : α
ε0 : ε > 0
F : α
F0 : F > 0
hF : ∀ (i : ℕ), abv (↑f i) < F
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑g j) < ε / F
j : ℕ
ij : j ≥ x✝
this : abv (↑f j) * abv (↑g j) < F * (ε / F)
⊢ abv (↑(f * g) j) < ε

Tactic:
rwa [mul_comm F, div_mul_cancel₀ _ (ne_of_gt F0), ← abv_mul] at this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : g.LimZero
ε : α
ε0 : ε > 0
F : α
F0 : F > 0
hF : ∀ (i : ℕ), abv (↑f i) < F
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑g j) < ε / F
j : ℕ
ij : j ≥ x✝
⊢ abv (↑(f * g) j) < ε

Tactic:
have := mul_lt_mul' (le_of_lt <| hF j) (H _ ij) (abv_nonneg abv _) F0

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : CauSeq β abv
hg : g.LimZero
ε : α
ε0 : ε > 0
F : α
F0 : F > 0
hF : ∀ (i : ℕ), abv (↑f i) < F
x✝ : ℕ
H : ∀ j ≥ x✝, abv (↑g j) < ε / F
j : ℕ
ij : j ≥ x✝
this : abv (↑f j) * abv (↑g j) < F * (ε / F)
⊢ abv (↑(f * g) j) < ε
-- Mathlib/Data/Matroid/Restrict.lean
theorem restrict_ground_eq_self (M : Matroid α) : (M ↾ M.E) = M

Proof state:
α : Type u_1
M : Matroid α
⊢ ∀ ⦃I : Set α⦄, I ⊆ (M ↾ M.E).E → ((M ↾ M.E).Indep I ↔ M.Indep I)

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
⊢ M ↾ M.E = M

Tactic:
refine ext_indep rfl ?_

Result:
α : Type u_1
M : Matroid α
⊢ ∀ ⦃I : Set α⦄, I ⊆ (M ↾ M.E).E → ((M ↾ M.E).Indep I ↔ M.Indep I)
-- Mathlib/Algebra/Group/Prod.lean
theorem prod_unique (f : M →* N × P) : ((fst N P).comp f).prod ((snd N P).comp f) = f :=
  ext fun x => by simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Proof state:
M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : M →* N × P
x : M
⊢ (((fst N P).comp f).prod ((snd N P).comp f)) x = f x

Tactic:
simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem hasStrictDerivAt_of_bilinear (hu : HasStrictDerivAt u u' x) (hv : HasStrictDerivAt v v' x) :
    HasStrictDerivAt (fun x ↦ B (u x) (v x)) (B (u x) v' + B u' (v x)) x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : HasStrictDerivAt u u' x
hv : HasStrictDerivAt v v' x
⊢ HasStrictDerivAt (fun x => (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x

Tactic:
simpa using
  (B.hasStrictFDerivAt_of_bilinear hu.hasStrictFDerivAt hv.hasStrictFDerivAt).hasStrictDerivAt

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem r_of_eq {x y : M × S} (h : ↑y.2 * x.1 = ↑x.2 * y.1) : r S x y :=
  r_iff_exists.2 ⟨1, by rw [h]⟩

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
h : ↑y.2 * x.1 = ↑x.2 * y.1
⊢ ↑1 * (↑y.2 * x.1) = ↑1 * (↑x.2 * y.1)

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem star_add_self : star a + a = 2 * a.re + c₂ * a.imI

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a + a = 2 * ↑a.re + ↑c₂ * ↑a.imI

Tactic:
rw [add_comm, self_add_star]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Power2.lean
theorem one_isPowerOfTwo : isPowerOfTwo 1 :=
  ⟨0, by decide⟩

Proof state:
⊢ 1 = 2 ^ 0

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Basic.lean
theorem coe_decompose_mul_of_left_mem_zero [AddMonoid ι] [GradedRing 𝒜] {a b : A}
    (a_mem : a ∈ 𝒜 0) : (decompose 𝒜 (a * b) j : A) = a * decompose 𝒜 b j

Proof state:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
j : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
b : A
a : ↥(𝒜 0)
⊢ ↑(((decompose 𝒜) (↑a * b)) j) = ↑a * ↑(((decompose 𝒜) b) j)

Tactic:
rw [decompose_mul, decompose_coe, coe_of_mul_apply_of_mem_zero]

Result:
no goals

Proof state:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
j : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
a b : A
a_mem : a ∈ 𝒜 0
⊢ ↑(((decompose 𝒜) (a * b)) j) = a * ↑(((decompose 𝒜) b) j)

Tactic:
lift a to 𝒜 0 using a_mem

Result:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
j : ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
b : A
a : ↥(𝒜 0)
⊢ ↑(((decompose 𝒜) (↑a * b)) j) = ↑a * ↑(((decompose 𝒜) b) j)
-- Mathlib/Algebra/Ring/Units.lean
theorem divp_add (a b : α) (u : αˣ) : a /ₚ u + b = (a + b * u) /ₚ u

Proof state:
α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a /ₚ u + b = (a + b * ↑u) /ₚ u

Tactic:
simp only [divp, add_mul, Units.mul_inv_cancel_right]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
lemma ContinuousMap.integral_apply [NormedSpace ℝ E] [CompleteSpace E] {f : X → C(Y, E)}
    (hf : Integrable f μ) (y : Y) : (∫ x, f x ∂μ) y = ∫ x, f x y ∂μ

Proof state:
X : Type u_1
Y : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace X
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace Y
inst✝² : CompactSpace Y
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : X → C(Y, E)
hf : Integrable f μ
y : Y
⊢ (∫ (x : X), f x ∂μ) y = ∫ (x : X), (f x) y ∂μ

Tactic:
calc (∫ x, f x ∂μ) y = ContinuousMap.evalCLM ℝ y (∫ x, f x ∂μ) := rfl
  _ = ∫ x, ContinuousMap.evalCLM ℝ y (f x) ∂μ :=
        (ContinuousLinearMap.integral_comp_comm _ hf).symm
  _ = _ := rfl

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Polar.lean
theorem polar_eq_iInter {s : Set E} : B.polar s = ⋂ x ∈ s, { y : F | ‖B x y‖ ≤ 1 }

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x✝ : F
⊢ x✝ ∈ B.polar s ↔ x✝ ∈ ⋂ x ∈ s, {y | ‖(B x) y‖ ≤ 1}

Tactic:
simp only [polar_mem_iff, Set.mem_iInter, Set.mem_setOf_eq]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ B.polar s = ⋂ x ∈ s, {y | ‖(B x) y‖ ≤ 1}

Tactic:
ext

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x✝ : F
⊢ x✝ ∈ B.polar s ↔ x✝ ∈ ⋂ x ∈ s, {y | ‖(B x) y‖ ≤ 1}
-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem measure_iUnion_fintype_le [Fintype ι] (μ : F) (s : ι → Set α) :
    μ (⋃ i, s i) ≤ ∑ i, μ (s i)

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Fintype ι
μ : F
s : ι → Set α
⊢ μ (⋃ i, s i) ≤ ∑ i : ι, μ (s i)

Tactic:
simpa using measure_biUnion_finset_le Finset.univ s

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem dotProduct_smul [SMulCommClass R α α] (x : R) (v w : m → α) :
    v ⬝ᵥ x • w = x • (v ⬝ᵥ w)

Proof state:
m : Type u_2
R : Type u_7
α : Type v
inst✝⁵ : Fintype m
inst✝⁴ : Monoid R
inst✝³ : Mul α
inst✝² : AddCommMonoid α
inst✝¹ : DistribMulAction R α
inst✝ : SMulCommClass R α α
x : R
v w : m → α
⊢ v ⬝ᵥ x • w = x • (v ⬝ᵥ w)

Tactic:
simp [dotProduct, Finset.smul_sum, mul_smul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem get_find?_mem {xs : Vector α n} (h) : (xs.find? p).get h ∈ xs

Proof state:
α : Type
n : Nat
p : α → Bool
xs : Vector α n
h : (find? p xs).isSome = true
⊢ (find? p xs).get h ∈ xs

Tactic:
cases xs

Result:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : (find? p { toArray := toArray✝, size_toArray := size_toArray✝ }).isSome = true
⊢ (find? p { toArray := toArray✝, size_toArray := size_toArray✝ }).get h ∈
    { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : (find? p { toArray := toArray✝, size_toArray := size_toArray✝ }).isSome = true
⊢ (find? p { toArray := toArray✝, size_toArray := size_toArray✝ }).get h ∈
    { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp [Array.get_find?_mem]

Result:
no goals
-- Mathlib/Data/Finsupp/AList.lean
theorem insert_lookupFinsupp [DecidableEq α] (l : AList fun _x : α => M) (a : α) (m : M) :
    (l.insert a m).lookupFinsupp = l.lookupFinsupp.update a m

Proof state:
case h
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
b : α
⊢ (insert a m l).lookupFinsupp b = (l.lookupFinsupp.update a m) b

Tactic:
by_cases h : b = a <;> simp [h]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
⊢ (insert a m l).lookupFinsupp = l.lookupFinsupp.update a m

Tactic:
ext b

Result:
case h
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
b : α
⊢ (insert a m l).lookupFinsupp b = (l.lookupFinsupp.update a m) b
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem vadd_right_mem_affineSpan_pair {p₁ p₂ : P} {v : V} :
    v +ᵥ p₂ ∈ line[k, p₁, p₂] ↔ ∃ r : k, r • (p₁ -ᵥ p₂) = v

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
p₁ p₂ : P
v : V
⊢ v +ᵥ p₂ ∈ affineSpan k {p₁, p₂} ↔ ∃ r, r • (p₁ -ᵥ p₂) = v

Tactic:
rw [vadd_mem_iff_mem_direction _ (right_mem_affineSpan_pair _ _ _), direction_affineSpan,
  mem_vectorSpan_pair]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean
lemma centralizer_coe_sup (S T : Subalgebra R A) :
    centralizer R ((S ⊔ T : Subalgebra R A) : Set A) = centralizer R S ⊓ centralizer R T :=
  eq_of_forall_le_iff fun K ↦ by
    simp_rw [le_centralizer_iff, sup_le_iff, le_inf_iff, K.le_centralizer_iff]

Proof state:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T K : Subalgebra R A
⊢ K ≤ centralizer R ↑(S ⊔ T) ↔ K ≤ centralizer R ↑S ⊓ centralizer R ↑T

Tactic:
simp_rw [le_centralizer_iff, sup_le_iff, le_inf_iff, K.le_centralizer_iff]

Result:
no goals
-- Mathlib/Logic/Equiv/Set.lean
theorem prod_assoc_image {α β γ} {s : Set α} {t : Set β} {u : Set γ} :
    Equiv.prodAssoc α β γ '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
⊢ ⇑(prodAssoc α β γ) '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

Tactic:
simpa only [Equiv.image_eq_preimage] using prod_assoc_symm_preimage

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem pairwise_insert :
    (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b ∧ r b a

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
⊢ (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b ∧ r b a

Tactic:
simp only [insert_eq, pairwise_union, pairwise_singleton, true_and, mem_singleton_iff, forall_eq]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_add_eq_of_lt_left {x y : R} (h : v x < v y) :
    v (x + y) = v x

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
h : v x < v y
⊢ v (x + y) = v x

Tactic:
rw [map_add_of_distinct_val _ h.ne, min_eq_left h.le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
    (a :: l)[i] =
      if h : i = 0 then a else l[i-1]'(match i, h with | i+1, _ => succ_lt_succ_iff.mp w)

Proof state:
α : Type u_1
i : Nat
a : α
l : List α
w : i < (a :: l).length
⊢ (a :: l)[i] = if h : i = 0 then a else l[i - 1]

Tactic:
cases i <;> simp

Result:
no goals
-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_eq_append_iff (l : List (Option α)) (l'₁ l'₂ : List α) :
    l.reduceOption = l'₁ ++ l'₂ ↔
      ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.reduceOption = l'₁ ∧ l₂.reduceOption = l'₂

Proof state:
α : Type u_1
l : List (Option α)
l'₁ l'₂ : List α
⊢ filterMap id l = l'₁ ++ l'₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap id l₁ = l'₁ ∧ filterMap id l₂ = l'₂

Tactic:
exact filterMap_eq_append_iff

Result:
no goals

Proof state:
α : Type u_1
l : List (Option α)
l'₁ l'₂ : List α
⊢ l.reduceOption = l'₁ ++ l'₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.reduceOption = l'₁ ∧ l₂.reduceOption = l'₂

Tactic:
dsimp [reduceOption]

Result:
α : Type u_1
l : List (Option α)
l'₁ l'₂ : List α
⊢ filterMap id l = l'₁ ++ l'₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap id l₁ = l'₁ ∧ filterMap id l₂ = l'₂