harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean
lemma prod_boole : ∏ i ∈ s, (ite (p i) 1 0 : M₀) = ite (∀ i ∈ s, p i) 1 0

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
s : Finset ι
⊢ (∏ i ∈ s, if p i then 1 else 0) = if ∀ i ∈ s, p i then 1 else 0

Tactic:
rw [prod_ite_zero, prod_const_one]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/End.lean
theorem μ_naturalityᵣ {m n n' : M} (g : n ⟶ n') (X : C) [F.LaxMonoidal] :
    (F.map g).app ((F.obj m).obj X) ≫ (μ F m n').app X =
      (μ F m n).app X ≫ (F.map (m ◁ g)).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n n' : M
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.map g).app ((F.obj m).obj X) ≫ (μ F m n').app X = (μ F m n).app X ≫ (F.map (m ◁ g)).app X

Tactic:
rw [← id_tensorHom, ← μ_naturality₂ F (𝟙 m) g X]

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n n' : M
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.map g).app ((F.obj m).obj X) ≫ (μ F m n').app X =
    (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map (𝟙 m)).app X) ≫ (μ F m n').app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n n' : M
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.map g).app ((F.obj m).obj X) ≫ (μ F m n').app X =
    (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map (𝟙 m)).app X) ≫ (μ F m n').app X

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_mul : eval .mul = ((· * ·) : BitVec w → BitVec w → BitVec w)

Proof state:
w : Nat
⊢ mul.eval = fun x1 x2 => x1 * x2

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioo_subset_Ioc_self : Ioo a b ⊆ Ioc a b

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ Set.Ioc a b

Tactic:
exact Set.Ioo_subset_Ioc_self

Result:
no goals

Proof state:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ioc a b

Tactic:
rw [← coe_subset, coe_Ioo, coe_Ioc]

Result:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ Set.Ioc a b
-- Mathlib/Algebra/Group/Int/Units.lean
lemma isUnit_iff_natAbs_eq : IsUnit u ↔ u.natAbs = 1

Proof state:
u : ℤ
⊢ IsUnit u ↔ u.natAbs = 1

Tactic:
simp [natAbs_eq_iff, isUnit_iff]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem ofAdd_list_prod (s : List α) : ofAdd s.sum = (s.map ofAdd).prod

Proof state:
α : Type u_3
inst✝ : AddMonoid α
s : List α
⊢ s.sum = s.prod

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
inst✝ : AddMonoid α
s : List α
⊢ ofAdd s.sum = (List.map (⇑ofAdd) s).prod

Tactic:
simp [ofAdd]

Result:
α : Type u_3
inst✝ : AddMonoid α
s : List α
⊢ s.sum = s.prod
-- Mathlib/Algebra/Order/UpperLower.lean
theorem mul_upperClosure : s * upperClosure t = upperClosure (s * t)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
⊢ s * ↑(upperClosure t) = ↑(upperClosure (s * t))

Tactic:
simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, upperClosure_iUnion, upperClosure_smul,
  UpperSet.coe_iInf₂]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
