harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem gluedCoverT'_fst_fst (x y z : 𝒰.J) :
    𝒰.gluedCoverT' x y z ≫ pullback.fst _ _ ≫ pullback.fst _ _ =
      pullback.fst _ _ ≫ pullback.snd _ _

Proof state:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ ((pullbackRightPullbackFstIso (𝒰.map x) (𝒰.map z) (pullback.fst (𝒰.map x) (𝒰.map y))).hom ≫
        (pullback.map (pullback.fst (𝒰.map x) (𝒰.map y) ≫ 𝒰.map x) (𝒰.map z)
              (pullback.fst (𝒰.map y) (𝒰.map x) ≫ 𝒰.map y) (𝒰.map z) (pullbackSymmetry (𝒰.map x) (𝒰.map y)).hom
              (𝟙 (𝒰.obj z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.map y) (𝒰.map z) (pullback.fst (𝒰.map y) (𝒰.map x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.map y) (𝒰.map x)) (pullback.fst (𝒰.map y) (𝒰.map z))).hom) ≫
      pullback.fst (pullback.fst (𝒰.map y) (𝒰.map z)) (pullback.fst (𝒰.map y) (𝒰.map x)) ≫
        pullback.fst (𝒰.map y) (𝒰.map z) =
    pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) ≫
      pullback.snd (𝒰.map x) (𝒰.map y)

Tactic:
simp

Result:
no goals

Proof state:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ gluedCoverT' 𝒰 x y z ≫
      pullback.fst (pullback.fst (𝒰.map y) (𝒰.map z)) (pullback.fst (𝒰.map y) (𝒰.map x)) ≫
        pullback.fst (𝒰.map y) (𝒰.map z) =
    pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) ≫
      pullback.snd (𝒰.map x) (𝒰.map y)

Tactic:
delta gluedCoverT'

Result:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ ((pullbackRightPullbackFstIso (𝒰.map x) (𝒰.map z) (pullback.fst (𝒰.map x) (𝒰.map y))).hom ≫
        (pullback.map (pullback.fst (𝒰.map x) (𝒰.map y) ≫ 𝒰.map x) (𝒰.map z)
              (pullback.fst (𝒰.map y) (𝒰.map x) ≫ 𝒰.map y) (𝒰.map z) (pullbackSymmetry (𝒰.map x) (𝒰.map y)).hom
              (𝟙 (𝒰.obj z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.map y) (𝒰.map z) (pullback.fst (𝒰.map y) (𝒰.map x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.map y) (𝒰.map x)) (pullback.fst (𝒰.map y) (𝒰.map z))).hom) ≫
      pullback.fst (pullback.fst (𝒰.map y) (𝒰.map z)) (pullback.fst (𝒰.map y) (𝒰.map x)) ≫
        pullback.fst (𝒰.map y) (𝒰.map z) =
    pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) ≫
      pullback.snd (𝒰.map x) (𝒰.map y)
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
/-- The triangle inequality for an `AbsoluteValue` applied to a list. -/
lemma listSum_le (l : List R) : abv l.sum ≤ (l.map abv).sum

Proof state:
case nil
R : Type u_5
S : Type u_6
inst✝¹ : Semiring R
inst✝ : OrderedSemiring S
abv : AbsoluteValue R S
⊢ abv [].sum ≤ (List.map ⇑abv []).sum

Tactic:
simp

Result:
no goals

Proof state:
case cons
R : Type u_5
S : Type u_6
inst✝¹ : Semiring R
inst✝ : OrderedSemiring S
abv : AbsoluteValue R S
head : R
tail : List R
ih : abv tail.sum ≤ (List.map (⇑abv) tail).sum
⊢ abv (head :: tail).sum ≤ (List.map (⇑abv) (head :: tail)).sum

Tactic:
exact (abv.add_le ..).trans <| add_le_add_left ih (abv head)

Result:
no goals

Proof state:
R : Type u_5
S : Type u_6
inst✝¹ : Semiring R
inst✝ : OrderedSemiring S
abv : AbsoluteValue R S
l : List R
⊢ abv l.sum ≤ (List.map (⇑abv) l).sum

