harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem inv_mul_cancel {f : CauSeq β abv} (hf) : inv f hf * f ≈ 1 := fun ε ε0 =>
  let ⟨K, K0, i, H⟩ := abv_pos_of_not_limZero hf
  ⟨i, fun j ij => by simpa [(abv_pos abv).1 (lt_of_lt_of_le K0 (H _ ij)), abv_zero abv] using ε0⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f.LimZero
ε : α
ε0 : ε > 0
K : α
K0 : K > 0
i : ℕ
H : ∀ j ≥ i, K ≤ abv (↑f j)
j : ℕ
ij : j ≥ i
⊢ abv (↑(f.inv hf * f - 1) j) < ε

Tactic:
simpa [(abv_pos abv).1 (lt_of_lt_of_le K0 (H _ ij)), abv_zero abv] using ε0

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem induction_on' {P : MvPolynomial σ R → Prop} (p : MvPolynomial σ R)
    (h1 : ∀ (u : σ →₀ ℕ) (a : R), P (monomial u a))
    (h2 : ∀ p q : MvPolynomial σ R, P p → P q → P (p + q)) : P p :=
  Finsupp.induction p
    (suffices P (monomial 0 0) by rwa [monomial_zero] at this
    show P (monomial 0 0) from h1 0 0)
    fun _ _ _ _ha _hb hPf => h2 _ _ (h1 _ _) hPf

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
P : MvPolynomial σ R → Prop
p : MvPolynomial σ R
h1 : ∀ (u : σ →₀ ℕ) (a : R), P ((monomial u) a)
h2 : ∀ (p q : MvPolynomial σ R), P p → P q → P (p + q)
this : P ((monomial 0) 0)
⊢ P 0

Tactic:
rwa [monomial_zero] at this

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem natDegree_of_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) :
    P.toPoly.natDegree = 0

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ P.toPoly.natDegree = 0

Tactic:
rw [of_c_eq_zero ha hb hc, natDegree_C]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
lemma specializingMap_iff_stableUnderSpecialization_image_singleton :
    SpecializingMap f ↔ ∀ x, StableUnderSpecialization (f '' closure {x})

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ SpecializingMap f ↔ ∀ (x : X), StableUnderSpecialization (f '' closure {x})

Tactic:
simpa only [closure_singleton_eq_Iic] using Relation.fibration_iff_isLowerSet_image_Iic

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_decide {α} (p : Prop) [Decidable p] (t e : α) :
    cond (decide p) t e = if p then t else e

Proof state:
α : Type u_1
p : Prop
inst✝ : Decidable p
t e : α
⊢ (bif decide p then t else e) = if p then t else e

Tactic:
simp [cond_eq_ite]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
@[simp]
lemma equation_zero : W'.Equation 0 0 ↔ W'.a₆ = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ W'.Equation 0 0 ↔ W'.a₆ = 0

Tactic:
rw [Equation, evalEval_polynomial_zero, neg_eq_zero]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem annihilator_eq_top_iff : N.annihilator = ⊤ ↔ N = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ N.annihilator = ⊤ ↔ N = ⊥

Tactic:
rw [annihilator, Module.annihilator_eq_top_iff, Submodule.subsingleton_iff_eq_bot]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b' ↔ b = b'