⊢ ⋃ a ∈ s, a • ↑(upperClosure t) = ⋃ i ∈ s, ↑(i • upperClosure t)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
⊢ ⋃ a ∈ s, a • ↑(upperClosure t) = ⋃ i ∈ s, ↑(i • upperClosure t)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma leftUnshift_neg {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') :
    (-γ).leftUnshift n hn = -γ.leftUnshift n hn

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
⊢ (leftShiftAddEquiv K L n a n' hn).symm (-γ) = -γ.leftUnshift n hn

Tactic:
apply _root_.map_neg

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
⊢ (-γ).leftUnshift n hn = -γ.leftUnshift n hn

Tactic:
change (leftShiftAddEquiv K L n a n' hn).symm (-γ) = _

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
⊢ (leftShiftAddEquiv K L n a n' hn).symm (-γ) = -γ.leftUnshift n hn
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem tail_eq_tailD (l) : @tail α l = tailD l []

Proof state:
α : Type u_1
l : List α
⊢ l.tail = l.tailD []

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem bliminf_true (f : Filter β) (u : β → α) : (bliminf u f fun _ => True) = liminf u f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ (bliminf u f fun x => True) = liminf u f

Tactic:
simp [bliminf_eq, liminf_eq]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem _root_.Irreducible.normalizedFactors_pow {p : α} (hp : Irreducible p) (k : ℕ) :
    normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
⊢ normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

Tactic:
rw [UniqueFactorizationMonoid.normalizedFactors_pow, normalizedFactors_irreducible hp,
  Multiset.nsmul_singleton]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
/-- A new right option cannot hurt Right. -/
lemma insertRight_le (x x' : PGame) : insertRight x x' ≤ x

Proof state:
x x' : PGame
⊢ -x ≤ (-x).insertLeft (-x')

Tactic:
exact le_insertLeft _ _

Result:
no goals

Proof state:
x x' : PGame
⊢ x.insertRight x' ≤ x

Tactic:
rw [← neg_le_neg_iff, ← neg_insertLeft_neg]

Result:
x x' : PGame
⊢ -x ≤ (-x).insertLeft (-x')
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ioc_sub_one_left_eq_Icc (a b : α) : Ioc (a - 1) b = Icc a b

Proof state:
α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioc (a - 1) b = Icc a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_left_eq_Icc a b

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem refl_restr_target (s : Set α) : ((PartialEquiv.refl α).restr s).target = s

Proof state:
α : Type u_1
s : Set α
⊢ ((PartialEquiv.refl α).restr s).target = s

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Filter.lean
theorem filter_nonempty_iff : (s.filter p).Nonempty ↔ ∃ a ∈ s, p a

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ (filter p s).Nonempty ↔ ∃ a ∈ s, p a

Tactic:
simp only [nonempty_iff_ne_empty, Ne, filter_eq_empty_iff, Classical.not_not, not_forall,
  exists_prop]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem single_one_eq_pow {R : Type _} [Ring R] (n : ℕ) :
    single (n : ℤ) (1 : R) = single (1 : ℤ) 1 ^ n

Proof state:
case zero
R : Type u_2
inst✝ : Ring R
⊢ (single ↑0) 1 = (single 1) 1 ^ 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_2
inst✝ : Ring R
n : ℕ
⊢ (single ↑n) 1 = (single 1) 1 ^ n

Tactic:
induction' n with n h_ind

Result:
case zero
R : Type u_2
inst✝ : Ring R
⊢ (single ↑0) 1 = (single 1) 1 ^ 0

case succ
R : Type u_2
inst✝ : Ring R
n : ℕ
h_ind : (single ↑n) 1 = (single 1) 1 ^ n
⊢ (single ↑(n + 1)) 1 = (single 1) 1 ^ (n + 1)

Proof state:
case succ
R : Type u_2
inst✝ : Ring R
n : ℕ
h_ind : (single ↑n) 1 = (single 1) 1 ^ n
⊢ (single ↑(n + 1)) 1 = (single 1) 1 ^ (n + 1)

Tactic:
rw [← Int.ofNat_add_one_out, pow_succ', ← h_ind, HahnSeries.single_mul_single, one_mul,
  add_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
/-- Transfer reflection of limits along an equivalence in the shape. -/
lemma reflectsLimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
    [ReflectsLimitsOfShape J F] : ReflectsLimitsOfShape J' F where
  reflectsLimit {K} :=
    { reflects := fun {c} t => ⟨by
        apply IsLimit.ofWhiskerEquivalence e
        apply isLimitOfReflects F
        apply IsLimit.ofIsoLimit _ (Functor.mapConeWhisker _).symm
        exact IsLimit.whiskerEquivalence t _⟩ }

Proof state:
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (F.mapCone (Cone.whisker e.functor c))

Tactic:
apply IsLimit.ofIsoLimit _ (Functor.mapConeWhisker _).symm

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (Cone.whisker e.functor (F.mapCone c))

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (Cone.whisker e.functor c)

Tactic:
apply isLimitOfReflects F

Result:
case t
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (F.mapCone (Cone.whisker e.functor c))

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (Cone.whisker e.functor (F.mapCone c))

Tactic:
exact IsLimit.whiskerEquivalence t _

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit c

Tactic:
apply IsLimit.ofWhiskerEquivalence e

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (Cone.whisker e.functor c)
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem QuadraticMap.toMatrix'_smul (a : R) (Q : QuadraticMap R (n → R) R) :
    (a • Q).toMatrix' = a • Q.toMatrix'

Proof state:
R : Type u_3
n : Type w
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Invertible 2
a : R
Q : QuadraticMap R (n → R) R
⊢ (a • Q).toMatrix' = a • Q.toMatrix'

Tactic:
simp only [toMatrix', LinearEquiv.map_smul, LinearMap.map_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/DecidableEq.lean
theorem isEqv_self_beq [BEq α] [ReflBEq α] (a : Array α) : Array.isEqv a a (· == ·) = true

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : ReflBEq α
a : Array α
⊢ (a.isEqv a fun x1 x2 => x1 == x2) = true

Tactic:
simp [isEqv, isEqvAux_self]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_fintype (α : Type u) [h : Fintype α] : #α = Fintype.card α :=
  mk_congr (Fintype.equivOfCardEq (by simp))

Proof state:
α : Type u
h : Fintype α
⊢ Fintype.card α = Fintype.card (ULift.{u, 0} (Fin (Fintype.card α)))

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma coproducts_iff {X Y : C} (f : X ⟶ Y) :
    coproducts.{w} W f ↔ ∃ (J : Type w), W.colimitsOfShape (Discrete J) f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ coproducts.{w, v, u} W f ↔ ∃ J, W.colimitsOfShape (Discrete J) f

Tactic:
simp only [coproducts, iSup_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
lemma associated_of_dvd_of_degree_eq {K} [Field K] {p q : K[X]} (hpq : p ∣ q)
    (h₁ : p.degree = q.degree) : Associated p q :=
  (Classical.em (q = 0)).elim (fun hq ↦ (show p = q by simpa [hq] using h₁) ▸ Associated.refl p)
    (associated_of_dvd_of_natDegree_le hpq · (natDegree_le_natDegree h₁.ge))

Proof state:
K : Type u_1
inst✝ : Field K
p q : K[X]
hpq : p ∣ q
h₁ : p.degree = q.degree
hq : q = 0
⊢ p = q

Tactic:
simpa [hq] using h₁

Result:
no goals
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem uniqueDiffWithinAt_Iio (a : ℝ) : UniqueDiffWithinAt ℝ (Iio a) a :=
  uniqueDiffWithinAt_convex (convex_Iio a) (by simp) (by simp)

Proof state:
a : ℝ
⊢ (interior (Iio a)).Nonempty

Tactic:
simp

Result:
no goals

Proof state:
a : ℝ
⊢ a ∈ closure (Iio a)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean
@[reassoc (attr := simp)]
lemma inr_π : biprod.inr ≫ π f g = cokernel.π (f ≫ g)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inr ≫ π f g = cokernel.π (f ≫ g)

Tactic:
simp [π]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma Affine.CoordinateRing.mk_φ (n : ℤ) : mk W (W.φ n) = mk W (C <| W.Φ n)

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (W.φ n) = (mk W) (C (W.Φ n))

Tactic:
simp_rw [φ, Φ, map_sub, map_mul, map_pow, mk_ψ, mk_Ψ_sq, Ψ, map_mul,
  mul_mul_mul_comm _ <| mk W <| ite .., Int.even_add_one, Int.even_sub_one, ← sq, ite_not,
  apply_ite C, apply_ite <| mk W, ite_pow, map_one, one_pow, mk_ψ₂_sq]

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem smul_div_one {p : R} {r : X} {s : S} : (p /ₒ s) • (r /ₒ 1) = (p • r) /ₒ s

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
p : R
r : X
s : ↥S
⊢ (p /ₒ s) • (r /ₒ 1) = p • r /ₒ s

Tactic:
simp [oreDiv_smul_char p r s 1 p 1 (by simp)]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
p : R
r : X
s : ↥S
⊢ ↑1 * p = p * ↑1

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem hasGradientAtFilter_const : HasGradientAtFilter (fun _ => c) 0 x L

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
x : F
L : Filter F
c : 𝕜
⊢ HasFDerivAtFilter (fun x => c) 0 x L

Tactic:
apply hasFDerivAtFilter_const c x L

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
x : F
L : Filter F
c : 𝕜
⊢ HasGradientAtFilter (fun x => c) 0 x L

Tactic:
rw [HasGradientAtFilter, map_zero]

Result:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
x : F
L : Filter F
c : 𝕜
⊢ HasFDerivAtFilter (fun x => c) 0 x L
-- Mathlib/Data/Matrix/Defs.lean
theorem transpose_smul {R : Type*} [SMul R α] (c : R) (M : Matrix m n α) : (c • M)ᵀ = c • Mᵀ

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
R : Type u_10
inst✝ : SMul R α
c : R
M : Matrix m n α
i✝ : n
j✝ : m
⊢ (c • M)ᵀ i✝ j✝ = (c • Mᵀ) i✝ j✝

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
R : Type u_10
inst✝ : SMul R α
c : R
M : Matrix m n α
⊢ (c • M)ᵀ = c • Mᵀ

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
R : Type u_10
inst✝ : SMul R α
c : R
M : Matrix m n α
i✝ : n
j✝ : m
⊢ (c • M)ᵀ i✝ j✝ = (c • Mᵀ) i✝ j✝
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem lipschitzWith_circleMap (c : ℂ) (R : ℝ) : LipschitzWith (Real.nnabs R) (circleMap c R) :=
  lipschitzWith_of_nnnorm_deriv_le (differentiable_circleMap _ _) fun θ =>
    NNReal.coe_le_coe.1 <| by simp

Proof state:
c : ℂ
R θ : ℝ
⊢ ↑‖deriv (circleMap c R) θ‖₊ ≤ ↑(Real.nnabs R)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublistsLen_succ_cons (n) (a : α) (l) :
    sublistsLen (n + 1) (a :: l) = sublistsLen (n + 1) l ++ (sublistsLen n l).map (cons a)

Proof state:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (id ∘ cons a) (sublistsLen n l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) (a :: l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)

Tactic:
rw [sublistsLen, sublistsLenAux, sublistsLenAux_eq, sublistsLenAux_eq, map_id,
    append_nil]

Result:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (id ∘ cons a) (sublistsLen n l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem homothety_one (c : P1) : homothety c (1 : k) = id k P1

Proof state:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c : P1
⊢ homothety c 1 = id k P1

Tactic:
ext p

Result:
case h
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c p : P1
⊢ (homothety c 1) p = (id k P1) p

Proof state:
case h
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst✝³ : CommRing k
inst✝² : AddCommGroup V1
inst✝¹ : AffineSpace V1 P1
inst✝ : Module k V1
c p : P1
⊢ (homothety c 1) p = (id k P1) p

Tactic:
simp [homothety_apply]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma d_toCycles [K.HasHomology k] :
    K.d i j ≫ K.toCycles j k = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
inst✝ : K.HasHomology k
⊢ K.d i j ≫ K.toCycles j k = 0

Tactic:
simp only [← cancel_mono (K.iCycles k), assoc, toCycles_i, d_comp_d, zero_comp]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
protected lemma exists_congr (h : ∀ a, p a ↔ q (e a)) : (∃ a, p a) ↔ ∃ b, q b :=
  e.exists_congr_left.trans <| by simp [h]

Proof state:
α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ (∃ b, p (e.symm b)) ↔ ∃ b, q b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem pi_pos : 0 < π :=
  lt_of_lt_of_le (by norm_num) two_le_pi

Proof state:
⊢ 0 < 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/LinearAlgebra/FreeProduct/Basic.lean
theorem lof_map_one (i : I) : lof R A i 1 = 1

Proof state:
I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
⊢ (RingQuot.mkAlgHom R (rel R A)) ((ι R) ((DirectSum.lof R I A i) 1)) = 1

Tactic:
exact identify_one R A i

Result:
no goals

Proof state:
I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
⊢ (lof R A i) 1 = 1

Tactic:
rw [lof]

Result:
I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
⊢ (ι' R A ∘ₗ DirectSum.lof R I A i) 1 = 1

Proof state:
I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
⊢ (ι' R A ∘ₗ DirectSum.lof R I A i) 1 = 1

Tactic:
dsimp [mkAlgHom]

Result:
I : Type u
inst✝³ : DecidableEq I
R : Type v
inst✝² : CommSemiring R
A : I → Type w
inst✝¹ : (i : I) → Semiring (A i)
inst✝ : (i : I) → Algebra R (A i)
i : I
⊢ (RingQuot.mkAlgHom R (rel R A)) ((ι R) ((DirectSum.lof R I A i) 1)) = 1
-- Mathlib/Algebra/Lie/Weights/Basic.lean
/-- Lie module weight spaces are independent.

See also `LieModule.iSupIndep_genWeightSpace'`. -/
lemma iSupIndep_genWeightSpace [NoZeroSMulDivisors R M] :
    iSupIndep fun χ : L → R ↦ genWeightSpace M χ

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
⊢ iSupIndep fun i => ⨅ i_1, ↑(genWeightSpaceOf M (i i_1) i_1)

Tactic:
exact Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo (toEnd R L M)
  (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem)

Result:
no goals

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
⊢ iSupIndep fun χ => genWeightSpace M χ

Tactic:
simp only [LieSubmodule.iSupIndep_iff_toSubmodule, genWeightSpace,
  LieSubmodule.iInf_toSubmodule]

Result:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
⊢ iSupIndep fun i => ⨅ i_1, ↑(genWeightSpaceOf M (i i_1) i_1)
-- Mathlib/Topology/Inseparable.lean
theorem inseparable_iff_mem_closure :
    (x ~ᵢ y) ↔ x ∈ closure ({y} : Set X) ∧ y ∈ closure ({x} : Set X) :=
  inseparable_iff_specializes_and.trans <| by simp only [specializes_iff_mem_closure, and_comm]

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ x ⤳ y ∧ y ⤳ x ↔ x ∈ closure {y} ∧ y ∈ closure {x}

Tactic:
simp only [specializes_iff_mem_closure, and_comm]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_bound {x : ℝ} (hx : |x| ≤ 1) {n : ℕ} (hn : 0 < n) :
    |exp x - ∑ m ∈ range n, x ^ m / m.factorial| ≤ |x| ^ n * (n.succ / (n.factorial * n))

Proof state:
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
⊢ |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ |x| ^ n * (↑n.succ / (↑n.factorial * ↑n))

Tactic:
have hxc : ‖(x : ℂ)‖ ≤ 1 := mod_cast hx

Result:
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖↑x‖ ≤ 1
⊢ |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ |x| ^ n * (↑n.succ / (↑n.factorial * ↑n))

Proof state:
x : ℝ
hx : |x| ≤ 1
n : ℕ
hn : 0 < n
hxc : ‖↑x‖ ≤ 1
⊢ |rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ |x| ^ n * (↑n.succ / (↑n.factorial * ↑n))

Tactic:
convert exp_bound hxc hn using 2 <;>
norm_cast

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem prodCongr_refl_right (e : β₁ ≃ β₂) :
    prodCongr e (Equiv.refl α₁) = prodCongrLeft fun _ => e

Proof state:
case H.mk
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : β₁ ≃ β₂
a : β₁
b : α₁
⊢ (e.prodCongr (Equiv.refl α₁)) (a, b) = (prodCongrLeft fun x => e) (a, b)

Tactic:
simp

Result:
no goals

Proof state:
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : β₁ ≃ β₂
⊢ e.prodCongr (Equiv.refl α₁) = prodCongrLeft fun x => e

Tactic:
ext ⟨a, b⟩ : 1

Result:
case H.mk
α₁ : Type u_9
β₁ : Type u_11
β₂ : Type u_12
e : β₁ ≃ β₂
a : β₁
b : α₁
⊢ (e.prodCongr (Equiv.refl α₁)) (a, b) = (prodCongrLeft fun x => e) (a, b)
-- Mathlib/Data/Int/Order/Units.lean
theorem units_div_eq_mul (u₁ u₂ : ℤˣ) : u₁ / u₂ = u₁ * u₂

Proof state:
u₁ u₂ : ℤˣ
⊢ u₁ / u₂ = u₁ * u₂

Tactic:
rw [div_eq_mul_inv, units_inv_eq_self]

Result:
no goals