Tactic:
induction l with
| nil => simp
| cons head tail ih => exact (abv.add_le ..).trans <| add_le_add_left ih (abv head)

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem eq_re_of_eq_coe {a : ℍ[R,c₁,c₂,c₃]} {x : R} (h : a = x) : a = a.re

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
inst✝ : CommRing R
a : ℍ[R,c₁,c₂,c₃]
x : R
h : a = ↑x
⊢ a = ↑a.re

Tactic:
rw [h, coe_re]

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem summable_rpow_inv {p : ℝ} :
    Summable (fun n => ((n : ℝ≥0) ^ p)⁻¹ : ℕ → ℝ≥0) ↔ 1 < p

Proof state:
p : ℝ
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
simp [← NNReal.summable_coe]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
lemma LinearMap.toMatrix_prodMap [DecidableEq m] [DecidableEq (n ⊕ m)]
    (φ₁ : Module.End R M₁) (φ₂ : Module.End R M₂) :
    toMatrix (v₁.prod v₂) (v₁.prod v₂) (φ₁.prodMap φ₂) =
      Matrix.fromBlocks (toMatrix v₁ v₁ φ₁) 0 0 (toMatrix v₂ v₂ φ₂)

Proof state:
R : Type u_1
inst✝⁹ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝¹ : DecidableEq m
inst✝ : DecidableEq (n ⊕ m)
φ₁ : Module.End R M₁
φ₂ : Module.End R M₂
⊢ (toMatrix (v₁.prod v₂) (v₁.prod v₂)) (prodMap φ₁ φ₂) = fromBlocks ((toMatrix v₁ v₁) φ₁) 0 0 ((toMatrix v₂ v₂) φ₂)

Tactic:
ext (i|i) (j|j) <;> simp [toMatrix]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive card_nsmul_le_sum]
lemma pow_card_le_prod (h : ∀ x ∈ s, a ≤ x) : a ^ card s ≤ s.prod

Proof state:
α : Type u_2
inst✝ : OrderedCommMonoid α
s : Multiset α
a : α
h : ∀ x ∈ s, a ≤ x
⊢ a ^ s.card ≤ s.prod

Tactic:
rw [← Multiset.prod_replicate, ← Multiset.map_const]

Result:
α : Type u_2
inst✝ : OrderedCommMonoid α
s : Multiset α
a : α
h : ∀ x ∈ s, a ≤ x
⊢ (map (Function.const α a) s).prod ≤ s.prod

Proof state:
α : Type u_2
inst✝ : OrderedCommMonoid α
s : Multiset α
a : α
h : ∀ x ∈ s, a ≤ x
⊢ (map (Function.const α a) s).prod ≤ s.prod

