harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Multiset/UnionInter.lean
theorem add_eq_union_iff_disjoint [DecidableEq α] {s t : Multiset α} :
    s + t = s ∪ t ↔ Disjoint s t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t = s ∪ t ↔ _root_.Disjoint s t

Tactic:
simp_rw [← inter_eq_zero_iff_disjoint, ext, count_add, count_union, count_inter, count_zero,
  Nat.min_eq_zero_iff, Nat.add_eq_max_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_div_pow_lt_one_div_pow_of_lt (a1 : 1 < a) {m n : ℕ} (mn : m < n) :
    1 / a ^ n < 1 / a ^ m

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 1 / a ^ n < 1 / a ^ m

Tactic:
refine (one_div_lt_one_div ?_ ?_).2 (pow_lt_pow_right₀ a1 mn) <;>
  exact pow_pos (zero_lt_one.trans a1) _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_eq_length_filter' : countP p = length ∘ filter p

Proof state:
case h
α : Type u_1
p : α → Bool
l : List α
⊢ countP p l = (length ∘ filter p) l

Tactic:
apply countP_eq_length_filter

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
⊢ countP p = length ∘ filter p

Tactic:
funext l

Result:
case h
α : Type u_1
p : α → Bool
l : List α
⊢ countP p l = (length ∘ filter p) l
-- Mathlib/Analysis/RCLike/Inner.lean
@[simp] lemma wInner_zero_left (w : ι → ℝ) (g : ∀ i, E i) : ⟪0, g⟫_[𝕜, w] = 0

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
g : (i : ι) → E i
⊢ wInner w 0 g = 0

Tactic:
simp [wInner]

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem _root_.LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad {L : Type v} [LieRing L]
    [LieAlgebra R L] (K : LieSubalgebra R L) {x : K} (h : IsNilpotent (LieAlgebra.ad R L ↑x)) :
    IsNilpotent (LieAlgebra.ad R K x)

Proof state:
R : Type u
inst✝² : CommRing R
L : Type v
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
h : IsNilpotent ((LieAlgebra.ad R L) ↑x)
⊢ IsNilpotent ((LieAlgebra.ad R ↥K) x)

Tactic:
obtain ⟨n, hn⟩ := h

Result:
case intro
R : Type u
inst✝² : CommRing R
L : Type v
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
n : ℕ
hn : (LieAlgebra.ad R L) ↑x ^ n = 0
⊢ IsNilpotent ((LieAlgebra.ad R ↥K) x)

Proof state:
case h
R : Type u
inst✝² : CommRing R
L : Type v
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
n : ℕ
hn : (LieAlgebra.ad R L) ↑x ^ n = 0
⊢ (LieAlgebra.ad R ↥K) x ^ n = 0

Tactic:
exact LinearMap.submodule_pow_eq_zero_of_pow_eq_zero (K.ad_comp_incl_eq x) hn

Result:
no goals

Proof state:
case intro
R : Type u
inst✝² : CommRing R
L : Type v
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
n : ℕ
hn : (LieAlgebra.ad R L) ↑x ^ n = 0
⊢ IsNilpotent ((LieAlgebra.ad R ↥K) x)

Tactic:
use n

Result:
case h
R : Type u
inst✝² : CommRing R
L : Type v
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
n : ℕ
hn : (LieAlgebra.ad R L) ↑x ^ n = 0
⊢ (LieAlgebra.ad R ↥K) x ^ n = 0
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem Matrix.toBilin'_single (M : Matrix n n R₁) (i j : n) :
    Matrix.toBilin' M (Pi.single i 1) (Pi.single j 1) = M i j

Proof state:
R₁ : Type u_1
inst✝² : CommSemiring R₁
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R₁
i j : n
⊢ ((toBilin' M) (Pi.single i 1)) (Pi.single j 1) = M i j

Tactic:
simp [Matrix.toBilin'_apply, Pi.single_apply]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem gcd_add (s₁ s₂ : Multiset α) : (s₁ + s₂).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd :=
  Eq.trans (by simp [gcd]) (fold_add _ _ _ _ _)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ s₂ : Multiset α
⊢ (s₁ + s₂).gcd = fold GCDMonoid.gcd (GCDMonoid.gcd 0 0) (s₁ + s₂)

Tactic:
simp [gcd]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem gcd_eq_zero {xs : IntList} : xs.gcd = 0 ↔ ∀ x, x ∈ xs → x = 0

Proof state:
xs : IntList
⊢ xs.gcd = 0 ↔ ∀ (x : Int), x ∈ xs → x = 0

Tactic:
simp [gcd_eq_iff, Nat.dvd_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma leftUnitor_naturality {X Y : LocalizedMonoidal L W ε} (f : X ⟶ Y) :
    𝟙_ (LocalizedMonoidal L W ε) ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
f : X ⟶ Y
⊢ 𝟙_ (LocalizedMonoidal L W ε) ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f

Tactic:
simp [monoidalCategoryStruct]

Result:
no goals
-- Mathlib/Logic/Equiv/Option.lean
theorem removeNone_optionCongr (e : α ≃ β) : removeNone e.optionCongr = e :=
  Equiv.ext fun x => Option.some_injective _ <| removeNone_some _ ⟨e x, by simp [EquivFunctor.map]⟩

Proof state:
α : Type u_1
β : Type u_2
e : α ≃ β
x : α
⊢ e.optionCongr (some x) = some (e x)

Tactic:
simp [EquivFunctor.map]

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
@[simp] lemma mem_biUnion {b : β} : b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : α → Finset β
inst✝ : DecidableEq β
b : β
⊢ b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a

Tactic:
simp only [mem_def, biUnion_val, Multiset.mem_dedup, Multiset.mem_bind, exists_prop]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem closure_inv (s : Set G) : closure s⁻¹ = closure s

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ = closure s

Tactic:
simp only [← toSubmonoid_inj, closure_toSubmonoid, inv_inv, union_comm]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem ite_not (P : Prop) [Decidable P] (x : α) :
    f (ite P x (f x)) = ite (¬P) x (f x)

Proof state:
α : Sort u
f : α → α
h : Involutive f
P : Prop
inst✝ : Decidable P
x : α
⊢ f (if P then x else f x) = if ¬P then x else f x

Tactic:
rw [apply_ite f, h, ite_not]

Result:
no goals
-- Mathlib/Order/Category/LinOrd.lean
lemma inv_hom_apply {X Y : LinOrd} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x

Proof state:
X Y : LinOrd
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

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

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
c : ι → R
⊢ ⇑(b.repr (∑ i : ι, c i • b i)) = c

Tactic:
simp_rw [← b.equivFun_symm_apply, ← b.equivFun_apply, b.equivFun.apply_symm_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
@[congr]
lemma expect_congr {t : Finset ι} (hst : s = t) (h : ∀ i ∈ t, f i = g i) :
    𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f g : ι → M
t : Finset ι
hst : s = t
h : ∀ i ∈ t, f i = g i
⊢ 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Tactic:
rw [expect, expect, sum_congr hst h, hst]

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem trans_toPartialEquiv :
    (e.trans e').toPartialEquiv = e.toPartialEquiv.trans e'.toPartialEquiv :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl)
    (by simp [PartialEquiv.trans_source, Equiv.toPartialEquiv])

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
⊢ (e.trans e').toPartialEquiv.source = (e.toPartialEquiv.trans e'.toPartialEquiv).source

Tactic:
simp [PartialEquiv.trans_source, Equiv.toPartialEquiv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_toVector (f : Nat → α → β) (l : Array α) :
    l.toVector.mapIdx f = (l.mapIdx f).toVector.cast (by simp)

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
l : Array α
⊢ Vector.mapIdx f l.toVector = Vector.cast ⋯ (mapIdx f l).toVector

Tactic:
ext <;> simp

Result:
no goals

Proof state:
α : Type ?u.8842
β : Type ?u.8849
f : Nat → α → β
l : Array α
⊢ (mapIdx f l).size = l.size

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem ofReal_neg (r : ℝ) : ((-r : ℝ) : ℂ) = -r :=
  Complex.ext_iff.2 <| by simp [ofReal]

Proof state:
r : ℝ
⊢ (↑(-r)).re = (-↑r).re ∧ (↑(-r)).im = (-↑r).im

Tactic:
simp [ofReal]

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
/-- **Gibbs' inequality**: the Kullback-Leibler divergence is nonnegative.
Note that since `klDiv` takes value in `ℝ≥0∞` (defined when it is finite as `ENNReal.ofReal (...)`),
it is nonnegative by definition. This lemma proves that the argument of `ENNReal.ofReal`
is also nonnegative. -/
lemma integral_llr_add_sub_measure_univ_nonneg (hμν : μ ≪ ν) (h_int : Integrable (llr μ ν) μ) :
    0 ≤ ∫ x, llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ 0 ≤ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν

Tactic:
exact integral_nonneg fun x ↦ klFun_nonneg ENNReal.toReal_nonneg

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal

Tactic:
rw [← integral_klFun_rnDeriv hμν h_int]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ 0 ≤ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem Ici_disjoint_Iic : Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b

Proof state:
α : Type v
inst✝ : Preorder α
a b : α
⊢ Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b

Tactic:
rw [Set.disjoint_iff_inter_eq_empty, Ici_inter_Iic, Icc_eq_empty_iff]

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem mem_res (f : α → β) (s : Set α) (a : α) (b : β) : b ∈ res f s a ↔ a ∈ s ∧ f a = b

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
b : β
⊢ b ∈ res f s a ↔ a ∈ s ∧ f a = b

Tactic:
simp [res, @eq_comm _ b]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
lemma isCoprime_row (A : SL(2, R)) (i : Fin 2) : IsCoprime (A i 0) (A i 1)

Proof state:
case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ -↑A 0 1 * ↑A 1 0 + ↑A 0 0 * ↑A 1 1 = 1

Tactic:
simp_rw [det_coe A ▸ det_fin_two A.1]

Result:
case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ -↑A 0 1 * ↑A 1 0 + ↑A 0 0 * ↑A 1 1 = ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0

Proof state:
case refine_2
R : Type v
inst✝ : CommRing R
A : SL(2, R)
i : Fin 2
⊢ -↑A 0 1 * ↑A 1 0 + ↑A 0 0 * ↑A 1 1 = ↑A 0 0 * ↑A 1 1 - ↑A 0 1 * ↑A 1 0

Tactic:
ring

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem boundedLimitRec_succ {l} (lLim : l.IsLimit) {C} (o H₁ H₂ H₃) :
    @boundedLimitRecOn l lLim C ⟨succ o.1, lLim.succ_lt o.2⟩ H₁ H₂ H₃ = H₂ o
    (@boundedLimitRecOn l lLim C o H₁ H₂ H₃)

Proof state:
l : Ordinal.{u_4}
lLim : l.IsLimit
C : ↑(Iio l) → Sort u_5
o : ↑(Iio l)
H₁ : C ⟨0, ⋯⟩
H₂ : (o : ↑(Iio l)) → C o → C ⟨succ ↑o, ⋯⟩
H₃ : (o : ↑(Iio l)) → (↑o).IsLimit → ((o' : ↑(Iio l)) → o' < o → C o') → C o
⊢ H₂ ⟨↑o, ⋯⟩
      ((↑o).limitRecOn (fun x => H₁) (fun o ih h => H₂ ⟨o, ⋯⟩ (ih ⋯))
        (fun _o ho ih x => H₃ ⟨_o, x⟩ ho fun _o' h => ih (↑_o') h ⋯) ⋯) =
    H₂ o (boundedLimitRecOn lLim o H₁ H₂ H₃)

Tactic:
rfl

Result:
no goals

Proof state:
l : Ordinal.{u_4}
lLim : l.IsLimit
C : ↑(Iio l) → Sort u_5
o : ↑(Iio l)
H₁ : C ⟨0, ⋯⟩
H₂ : (o : ↑(Iio l)) → C o → C ⟨succ ↑o, ⋯⟩
H₃ : (o : ↑(Iio l)) → (↑o).IsLimit → ((o' : ↑(Iio l)) → o' < o → C o') → C o
⊢ boundedLimitRecOn lLim ⟨succ ↑o, ⋯⟩ H₁ H₂ H₃ = H₂ o (boundedLimitRecOn lLim o H₁ H₂ H₃)

Tactic:
rw [boundedLimitRecOn, limitRecOn_succ]

Result:
l : Ordinal.{u_4}
lLim : l.IsLimit
C : ↑(Iio l) → Sort u_5
o : ↑(Iio l)
H₁ : C ⟨0, ⋯⟩
H₂ : (o : ↑(Iio l)) → C o → C ⟨succ ↑o, ⋯⟩
H₃ : (o : ↑(Iio l)) → (↑o).IsLimit → ((o' : ↑(Iio l)) → o' < o → C o') → C o
⊢ H₂ ⟨↑o, ⋯⟩
      ((↑o).limitRecOn (fun x => H₁) (fun o ih h => H₂ ⟨o, ⋯⟩ (ih ⋯))
        (fun _o ho ih x => H₃ ⟨_o, x⟩ ho fun _o' h => ih (↑_o') h ⋯) ⋯) =
    H₂ o (boundedLimitRecOn lLim o H₁ H₂ H₃)
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[simp] lemma ofEpiOfIsIsoOfMono'_g'_τ₃ : (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = h.g'

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.RightHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = h.g'

Tactic:
rw [← cancel_epi (ofEpiOfIsIsoOfMono' φ h).p, p_g'_assoc, ofEpiOfIsIsoOfMono'_p,
  assoc, p_g', φ.comm₂₃]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem product_eq_biUnion_right [DecidableEq (α × β)] (s : Finset α) (t : Finset β) :
    s ×ˢ t = t.biUnion fun b => s.image fun a => (a, b) :=
  ext fun ⟨x, y⟩ => by
    simp only [mem_product, mem_biUnion, mem_image, exists_prop, Prod.mk.inj_iff, and_left_comm,
      exists_and_left, exists_eq_right, exists_eq_left]

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
x✝ : α × β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ t ↔ (x, y) ∈ t.biUnion fun b => image (fun a => (a, b)) s

Tactic:
simp only [mem_product, mem_biUnion, mem_image, exists_prop, Prod.mk.inj_iff, and_left_comm,
  exists_and_left, exists_eq_right, exists_eq_left]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
theorem neg_e0_mul_v (m : M) : -(e0 Q * v Q m) = v Q m * e0 Q

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ -(e0 Q * (v Q) m) = (v Q) m * e0 Q

Tactic:
refine neg_eq_of_add_eq_zero_right ((ι_mul_ι_add_swap _ _).trans ?_)

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (algebraMap R (CliffordAlgebra (Q' Q))) (QuadraticMap.polar ⇑(Q' Q) (0, 1) ((LinearMap.inl R M R) m)) = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (algebraMap R (CliffordAlgebra (Q' Q))) (Q (0 + m) + -((1 + 0) * (1 + 0)) - (Q 0 + -(1 * 1)) - (Q m + -(0 * 0))) = 0

Tactic:
simp only [add_zero, mul_zero, mul_one, zero_add, neg_zero, QuadraticMap.map_zero,
  add_sub_cancel_right, sub_self, map_zero, zero_sub]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (algebraMap R (CliffordAlgebra (Q' Q))) (QuadraticMap.polar ⇑(Q' Q) (0, 1) ((LinearMap.inl R M R) m)) = 0

Tactic:
dsimp [QuadraticMap.polar]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (algebraMap R (CliffordAlgebra (Q' Q))) (Q (0 + m) + -((1 + 0) * (1 + 0)) - (Q 0 + -(1 * 1)) - (Q m + -(0 * 0))) = 0
-- Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean
theorem Sphere.secondInter_collinear (s : Sphere P) (p p' : P) :
    Collinear ℝ ({p, p', s.secondInter p (p' -ᵥ p)} : Set P)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p p' : P
⊢ Collinear ℝ {p, p', s.secondInter p (p' -ᵥ p)}

Tactic:
rw [Set.pair_comm, Set.insert_comm]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p p' : P
⊢ Collinear ℝ {s.secondInter p (p' -ᵥ p), p, p'}

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p p' : P
⊢ Collinear ℝ {s.secondInter p (p' -ᵥ p), p, p'}

Tactic:
exact
  (collinear_insert_iff_of_mem_affineSpan (s.secondInter_vsub_mem_affineSpan _ _)).2
    (collinear_pair ℝ _ _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem dvd_add {a b c : Nat} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c :=
  let ⟨d, hd⟩ := h₁; let ⟨e, he⟩ := h₂; ⟨d + e, by simp [Nat.left_distrib, hd, he]⟩

Proof state:
a b c : Nat
h₁ : a ∣ b
h₂ : a ∣ c
d : Nat
hd : b = a * d
e : Nat
he : c = a * e
⊢ b + c = a * (d + e)

Tactic:
simp [Nat.left_distrib, hd, he]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean
theorem C_two_mul_complex_cos (n : ℤ) : (C ℂ n).eval (2 * cos θ) = 2 * cos (n * θ)

Proof state:
θ : ℂ
n : ℤ
⊢ eval (2 * cos θ) (C ℂ n) = 2 * cos (↑n * θ)

Tactic:
simp [C_eq_two_mul_T_comp_half_mul_X]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem hasFDerivWithinAt_comp_add_left (a : E) :
    HasFDerivWithinAt (fun x ↦ f (a + x)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (a + x)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
a : E
⊢ map (fun x => a + x) (𝓝[s] x) = 𝓝[a +ᵥ s] (a + x)

Tactic:
simp only [add_comm x a, nhdsWithin, Filter.map_inf (add_right_injective a)]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
a : E
⊢ map (fun x => a + x) (𝓝 x) ⊓ map (fun x => a + x) (𝓟 s) = 𝓝 (a + x) ⊓ 𝓟 (a +ᵥ s)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
a : E
this : map (fun x => a + x) (𝓝[s] x) = 𝓝[a +ᵥ s] (a + x)
⊢ HasFDerivWithinAt (fun x => f (a + x)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (a + x)

Tactic:
simp [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleOTVS, ← this, Function.comp_def]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
a : E
⊢ map (fun x => a + x) (𝓝 x) ⊓ map (fun x => a + x) (𝓟 s) = 𝓝 (a + x) ⊓ 𝓟 (a +ᵥ s)

Tactic:
simp [← Set.image_vadd]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem add_smul_subset (a b : α) (s : Set β) : (a + b) • s ⊆ a • s + b • s

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
a b : α
s : Set β
⊢ (a + b) • s ⊆ a • s + b • s

Tactic:
rintro _ ⟨x, hx, rfl⟩

Result:
case intro.intro
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
a b : α
s : Set β
x : β
hx : x ∈ s
⊢ (fun x => (a + b) • x) x ∈ a • s + b • s

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
a b : α
s : Set β
x : β
hx : x ∈ s
⊢ (fun x => (a + b) • x) x ∈ a • s + b • s

Tactic:
simpa only [add_smul] using add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hx)

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean
lemma extend_exactAt_iff :
    (K.extend e).ExactAt j' ↔ K.ExactAt j

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.extend e).ExactAt j' ↔ K.ExactAt j

Tactic:
simp only [HomologicalComplex.exactAt_iff_isZero_homology]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ IsZero ((K.extend e).homology j') ↔ IsZero (K.homology j)

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ IsZero ((K.extend e).homology j') ↔ IsZero (K.homology j)

Tactic:
exact (K.extendHomologyIso e hj').isZero_iff

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem sigma_one_apply_prime_pow {p i : ℕ} (hp : p.Prime) :
    σ 1 (p ^ i) = ∑ k ∈ .range (i + 1), p ^ k

Proof state:
p i : ℕ
hp : Nat.Prime p
⊢ (σ 1) (p ^ i) = ∑ k ∈ range (i + 1), p ^ k

Tactic:
simp [sigma_apply_prime_pow hp]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem succ_nadd : succ a ♯ b = succ (a ♯ b)

Proof state:
a b : Ordinal.{u}
⊢ succ a ♯ b = succ (a ♯ b)

Tactic:
rw [← one_nadd (a ♯ b), ← nadd_assoc, one_nadd]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval_natCast_mul {n : ℕ} : ((n : R[X]) * p).eval x = n * p.eval x

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
x : R
n : ℕ
⊢ eval x (↑n * p) = ↑n * eval x p

Tactic:
rw [← C_eq_natCast, eval_C_mul]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Hom.lean
theorem _root_.IsScalarTower.smulHomClass [MulOneClass X] [SMul X Y] [IsScalarTower M' X Y]
    [MulActionHomClass F X X Y] : MulActionHomClass F M' X Y where
  map_smulₛₗ f m x

Proof state:
M' : Type u_1
X : Type u_5
inst✝⁶ : SMul M' X
Y : Type u_6
inst✝⁵ : SMul M' Y
F : Type u_8
inst✝⁴ : FunLike F X Y
inst✝³ : MulOneClass X
inst✝² : SMul X Y
inst✝¹ : IsScalarTower M' X Y
inst✝ : MulActionHomClass F X X Y
f : F
m : M'
x : X
⊢ f (m • x) = id m • f x

Tactic:
rw [← mul_one (m • x), ← smul_eq_mul, map_smul, smul_assoc, ← map_smul,
  smul_eq_mul, mul_one, id_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
@[simp]
lemma finsuppRight_symm_apply_single (i : ι) (m : M) (n : N) :
    (finsuppRight R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) =
      m ⊗ₜ[R] Finsupp.single i n

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
i : ι
m : M
n : N
⊢ (finsuppRight R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) = m ⊗ₜ[R] Finsupp.single i n

Tactic:
simp [finsuppRight, Finsupp.lsum]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem or_eq_orElse : or o o' = o.orElse (fun _ => o')

Proof state:
α✝ : Type u_1
o o' : Option α✝
⊢ o.or o' = o.orElse fun x => o'

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem eq_prod_roots_of_splits_id {p : K[X]} (hsplit : Splits (RingHom.id K) p) :
    p = C p.leadingCoeff * (p.roots.map fun a => X - C a).prod

Proof state:
K : Type v
inst✝ : Field K
p : K[X]
hsplit : Splits (RingHom.id K) p
⊢ p = C p.leadingCoeff * (Multiset.map (fun a => X - C a) p.roots).prod

Tactic:
simpa using eq_prod_roots_of_splits hsplit

Result:
no goals