Proof state:
⊢ ∀ {b b' : Bool}, ofBool b = ofBool b' ↔ b = b'

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Pi.lean
/-- Taking a product over `univ.pi t` is the same as taking the product over `Fintype.piFinset t`.
`univ.pi t` and `Fintype.piFinset t` are essentially the same `Finset`, but differ
in the type of their element, `univ.pi t` is a `Finset (Π a ∈ univ, t a)` and
`Fintype.piFinset t` is a `Finset (Π a, t a)`. -/
@[to_additive "Taking a sum over `univ.pi t` is the same as taking the sum over
`Fintype.piFinset t`. `univ.pi t` and `Fintype.piFinset t` are essentially the same `Finset`,
but differ in the type of their element, `univ.pi t` is a `Finset (Π a ∈ univ, t a)` and
`Fintype.piFinset t` is a `Finset (Π a, t a)`."]
lemma prod_univ_pi [DecidableEq ι] [Fintype ι] {κ : ι → Type*} (t : ∀ i, Finset (κ i))
    (f : (∀ i ∈ (univ : Finset ι), κ i) → β) :
    ∏ x ∈ univ.pi t, f x = ∏ x ∈ Fintype.piFinset t, f fun a _ ↦ x a

Proof state:
ι : Type u_1
β : Type u_2
inst✝² : CommMonoid β
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : ((i : ι) → i ∈ univ → κ i) → β
⊢ ∏ x ∈ univ.pi t, f x = ∏ x ∈ Fintype.piFinset t, f fun a x_1 => x a

Tactic:
apply prod_nbij' (fun x i ↦ x i <| mem_univ _) (fun x i _ ↦ x i) <;> simp

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem cons_prefix_iff : a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
a b : α
⊢ a :: l₁ <+: b :: l₂ ↔ a = b ∧ l₁ <+: l₂

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Azumaya/Matrix.lean
lemma AlgHom.mulLeftRightMatrix.inv_comp :
    (AlgHom.mulLeftRightMatrix_inv R n).comp
    (AlgHom.mulLeftRight R (Matrix n n R)).toLinearMap = .id :=
  Basis.ext (Basis.tensorProduct (Matrix.stdBasis _ _ _)
    ((Matrix.stdBasis _ _ _).map (opLinearEquiv ..)))
  fun ⟨⟨i0, j0⟩, k0, l0⟩ ↦ by
    simp [stdBasis_eq_stdBasisMatrix, ite_and, Fintype.sum_prod_type,
      mulLeftRight_apply, stdBasisMatrix, Matrix.mul_apply]

Proof state:
R : Type u_1
n : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x✝ : (n × n) × n × n
i0 j0 k0 l0 : n
⊢ (mulLeftRightMatrix_inv R n ∘ₗ (mulLeftRight R (Matrix n n R)).toLinearMap)
      (((stdBasis R n n).tensorProduct ((stdBasis R n n).map (opLinearEquiv R))) ((i0, j0), k0, l0)) =
    LinearMap.id (((stdBasis R n n).tensorProduct ((stdBasis R n n).map (opLinearEquiv R))) ((i0, j0), k0, l0))

Tactic:
simp [stdBasis_eq_stdBasisMatrix, ite_and, Fintype.sum_prod_type,
  mulLeftRight_apply, stdBasisMatrix, Matrix.mul_apply]

Result:
no goals
-- Mathlib/Logic/ExistsUnique.lean
theorem existsUnique_prop {p q : Prop} : (∃! _ : p, q) ↔ p ∧ q

Proof state:
p q : Prop
⊢ (∃! x, q) ↔ p ∧ q

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Perfectoid/Untilt.lean
lemma untiltAux_smodEq_untiltFun (x : PreTilt O p) (n : ℕ) :
    x.untiltAux n ≡ x.untiltFun [SMOD (span {(p : O)}) ^ n]

Proof state:
O : Type u_1
inst✝³ : CommRing O
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsPrecomplete (span {↑p}) O
x : PreTilt O p
n : ℕ
⊢ x.untiltAux n ≡ x.untiltFun [SMOD span {↑p} ^ n]

Tactic:
simpa [untiltFun] using Classical.choose_spec x.exists_smodEq_untiltAux n

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Abs.lean
theorem HasFDerivWithinAt.abs_of_pos (hf : HasFDerivWithinAt f f' s x)
    (h₀ : 0 < f x) : HasFDerivWithinAt (fun x ↦ |f x|) f' s x

Proof state:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : 0 < f x
⊢ f' = 1 • f'

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : 0 < f x
⊢ HasFDerivWithinAt (fun x => |f x|) f' s x

Tactic:
convert (hasDerivAt_abs_pos h₀).comp_hasFDerivWithinAt x hf using 1

Result:
case h.e'_12
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
f' : E →L[ℝ] ℝ
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : 0 < f x
⊢ f' = 1 • f'
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem MeasurePreserving.setLIntegral_comp_preimage_emb {mb : MeasurableSpace β} {ν : Measure β}
    {g : α → β} (hg : MeasurePreserving g μ ν) (hge : MeasurableEmbedding g) (f : β → ℝ≥0∞)
    (s : Set β) : ∫⁻ a in g ⁻¹' s, f (g a) ∂μ = ∫⁻ b in s, f b ∂ν

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
mb : MeasurableSpace β
ν : Measure β
g : α → β
hg : MeasurePreserving g μ ν
hge : MeasurableEmbedding g
f : β → ℝ≥0∞
s : Set β
⊢ ∫⁻ (a : α) in g ⁻¹' s, f (g a) ∂μ = ∫⁻ (b : β) in s, f b ∂ν

Tactic:
rw [← hg.map_eq, hge.restrict_map, hge.lintegral_map]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem mk_toType (o : Ordinal) : #o.toType = o.card :=
  (Ordinal.card_type _).symm.trans <| by rw [Ordinal.type_toType]

Proof state:
o : Ordinal.{u_1}
⊢ (type ?m.151078).card = o.card

Tactic:
rw [Ordinal.type_toType]

Result:
no goals
-- Mathlib/Data/List/TakeDrop.lean
@[simp] lemma drop_take_append_drop (x : List α) (m n : ℕ) :
    (x.drop m).take n ++ x.drop (m + n) = x.drop m

Proof state:
α : Type u
x : List α
m n : ℕ
⊢ take n (drop m x) ++ drop (m + n) x = drop m x

Tactic:
rw [← drop_drop, take_append_drop]

Result:
no goals
-- Mathlib/MeasureTheory/Group/AEStabilizer.lean
@[to_additive (attr := simp)]
lemma aestabilizer_univ : aestabilizer G μ univ = ⊤ := top_unique fun _ _ ↦ by simp

Proof state:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝² : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x✝¹ : G
x✝ : x✝¹ ∈ ⊤
⊢ x✝¹ ∈ aestabilizer G μ univ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem isTheta_exp_comp_one {f : α → ℝ} :
    (fun x => exp (f x)) =Θ[l] (fun _ => 1 : α → ℝ) ↔ IsBoundedUnder (· ≤ ·) l fun x => |f x|

Proof state:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ ((fun x => rexp (f x)) =Θ[l] fun x => 1) ↔ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => |f x|

Tactic:
simp only [← exp_zero, isTheta_exp_comp_exp_comp, sub_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem LinearIndepOn.id_imageₛ {s : Set M} {f : M →ₗ[R] M'} (hs : LinearIndepOn R id s)
    (hf_inj : Set.InjOn f (span R s)) : LinearIndepOn R id (f '' s) :=
  id_image <| hs.map_injOn f (by simpa using hf_inj)

Proof state:
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
f : M →ₗ[R] M'
hs : LinearIndepOn R _root_.id s
hf_inj : InjOn ⇑f ↑(span R s)
⊢ InjOn ⇑f ↑(span R (_root_.id '' s))

Tactic:
simpa using hf_inj

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem nfpBFamily_lt_ord_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal → Ordinal} {c}
    (hc : IsRegular c) (ho : o.card < c) (hc' : c ≠ ℵ₀)
    (hf : ∀ (i hi), ∀ b < c.ord, f i hi b < c.ord) {a} :
    a < c.ord → nfpBFamily.{u, u} o f a < c.ord :=
  nfpBFamily_lt_ord_lift_of_isRegular hc (by rwa [lift_id]) hc' hf

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
ho : o.card < c
hc' : c ≠ ℵ₀
hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c.ord, f i hi b < c.ord
a : Ordinal.{u}
⊢ lift.{u, u} o.card < c

Tactic:
rwa [lift_id]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
lemma forall_mem_image {p : β → Prop} : (∀ y ∈ s.image f, p y) ↔ ∀ ⦃x⦄, x ∈ s → p (f x)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
⊢ (∀ y ∈ image f s, p y) ↔ ∀ ⦃x : α⦄, x ∈ s → p (f x)

Tactic:
simp

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

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

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_self_mul_transpose [LinearOrderedField R] [Fintype m] (A : Matrix m n R) :
    (A * Aᵀ).rank = A.rank

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : LinearOrderedField R
inst✝ : Fintype m
A : Matrix m n R
⊢ (A * Aᵀ).rank = A.rank

Tactic:
simpa only [rank_transpose, transpose_transpose] using rank_transpose_mul_self Aᵀ

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem fixed_point₂ {f : Code → ℕ →. ℕ} (hf : Partrec₂ f) : ∃ c : Code, eval c = f c :=
  let ⟨cf, ef⟩ := exists_code.1 hf
  (fixed_point (curry_prim.comp (_root_.Primrec.const cf) Primrec.encode).to_comp).imp fun c e =>
    funext fun n => by simp [e.symm, ef, Part.map_id']

Proof state:
f : Code → ℕ →. ℕ
hf : Partrec₂ f
cf : Code
ef : cf.eval = fun n => (↑(decode n)).bind fun a => Part.map encode ((fun p => f p.1 p.2) a)
c : Code
e : (cf.curry (encode c)).eval = c.eval
n : ℕ
⊢ c.eval n = f c n

Tactic:
simp [e.symm, ef, Part.map_id']

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
theorem eval_one_cyclotomic_prime {R : Type*} [CommRing R] {p : ℕ} [hn : Fact p.Prime] :
    eval 1 (cyclotomic p R) = p

Proof state:
R : Type u_1
inst✝ : CommRing R
p : ℕ
hn : Fact (Nat.Prime p)
⊢ eval 1 (cyclotomic p R) = ↑p

Tactic:
simp only [cyclotomic_prime, eval_X, one_pow, Finset.sum_const, eval_pow, eval_finset_sum,
  Finset.card_range, smul_one_eq_cast]

Result:
no goals
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem uniqueDiffWithinAt_of_mem_nhds (h : s ∈ 𝓝 x) : UniqueDiffWithinAt 𝕜 s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
s : Set E
h : s ∈ 𝓝 x
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
simpa only [univ_inter] using uniqueDiffWithinAt_univ.inter h

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_sdiff_left' : (x \ y) \ z = x \ y ⊓ x \ z

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x \ y) \ z = x \ y ⊓ x \ z

Tactic:
rw [sdiff_sdiff_left, sdiff_sup]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
    {v : β k} {h} : getValueCast a (insertEntry k v l) h =
    if h' : k == a then cast (congrArg β (eq_of_beq h')) v
    else getValueCast a l (containsKey_of_containsKey_insertEntry h (Bool.eq_false_iff.2 h'))

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (insertEntry k v l) = true
⊢ getValueCast a (insertEntry k v l) h = if h' : (k == a) = true then cast ⋯ v else getValueCast a l ⋯

Tactic:
rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, apply_dite Option.some,
  getValueCast?_insertEntry]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (insertEntry k v l) = true
⊢ (if h : (k == a) = true then some (cast ⋯ v) else getValueCast? a l) =
    if h : (k == a) = true then some (cast ⋯ v) else some (getValueCast a l ⋯)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : containsKey a (insertEntry k v l) = true
⊢ (if h : (k == a) = true then some (cast ⋯ v) else getValueCast? a l) =
    if h : (k == a) = true then some (cast ⋯ v) else some (getValueCast a l ⋯)

Tactic:
simp only [← getValueCast?_eq_some_getValueCast]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem liftOn₂_mk {α : Type*} (f : M × S → M × S → α)
    (wd : ∀ (p q p' q' : M × S), p ≈ p' → q ≈ q' → f p q = f p' q') (m m' : M)
    (s s' : S) : liftOn₂ (mk m s) (mk m' s') f wd = f ⟨m, s⟩ ⟨m', s'⟩

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_2
f : M × ↥S → M × ↥S → α
wd : ∀ (p q p' q' : M × ↥S), p ≈ p' → q ≈ q' → f p q = f p' q'
m m' : M
s s' : ↥S
⊢ (mk m s).liftOn₂ (mk m' s') f wd = f (m, s) (m', s')

Tactic:
convert Quotient.liftOn₂_mk f wd _ _

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_one : Gamma 1 = 1

Proof state:
⊢ Gamma 1 = 1

Tactic:
rw [Gamma_eq_integral] <;> simp

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
protected lemma le_max_iff : (a : WithZero α) ≤ max (b : WithZero α) c ↔ a ≤ max b c

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ↑a ≤ ↑b ⊔ ↑c ↔ a ≤ b ⊔ c

Tactic:
simp only [WithZero.coe_le_coe, le_max_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Grp_.lean
theorem lift_inv_left_eq {A : C} {B : Grp_ C} (f g h : A ⟶ B.X) :
    lift (f ≫ B.inv) g ≫ B.mul = h ↔ g = lift f h ≫ B.mul

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f g h : A ⟶ B.X
⊢ lift (f ≫ B.inv) g ≫ B.mul = h ↔ g = lift f h ≫ B.mul

Tactic:
rw [eq_comm, eq_lift_inv_left, eq_comm]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic_zero (R : Type*) [Ring R] : cyclotomic 0 R = 1

Proof state:
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 0 R = 1

Tactic:
simp only [cyclotomic, dif_pos]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem count_some (hp : Irreducible p) (s : Multiset _) :
    count p (WithTop.some s) = s.count ⟨p, hp⟩

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
s : Multiset { a // Irreducible a }
⊢ p.count ↑s = Multiset.count ⟨p, hp⟩ s

Tactic:
simp only [count, dif_pos hp, bcount]

Result:
no goals
-- Mathlib/Algebra/Group/Int/Even.lean
lemma even_iff : Even n ↔ n % 2 = 0 where
  mp := fun ⟨m, hm⟩ ↦ by simp [← Int.two_mul, hm]
  mpr h := ⟨n / 2, (emod_add_ediv n 2).symm.trans (by simp [← Int.two_mul, h])⟩

Proof state:
n : ℤ
x✝ : Even n
m : ℤ
hm : n = m + m
⊢ n % 2 = 0

Tactic:
simp [← Int.two_mul, hm]

Result:
no goals

Proof state:
n : ℤ
h : n % 2 = 0
⊢ n % 2 + 2 * (n / 2) = n / 2 + n / 2

Tactic:
simp [← Int.two_mul, h]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem image_mul_right' : (· * b⁻¹) '' t = (· * b) ⁻¹' t

Proof state:
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ (fun x => x * b⁻¹) '' t = (fun x => x * b) ⁻¹' t

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean
theorem π_f_succ (n : ℕ) : P.π.f (n + 1) = 0 :=
  (isZero_single_obj_X _ _ _ _ (by simp)).eq_of_tgt _ _

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem insertNth_last' (x : β) (p : Fin n → β) :
    @insertNth _ (fun _ ↦ β) (last n) x p = snoc p x

Proof state:
n : ℕ
β : Sort u_2
x : β
p : Fin n → β
⊢ (last n).insertNth x p = snoc p x

Tactic:
simp [insertNth_last]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem bind_map (m : Multiset α) (n : β → Multiset γ) (f : α → β) :
    bind (map f m) n = bind m fun a => n (f a) :=
  Multiset.induction_on m (by simp) (by simp +contextual)

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : β → Multiset γ
f : α → β
⊢ (map f 0).bind n = bind 0 fun a => n (f a)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : β → Multiset γ
f : α → β
⊢ ∀ (a : α) (s : Multiset α),
    ((map f s).bind n = s.bind fun a => n (f a)) → (map f (a ::ₘ s)).bind n = (a ::ₘ s).bind fun a => n (f a)

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_insertIfNew [LawfulBEq α] (h : m.1.WF) {k a : α} {v : β k} {h₁} :
    (m.insertIfNew k v).get a h₁ =
      if h₂ : k == a ∧ m.contains k = false then cast (congrArg β (eq_of_beq h₂.1)) v
      else m.get a (contains_of_contains_insertIfNew' _ h h₁ h₂)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k a : α
v : β k
h₁ : (m.insertIfNew k v).contains a = true
⊢ (m.insertIfNew k v).get a h₁ = if h₂ : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.get a ⋯

Tactic:
simp_to_model [insertIfNew] using List.getValueCast_insertEntryIfNew

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem pi_inter_compl (s : Set ι) : pi s t ∩ pi sᶜ t = pi univ t

Proof state:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
s : Set ι
⊢ s.pi t ∩ sᶜ.pi t = univ.pi t

Tactic:
rw [← union_pi, union_compl_self]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem gluedLiftPullbackMap_snd (i j : 𝒰.J) :
    gluedLiftPullbackMap 𝒰 f g s i j ≫ pullback.snd _ _ = pullback.snd _ _ ≫ pullback.snd _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
s : PullbackCone f g
i j : 𝒰.J
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫ pullback.snd (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) =
    pullback.snd ((Cover.pullbackCover 𝒰 s.fst).map i) ((Cover.pullbackCover 𝒰 s.fst).map j) ≫
      pullback.snd s.fst (𝒰.map j)

Tactic:
simp [gluedLiftPullbackMap]

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma mem_compls : a ∈ sᶜˢ ↔ aᶜ ∈ s

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
a : α
⊢ a ∈ sᶜˢ ↔ aᶜ ∈ s

Tactic:
rw [Iff.comm, ← mem_map' ⟨compl, compl_injective⟩, Embedding.coeFn_mk, compl_compl, compls]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ (μ : Measure α)
    {f : α → ℝ≥0∞} {s : Set α} (hf : AEMeasurable f (μ.restrict s)) (g : α → ℝ≥0∞)
    (hs : MeasurableSet s) (h'f : ∀ᵐ x ∂μ.restrict s, f x < ∞) :
    ∫⁻ a in s, g a ∂μ.withDensity f = ∫⁻ a in s, (f * g) a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
g : α → ℝ≥0∞
hs : MeasurableSet s
h'f : ∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul_non_measurable₀ _ hf h'f]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
lemma equicontinuous_restrict_iff (F : ι → X → α) {S : Set X} :
    Equicontinuous (S.restrict ∘ F) ↔ EquicontinuousOn F S

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
⊢ Equicontinuous (S.restrict ∘ F) ↔ EquicontinuousOn F S

Tactic:
simp [Equicontinuous, EquicontinuousOn, equicontinuousAt_restrict_iff]

Result:
no goals
-- Mathlib/Logic/Lemmas.lean
theorem iff_assoc {a b c : Prop} : ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))

Proof state:
a b c : Prop
⊢ ((a ↔ b) ↔ c) ↔ (a ↔ (b ↔ c))

Tactic:
tauto

Result:
no goals
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem sub_mem_pNilradical_iff_pow_expChar_pow_eq {R : Type*} [CommRing R] {p : ℕ} [ExpChar R p]
    {x y : R} : x - y ∈ pNilradical R p ↔ ∃ n : ℕ, x ^ p ^ n = y ^ p ^ n

Proof state:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : ExpChar R p
x y : R
⊢ x - y ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = y ^ p ^ n

Tactic:
simp_rw [mem_pNilradical, sub_pow_expChar_pow, sub_eq_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem gluedLiftPullbackMap_fst (i j : 𝒰.J) :
    gluedLiftPullbackMap 𝒰 f g s i j ≫ pullback.fst _ _ =
      pullback.fst _ _ ≫
        (pullbackSymmetry _ _).hom ≫
          pullback.map _ _ _ _ (𝟙 _) s.snd f (Category.id_comp _).symm s.condition

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
s : PullbackCone f g
i j : 𝒰.J
⊢ gluedLiftPullbackMap 𝒰 f g s i j ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) =
    pullback.fst ((Cover.pullbackCover 𝒰 s.fst).map i) ((Cover.pullbackCover 𝒰 s.fst).map j) ≫
      (pullbackSymmetry s.fst (𝒰.map i)).hom ≫ pullback.map (𝒰.map i) s.fst (𝒰.map i ≫ f) g (𝟙 (𝒰.obj i)) s.snd f ⋯ ⋯

Tactic:
simp [gluedLiftPullbackMap]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_inv_eq_mul : a / b⁻¹ = a * b

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ a / b⁻¹ = a * b

Tactic:
simp

Result:
no goals