Tactic:
exact prod_map_le_prod _ h

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
@[reassoc]
lemma shiftIso_hom_app_comp (n m mn : M) (hnm : m + n = mn)
    (a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
    (shiftIso F n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫
      (shiftIso F m a' a'' ha'').hom.app X =
        (shift F a).map ((shiftFunctorAdd' C m n mn hnm).inv.app X) ≫
          (F.shiftIso mn a a'' (by rw [← hnm, ← ha'', ← ha', add_assoc])).hom.app X

Proof state:
C : Type u_1
A : Type u_2
inst✝⁶ : Category.{?u.65615, u_1} C
inst✝⁵ : Category.{?u.65619, u_2} A
F : C ⥤ A
M : Type u_3
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
G : Type u_4
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ mn + a = a''

Tactic:
rw [← hnm, ← ha'', ← ha', add_assoc]

Result:
no goals

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_6, u_1} C
inst✝³ : Category.{u_5, u_2} A
F : C ⥤ A
M : Type u_3
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X =
    (F.shift a).map ((shiftFunctorAdd' C m n mn hnm).inv.app X) ≫ (F.shiftIso mn a a'' ⋯).hom.app X

Tactic:
rw [F.shiftIso_add'_hom_app n m mn hnm a a' a'' ha' ha'', ← Functor.map_comp_assoc,
  Iso.inv_hom_id_app, Functor.map_id, id_comp]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_nonpos_le {s : Set X} (hs : MeasurableSet s) (hf : StronglyMeasurable f)
    (hfi : Integrable f μ) : ∫ x in {y | f y ≤ 0}, f x ∂μ ≤ ∫ x in s, f x ∂μ

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ ∫ (x : X) in {y | f y ≤ 0}, f x ∂μ ≤ ∫ (x : X) in s, f x ∂μ

Tactic:
rw [← integral_indicator hs, ←
  integral_indicator (hf.measurableSet_le stronglyMeasurable_const)]

Result:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ ∫ (x : X), {a | f a ≤ 0}.indicator f x ∂μ ≤ ∫ (x : X), s.indicator f x ∂μ

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ ∫ (x : X), {a | f a ≤ 0}.indicator f x ∂μ ≤ ∫ (x : X), s.indicator f x ∂μ

Tactic:
exact
  integral_mono (hfi.indicator (hf.measurableSet_le stronglyMeasurable_const))
    (hfi.indicator hs) (indicator_nonpos_le_indicator s f)

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/ConjAct.lean
theorem mem_orbit_conjAct {g h : G} : g ∈ orbit (ConjAct G) h ↔ IsConj g h

Proof state:
G : Type u_3
inst✝ : Group G
g h : G
⊢ g ∈ orbit (ConjAct G) h ↔ IsConj g h

Tactic:
rw [isConj_comm, isConj_iff, mem_orbit_iff]

Result:
G : Type u_3
inst✝ : Group G
g h : G
⊢ (∃ x, x • h = g) ↔ ∃ c, c * h * c⁻¹ = g

Proof state:
G : Type u_3
inst✝ : Group G
g h : G
⊢ (∃ x, x • h = g) ↔ ∃ c, c * h * c⁻¹ = g

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem DenseRange.subset_closure_image_preimage_of_isOpen (hf : DenseRange f) (hs : IsOpen s) :
    s ⊆ closure (f '' (f ⁻¹' s))

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_4
f : α → X
s : Set X
hf : DenseRange f
hs : IsOpen s
⊢ s ⊆ closure (f '' (f ⁻¹' s))

Tactic:
rw [image_preimage_eq_inter_range]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_4
f : α → X
s : Set X
hf : DenseRange f
hs : IsOpen s
⊢ s ⊆ closure (s ∩ range f)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_4
f : α → X
s : Set X
hf : DenseRange f
hs : IsOpen s
⊢ s ⊆ closure (s ∩ range f)

Tactic:
exact hf.open_subset_closure_inter hs

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem sup_left_right_swap (a b c : α) : a ⊔ b ⊔ c = c ⊔ b ⊔ a

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = c ⊔ b ⊔ a

Tactic:
rw [sup_comm, sup_comm a, sup_assoc]

Result:
no goals
-- Mathlib/RingTheory/WittVector/WittPolynomial.lean
theorem xInTermsOfW_zero [Invertible (p : R)] : xInTermsOfW p R 0 = X 0

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
⊢ xInTermsOfW p R 0 = X 0

Tactic:
rw [xInTermsOfW_eq, range_zero, sum_empty, pow_zero, C_1, mul_one, sub_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem monic_X_sub_C (x : R) : Monic (X - C x)

Proof state:
R : Type u
inst✝ : Ring R
x : R
⊢ (X - C x).Monic

Tactic:
simpa only [sub_eq_add_neg, C_neg] using monic_X_add_C (-x)

Result:
no goals
-- Mathlib/Algebra/Ring/Idempotent.lean
@[simp] lemma compl_compl (a : {a : R // IsIdempotentElem a}) : aᶜᶜ = a

Proof state:
R : Type u_1
inst✝ : NonAssocRing R
a : { a // IsIdempotentElem a }
⊢ aᶜᶜ = a

Tactic:
ext

Result:
case a
R : Type u_1
inst✝ : NonAssocRing R
a : { a // IsIdempotentElem a }
⊢ ↑aᶜᶜ = ↑a

Proof state:
case a
R : Type u_1
inst✝ : NonAssocRing R
a : { a // IsIdempotentElem a }
⊢ ↑aᶜᶜ = ↑a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat)

Proof state:
n : Nat
x y : BitVec n
⊢ x - y = BitVec.ofNat n (2 ^ n - y.toNat + x.toNat)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma yonedaEquiv_symm_naturality_right (X : C) {F F' : Cᵒᵖ ⥤ Type v₁} (f : F ⟶ F')
    (x : F.obj ⟨X⟩) : yonedaEquiv.symm x ≫ f = yonedaEquiv.symm (f.app ⟨X⟩ x)

Proof state:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F F' : Cᵒᵖ ⥤ Type v₁
f : F ⟶ F'
x : F.obj (op X)
⊢ yonedaEquiv (yonedaEquiv.symm x ≫ f) = yonedaEquiv (yonedaEquiv.symm (f.app (op X) x))

Tactic:
simp [yonedaEquiv_comp]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F F' : Cᵒᵖ ⥤ Type v₁
f : F ⟶ F'
x : F.obj (op X)
⊢ yonedaEquiv.symm x ≫ f = yonedaEquiv.symm (f.app (op X) x)

Tactic:
apply yonedaEquiv.injective

Result:
case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F F' : Cᵒᵖ ⥤ Type v₁
f : F ⟶ F'
x : F.obj (op X)
⊢ yonedaEquiv (yonedaEquiv.symm x ≫ f) = yonedaEquiv (yonedaEquiv.symm (f.app (op X) x))
-- Mathlib/Data/List/Rotate.lean
theorem length_rotate' : ∀ (l : List α) (n : ℕ), (l.rotate' n).length = l.length
  | [], _ => by simp
  | _ :: _, 0 => rfl
  | a :: l, n + 1 => by rw [List.rotate', length_rotate' (l ++ [a]) n]; simp

Proof state:
α : Type u
a : α
l : List α
n : ℕ
⊢ (l ++ [a]).length = (a :: l).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
n : ℕ
⊢ ((a :: l).rotate' (n + 1)).length = (a :: l).length

Tactic:
rw [List.rotate', length_rotate' (l ++ [a]) n]

Result:
α : Type u
a : α
l : List α
n : ℕ
⊢ (l ++ [a]).length = (a :: l).length

Proof state:
α : Type u
x✝ : ℕ
⊢ ([].rotate' x✝).length = [].length

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/IsSepClosed.lean
theorem IntermediateField.eq_bot_of_isSepClosed_of_isSeparable [IsSepClosed k] [Algebra k K]
    (L : IntermediateField k K) [Algebra.IsSeparable k L] : L = ⊥ := bot_unique fun x hx ↦ by
  obtain ⟨y, hy⟩ := IsSepClosed.algebraMap_surjective k L ⟨x, hx⟩
  exact ⟨y, congr_arg (algebraMap L K) hy⟩

Proof state:
case intro
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Algebra.IsSeparable k ↥L
x : K
hx : x ∈ L
y : k
hy : (algebraMap k ↥L) y = ⟨x, hx⟩
⊢ x ∈ ⊥

Tactic:
exact ⟨y, congr_arg (algebraMap L K) hy⟩

Result:
no goals

Proof state:
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Algebra.IsSeparable k ↥L
x : K
hx : x ∈ L
⊢ x ∈ ⊥

Tactic:
obtain ⟨y, hy⟩ := IsSepClosed.algebraMap_surjective k L ⟨x, hx⟩

Result:
case intro
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Algebra.IsSeparable k ↥L
x : K
hx : x ∈ L
y : k
hy : (algebraMap k ↥L) y = ⟨x, hx⟩
⊢ x ∈ ⊥
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
@[simp]
lemma toMvPolynomial_zero : (0 : Matrix m n R).toMvPolynomial = 0

Proof state:
case h.a
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
x✝ : m
m✝ : n →₀ ℕ
⊢ coeff m✝ (toMvPolynomial 0 x✝) = coeff m✝ (0 x✝)

Tactic:
simp only [toMvPolynomial, zero_apply, map_zero, Finset.sum_const_zero, Pi.zero_apply]

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
⊢ toMvPolynomial 0 = 0

Tactic:
ext

Result:
case h.a
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
x✝ : m
m✝ : n →₀ ℕ
⊢ coeff m✝ (toMvPolynomial 0 x✝) = coeff m✝ (0 x✝)
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem all (f) : ∀ {s}, Valid s → s.all f = s.toString.1.all f
  | _, h => let ⟨_, _, _, h⟩ := h.validFor; by simp [h.all, h.toString]

Proof state:
f : Char → Bool
x✝ : Substring
h✝ : x✝.Valid
w✝² w✝¹ w✝ : List Char
h : ValidFor w✝² w✝¹ w✝ x✝
⊢ x✝.all f = x✝.toString.data.all f

Tactic:
simp [h.all, h.toString]

Result:
no goals
-- Mathlib/Order/Hom/Basic.lean
theorem trans_refl (e : α ≃o β) : e.trans (refl β) = e

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
⊢ e.trans (refl β) = e

Tactic:
ext x

Result:
case h.h
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
x : α
⊢ (e.trans (refl β)) x = e x

Proof state:
case h.h
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
x : α
⊢ (e.trans (refl β)) x = e x

Tactic:
rfl

Result:
no goals
-- Mathlib/Control/Applicative.lean
theorem Applicative.map_seq_map (f : α → β → γ) (g : σ → β) (x : F α) (y : F σ) :
    f <$> x <*> g <$> y = ((· ∘ g) ∘ f) <$> x <*> y

Proof state:
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β γ σ : Type u
f : α → β → γ
g : σ → β
x : F α
y : F σ
⊢ f <$> x <*> g <$> y = ((fun x => x ∘ g) ∘ f) <$> x <*> y

Tactic:
simp [flip, functor_norm, Function.comp_def]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Associated.lean
theorem finset_prod_mk {p : Finset β} {f : β → α} :
    (∏ i ∈ p, Associates.mk (f i)) = Associates.mk (∏ i ∈ p, f i)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
p : Finset β
f : β → α
⊢ ∏ i ∈ p, Associates.mk (f i) = Associates.mk (∏ i ∈ p, f i)

Tactic:
have : (fun i => Associates.mk (f i)) = Associates.mk ∘ f :=
  funext fun x => Function.comp_apply

Result:
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
p : Finset β
f : β → α
this : (fun i => Associates.mk (f i)) = Associates.mk ∘ f
⊢ ∏ i ∈ p, Associates.mk (f i) = Associates.mk (∏ i ∈ p, f i)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CommMonoid α
p : Finset β
f : β → α
this : (fun i => Associates.mk (f i)) = Associates.mk ∘ f
⊢ ∏ i ∈ p, Associates.mk (f i) = Associates.mk (∏ i ∈ p, f i)

Tactic:
rw [Finset.prod_eq_multiset_prod, this, ← Multiset.map_map, prod_mk,
  ← Finset.prod_eq_multiset_prod]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem not_isSuccPrelimit [NoMinOrder α] : ¬ IsSuccPrelimit a

Proof state:
α : Type u_1
a : α
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMinOrder α
⊢ ¬IsSuccPrelimit a

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem coeff_nsmul {x : HahnSeries Γ R} {n : ℕ} : (n • x).coeff = n • x.coeff

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ R
n : ℕ
⊢ (n • x).coeff = n • x.coeff

Tactic:
induction n with
| zero => simp
| succ n ih => simp [add_nsmul, ih]

Result:
no goals

Proof state:
case succ
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ R
n : ℕ
ih : (n • x).coeff = n • x.coeff
⊢ ((n + 1) • x).coeff = (n + 1) • x.coeff

Tactic:
simp [add_nsmul, ih]

Result:
no goals

Proof state:
case zero
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : HahnSeries Γ R
⊢ (0 • x).coeff = 0 • x.coeff

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Closeds.lean
theorem lipschitz_infDist : LipschitzWith 2 fun p : α × NonemptyCompacts α => infDist p.1 p.2

Proof state:
case h.e'_5
α : Type u
inst✝ : MetricSpace α
⊢ 2 = 1 + 1

Tactic:
norm_num

Result:
no goals

Proof state:
α : Type u
inst✝ : MetricSpace α
⊢ LipschitzWith 2 fun p => infDist p.1 ↑p.2

Tactic:
convert @LipschitzWith.uncurry α (NonemptyCompacts α) ℝ _ _ _
  (fun (x : α) (s : NonemptyCompacts α) => infDist x s) 1 1
  (fun s => lipschitz_infDist_pt ↑s) lipschitz_infDist_set

Result:
case h.e'_5
α : Type u
inst✝ : MetricSpace α
⊢ 2 = 1 + 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem negSucc_inj : negSucc m = negSucc n ↔ m = n := ⟨negSucc.inj, fun H => by simp [H]⟩

Proof state:
m n : Nat
H : m = n
⊢ -[m+1] = -[n+1]

Tactic:
simp [H]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem modify_eq_alter (t : RBNode α) : t.modify cut f = t.alter cut (.map f)

Proof state:
α : Type u_1
cut : α → Ordering
f : α → α
t : RBNode α
⊢ modify cut f t = alter cut (Option.map f) t

Tactic:
simp [modify, alter]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem mem_polar_singleton {a : E} (y : Dual 𝕜 E) : y ∈ polar 𝕜 {a} ↔ ‖y a‖ ≤ 1

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a : E
y : Dual 𝕜 E
⊢ y ∈ polar 𝕜 {a} ↔ ‖y a‖ ≤ 1

Tactic:
simp only [polar_singleton, mem_setOf_eq]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem inner_rightAngleRotationAux₁_right (x y : E) :
    ⟪x, o.rightAngleRotationAux₁ 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 (o.rightAngleRotationAux₁ y) x = -(o.areaForm x) y

Tactic:
simp [o.areaForm_swap y x]

Result:
no goals

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.rightAngleRotationAux₁ y) = -(o.areaForm x) y

Tactic:
rw [real_inner_comm]

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 (o.rightAngleRotationAux₁ y) x = -(o.areaForm x) y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : e.toNormPoly == e'.toPoly) : e.denote ctx = e'.denote ctx

Proof state:
ctx : Context
e e' : Expr
h✝ : (e.toNormPoly == e'.toPoly) = true
h : Poly.denote ctx e.toNormPoly = Poly.denote ctx e'.toPoly
⊢ denote ctx e = denote ctx e'

Tactic:
simp [Expr.toNormPoly, Poly.norm] at h

Result:
ctx : Context
e e' : Expr
h✝ : (e.toNormPoly == e'.toPoly) = true
h : denote ctx e = denote ctx e'
⊢ denote ctx e = denote ctx e'

Proof state:
ctx : Context
e e' : Expr
h : (e.toNormPoly == e'.toPoly) = true
⊢ denote ctx e = denote ctx e'

Tactic:
have h := congrArg (Poly.denote ctx) (eq_of_beq h)

Result:
ctx : Context
e e' : Expr
h✝ : (e.toNormPoly == e'.toPoly) = true
h : Poly.denote ctx e.toNormPoly = Poly.denote ctx e'.toPoly
⊢ denote ctx e = denote ctx e'

Proof state:
ctx : Context
e e' : Expr
h✝ : (e.toNormPoly == e'.toPoly) = true
h : denote ctx e = denote ctx e'
⊢ denote ctx e = denote ctx e'

Tactic:
assumption

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem support_mk'_subset {f : ∀ i, β i} {s : Multiset ι} {h} :
    (mk' f <| Trunc.mk ⟨s, h⟩).support ⊆ s.toFinset := fun i H =>
  Multiset.mem_toFinset.1 <| by simpa using (Finset.mem_filter.1 H).1

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : (i : ι) → β i
s : Multiset ι
h : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
H : i ∈ { toFun := f, support' := Trunc.mk ⟨s, h⟩ }.support
⊢ i ∈ s.toFinset.val.toFinset

Tactic:
simpa using (Finset.mem_filter.1 H).1

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Basic.lean
theorem lift_eq (f : M →ₗ[R] N) (g : Hausdorffification I M →ₗ[R] N) (hg : g.comp (of I M) = f) :
    g = lift I f :=
  LinearMap.ext fun x => induction_on x fun x => by rw [lift_of, ← hg, LinearMap.comp_apply]

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : IsHausdorff I N
f : M →ₗ[R] N
g : Hausdorffification I M →ₗ[R] N
hg : g ∘ₗ of I M = f
x✝ : Hausdorffification I M
x : M
⊢ g ((of I M) x) = (lift I f) ((of I M) x)

Tactic:
rw [lift_of, ← hg, LinearMap.comp_apply]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem _root_.Finset.coe_infsep_of_offDiag_empty
    [DecidableEq α] {s : Finset α} (hs : s.offDiag = ∅) : (s : Set α).infsep = 0

Proof state:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : DecidableEq α
s : Finset α
hs : ¬s.offDiag.Nonempty
⊢ (↑s).infsep = 0

Tactic:
rw [Finset.coe_infsep, dif_neg hs]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : DecidableEq α
s : Finset α
hs : s.offDiag = ∅
⊢ (↑s).infsep = 0

Tactic:
rw [← Finset.not_nonempty_iff_eq_empty] at hs

Result:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : DecidableEq α
s : Finset α
hs : ¬s.offDiag.Nonempty
⊢ (↑s).infsep = 0