harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Monadic.lean
theorem forM_map [Monad m] [LawfulMonad m] (o : Option α) (g : α → β) (f : β → m PUnit) :
    (o.map g).forM f = o.forM (fun a => f (g a))

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : Monad m
inst✝ : LawfulMonad m
o : Option α
g : α → β
f : β → m PUnit
⊢ (Option.map g o).forM f = o.forM fun a => f (g a)

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem isSuccLimitRecOn_of_isSuccLimit (hb : IsSuccLimit b) :
    isSuccLimitRecOn b hm hs hl = hl b hb

Proof state:
α : Type u_1
b : α
C : α → Sort u_2
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hm : (a : α) → IsMin a → C a
hs : (a : α) → ¬IsMax a → C (succ a)
hl : (a : α) → IsSuccLimit a → C a
hb : IsSuccLimit b
⊢ isSuccLimitRecOn b hm hs hl = hl b hb

Tactic:
rw [isSuccLimitRecOn, isSuccPrelimitRecOn_of_isSuccPrelimit _ _ hb.isSuccPrelimit,
  dif_neg hb.not_isMin]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
@[to_additive tsum_setProd_singleton_left]
lemma tprod_setProd_singleton_left (b : β) (t : Set γ) (f : β × γ → α) :
    (∏' x : {b} ×ˢ t, f x) = ∏' c : t, f (b, c)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
b : β
t : Set γ
f : β × γ → α
⊢ ∏' (x : ↑({b} ×ˢ t)), f ↑x = ∏' (c : ↑t), f (b, ↑c)

Tactic:
rw [tprod_congr_set_coe _ Set.singleton_prod, tprod_image _ (Prod.mk.inj_left b).injOn]

Result:
no goals
-- Mathlib/RingTheory/Nakayama.lean
theorem le_of_le_smul_of_le_jacobson_bot {R M} [CommRing R] [AddCommGroup M] [Module R M]
    {I : Ideal R} {N N' : Submodule R M} (hN' : N'.FG)
    (hIJ : I ≤ jacobson ⊥) (hNN : N' ≤ N ⊔ I • N') : N' ≤ N

Proof state:
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ ⊥.jacobson
hNN : N' ≤ N ⊔ I • N'
⊢ N' ≤ N

Tactic:
rw [← sup_eq_left, sup_eq_sup_smul_of_le_smul_of_le_jacobson hN' hIJ hNN, bot_smul, sup_bot_eq]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem remainingToString {it} (h : ValidFor l r it) : it.remainingToString = ⟨r⟩

Proof state:
case refl
l r : List Char
h : ValidFor l r { s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l } }
⊢ { s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l } }.remainingToString = { data := r }

Tactic:
simpa [Iterator.remainingToString, List.reverseAux_eq] using extract_of_valid l.reverse r []

Result:
no goals

Proof state:
l r : List Char
it : Iterator
h : ValidFor l r it
⊢ it.remainingToString = { data := r }

Tactic:
cases h.out

Result:
case refl
l r : List Char
h : ValidFor l r { s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l } }
⊢ { s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l } }.remainingToString = { data := r }
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem laverage_zero : ⨍⁻ _x, (0 : ℝ≥0∞) ∂μ = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ ⨍⁻ (_x : α), 0 ∂μ = 0

Tactic:
rw [laverage, lintegral_zero]

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.lt_right_of_left_lt' (hf : ConvexOn 𝕜 s f) {x y : E} {a b : 𝕜} (hx : x ∈ s)
    (hy : y ∈ s) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hfx : f x < f (a • x + b • y)) :
    f (a • x + b • y) < f y

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 < a
hb : 0 < b
hab : b + a = 1
hfx : f x < f (b • y + a • x)
⊢ f (b • y + a • x) < f y

Tactic:
exact hf.lt_left_of_right_lt' hy hx hb ha hab hfx

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hfx : f x < f (a • x + b • y)
⊢ f (a • x + b • y) < f y

Tactic:
rw [add_comm] at hab hfx ⊢

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
a b : 𝕜
hx : x ∈ s
hy : y ∈ s
ha : 0 < a
hb : 0 < b
hab : b + a = 1
hfx : f x < f (b • y + a • x)
⊢ f (b • y + a • x) < f y
-- Mathlib/Algebra/Group/Units/Defs.lean
@[to_additive]
protected lemma div_mul_cancel_right (h : IsUnit b) (a : α) : b / (a * b) = a⁻¹

Proof state:
α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ b / (a * b) = a⁻¹

Tactic:
rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left]

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} :
    (m.insertIfNew k v).get? a =
      if h : k == a ∧ m.contains k = false then some (cast (congrArg β (eq_of_beq h.1)) v)
      else m.get? a

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

Tactic:
simp_to_model [insertIfNew] using List.getValueCast?_insertEntryIfNew

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean
@[simp, norm_cast]
lemma coe_iInf {ι : Sort*} (f : ι → G.Finsubgraph) : ⨅ i, f i = (⨅ i, f i : G.Subgraph)

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
ι : Sort u_1
f : ι → G.Finsubgraph
⊢ ↑(⨅ i, f i) = ⨅ i, ↑(f i)

Tactic:
rw [iInf, coe_sInf, iInf_range]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem nonneg_iff : 0 ≤ z ↔ 0 ≤ re z ∧ im z = 0

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ z ↔ 0 ≤ re z ∧ im z = 0

Tactic:
simpa only [map_zero, eq_comm] using le_iff_re_im (z := 0) (w := z)

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem all_ae_of {ι : Sort*} {p : α → ι → Prop} (hp : ∀ᵐ a ∂μ, ∀ i, p a i) (i : ι) :
    ∀ᵐ a ∂μ, p a i

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
ι : Sort u_4
p : α → ι → Prop
hp : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), p a i
i : ι
⊢ ∀ᵐ (a : α) ∂μ, p a i

Tactic:
filter_upwards [hp] with a ha using ha i

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem attach_bind {o : Option α} {f : α → Option β} :
    (o.bind f).attach =
      o.attach.bind fun ⟨x, h⟩ => (f x).attach.map fun ⟨y, h'⟩ => ⟨y, mem_bind_iff.mpr ⟨x, h, h'⟩⟩

Proof state:
α : Type u_1
β : Type u_2
o : Option α
f : α → Option β
⊢ (o.bind f).attach =
    o.attach.bind fun x =>
      match x with
      | ⟨x, h⟩ =>
        Option.map
          (fun x_1 =>
            match x_1 with
            | ⟨y, h'⟩ => ⟨y, ⋯⟩)
          (f x).attach

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_eq_getKeyD [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a fallback : α} {h} :
    m.getKey a h = m.getKeyD a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h✝ : m.val.WF
a fallback : α
h : m.contains a = true
⊢ m.getKey a h = m.getKeyD a fallback

Tactic:
simp_to_model using List.getKey_eq_getKeyD

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_eq_zero : μ.restrict s = 0 ↔ μ s = 0

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ.restrict s = 0 ↔ μ s = 0

Tactic:
rw [← measure_univ_eq_zero, restrict_apply_univ]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem tan_add_mul_I {x y : ℂ}
    (h :
      ((∀ k : ℤ, x ≠ (2 * k + 1) * π / 2) ∧ ∀ l : ℤ, y * I ≠ (2 * l + 1) * π / 2) ∨
        (∃ k : ℤ, x = (2 * k + 1) * π / 2) ∧ ∃ l : ℤ, y * I = (2 * l + 1) * π / 2) :
    tan (x + y * I) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)

Proof state:
x y : ℂ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y * I ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, y * I = (2 * ↑l + 1) * ↑π / 2
⊢ tan (x + y * I) = (tan x + tanh y * I) / (1 - tan x * tanh y * I)

Tactic:
rw [tan_add h, tan_mul_I, mul_assoc]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) :
    c • f x = f (σ' c • x)

Proof state:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
F : Type u_14
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module S M₃
σ : R →+* S
f : F
inst✝² : FunLike F M M₃
inst✝¹ : SemilinearMapClass F σ M M₃
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
c : S
x : M
⊢ c • f x = f (σ' c • x)

Tactic:
simp [map_smulₛₗ _]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem ker_eq_bot_of_inverse {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂}
    {g : M₂ →ₛₗ[τ₂₁] M} (h : (g.comp f : M →ₗ[R] M) = id) : ker f = ⊥ :=
  ker_eq_bot'.2 fun m hm => by rw [← id_apply (R := R) m, ← h, comp_apply, hm, g.map_zero]

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝ : RingHomInvPair τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₁] M
h : g.comp f = id
m : M
hm : f m = 0
⊢ m = 0

Tactic:
rw [← id_apply (R := R) m, ← h, comp_apply, hm, g.map_zero]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Root.lean
@[simp] lemma ceilRoot_zero_right (n : ℕ) : ceilRoot n 0 = 0

Proof state:
n : ℕ
⊢ n.ceilRoot 0 = 0

Tactic:
simp [ceilRoot]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
theorem units_involute_act_eq_conjAct {x : (CliffordAlgebra Q)ˣ} (hx : ↑x ∈ spinGroup Q) (y : M) :
    involute (Q := Q) ↑x * ι Q y * ↑x⁻¹ = ConjAct.toConjAct x • (ι Q y)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
hx : ↑x ∈ spinGroup Q
y : M
⊢ involute ↑x * (ι Q) y * ↑x⁻¹ = ConjAct.toConjAct x • (ι Q) y

Tactic:
rw [involute_eq hx, @ConjAct.units_smul_def, @ConjAct.ofConjAct_toConjAct]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem id : Nat.Primrec id :=
  (left.pair right).of_eq fun n => by simp

Proof state:
n : ℕ
⊢ Nat.pair (unpair n).1 (unpair n).2 = id n

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma IsDiameter.pointReflection_center_left (h : s.IsDiameter p₁ p₂) :
    Equiv.pointReflection s.center p₁ = p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ (Equiv.pointReflection s.center) p₁ = p₂

Tactic:
rw [← h.midpoint_eq_center, Equiv.pointReflection_midpoint_left]

Result:
no goals
-- Mathlib/Data/Nat/Cast/SetInterval.lean
theorem image_cast_int_Ioi (a : ℕ) : (↑) '' Ioi a = Ioi (a : ℤ) :=
  (castOrderEmbedding (α := ℤ)).image_Ioi (by simp [isUpperSet_Ici]) a

Proof state:
a : ℕ
⊢ IsUpperSet (range ⇑castOrderEmbedding)

Tactic:
simp [isUpperSet_Ici]

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem eval_curry (c n x) : eval (curry c n) x = eval c (Nat.pair n x)

Proof state:
c : Code
n x : ℕ
⊢ (c.curry n).eval x = c.eval (Nat.pair n x)

Tactic:
simp! [Seq.seq, curry]

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem IsSeparableContraction.natSepDegree_eq {g : Polynomial F} {q : ℕ} [ExpChar F q]
    (h : IsSeparableContraction q f g) : f.natSepDegree = g.natDegree

Proof state:
F : Type u
inst✝¹ : Field F
f g : F[X]
q : ℕ
inst✝ : ExpChar F q
h : IsSeparableContraction q f g
⊢ f.natSepDegree = g.natDegree

Tactic:
obtain ⟨h1, m, h2⟩ := h

Result:
case intro.intro
F : Type u
inst✝¹ : Field F
f g : F[X]
q : ℕ
inst✝ : ExpChar F q
h1 : g.Separable
m : ℕ
h2 : (expand F (q ^ m)) g = f
⊢ f.natSepDegree = g.natDegree

Proof state:
case intro.intro
F : Type u
inst✝¹ : Field F
f g : F[X]
q : ℕ
inst✝ : ExpChar F q
h1 : g.Separable
m : ℕ
h2 : (expand F (q ^ m)) g = f
⊢ f.natSepDegree = g.natDegree

Tactic:
rw [← h2, natSepDegree_expand, h1.natSepDegree_eq_natDegree]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean
@[reassoc (attr := simp)]
lemma toFreeYonedaCoproduct_fromFreeYonedaCoproduct :
    M.toFreeYonedaCoproduct ≫ M.fromFreeYonedaCoproduct = 0

Proof state:
C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
⊢ M.toFreeYonedaCoproduct ≫ M.fromFreeYonedaCoproduct = 0

Tactic:
simp [toFreeYonedaCoproduct]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_zero : Gamma 0 = 0

Proof state:
⊢ Gamma 0 = 0

Tactic:
simp_rw [Gamma, zero_re, sub_zero, Nat.floor_one, GammaAux, div_zero]

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem head_mk (x : F (M F)) : head (M.mk x) = x.1 :=
  Eq.symm <|
    calc
      x.1 = (dest (M.mk x)).1

Proof state:
F : PFunctor.{u}
x : ↑F F.M
⊢ x.fst = (M.mk x).dest.fst

Tactic:
rw [dest_mk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
    k ∈ m.insert k v

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
v : β k
⊢ k ∈ m.insert k v

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem or_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a ∨ b) = b

Proof state:
a b : Prop
h : a = False
⊢ (a ∨ b) = b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem cons_zero : cons x p 0 = x

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
⊢ cons x p 0 = x

Tactic:
simp [cons]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem mul_coe_eq_smul : a * r = r • a

Proof state:
R : Type u_3
c₁ c₂ c₃ r : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a * ↑r = r • a

Tactic:
rw [← coe_commutes, coe_mul_eq_smul]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PartitionOfUnity.lean
theorem exists_continuous_real_forall_closedBall_subset (hK : ∀ i, IsClosed (K i))
    (hU : ∀ i, IsOpen (U i)) (hKU : ∀ i, K i ⊆ U i) (hfin : LocallyFinite K) :
    ∃ δ : C(X, ℝ), (∀ x, 0 < δ x) ∧
      ∀ (i), ∀ x ∈ K i, closedBall x (ENNReal.ofReal <| δ x) ⊆ U i

Proof state:
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, closedBall x (ENNReal.ofReal (δ x)) ⊆ U i

Tactic:
simpa only [mem_inter_iff, forall_and, mem_preimage, mem_iInter, @forall_swap ι X] using
  exists_continuous_forall_mem_convex_of_local_const exists_forall_closedBall_subset_aux₂
    (exists_forall_closedBall_subset_aux₁ hK hU hKU hfin)

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean
@[simp]
lemma dynEntourage_zero {T : X → X} {U : Set (X × X)} :
    dynEntourage T U 0 = univ

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
⊢ dynEntourage T U 0 = univ

Tactic:
simp [dynEntourage]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Norm.lean
theorem extends_norm' (f : MulAlgebraNorm R S) (a : R) : f (a • (1 : S)) = ‖a‖

Proof state:
R : outParam (Type u_1)
S : outParam (Type u_2)
inst✝² : SeminormedCommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
f : MulAlgebraNorm R S
a : R
⊢ f (a • 1) = ‖a‖

Tactic:
rw [← mul_one ‖a‖, ← f.map_one', ← f.smul', toFun_eq_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem cond_true (discr : Bool) (lhs rhs : BitVec w) :
    (!discr || ((bif discr then lhs else rhs) == lhs)) = true

Proof state:
w : Nat
discr : Bool
lhs rhs : BitVec w
⊢ (!discr || (bif discr then lhs else rhs) == lhs) = true

Tactic:
cases discr <;> simp

Result:
no goals
-- Mathlib/Data/Multiset/Interval.lean
theorem card_uIcc :
    (uIcc s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, ((t.count i - s.count i : ℤ).natAbs + 1)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(uIcc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, ((↑(count i t) - ↑(count i s)).natAbs + 1)

Tactic:
simp_rw [uIcc_eq, Finset.card_map, DFinsupp.card_uIcc, Nat.card_uIcc, Multiset.toDFinsupp_apply,
  toDFinsupp_support]

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropWithinAt_indep_chart_aux (he : e ∈ G.maximalAtlas M) (xe : x ∈ e.source)
    (he' : e' ∈ G.maximalAtlas M) (xe' : x ∈ e'.source) (hf : f ∈ G'.maximalAtlas M')
    (xf : g x ∈ f.source) (hf' : f' ∈ G'.maximalAtlas M') (xf' : g x ∈ f'.source)
    (hgs : ContinuousWithinAt g s x) :
    P (f ∘ g ∘ e.symm) (e.symm ⁻¹' s) (e x) ↔ P (f' ∘ g ∘ e'.symm) (e'.symm ⁻¹' s) (e' x)

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
e e' : PartialHomeomorph M H
f f' : PartialHomeomorph M' H'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
x : M
hG : G.LocalInvariantProp G' P
he : e ∈ maximalAtlas M G
xe : x ∈ e.source
he' : e' ∈ maximalAtlas M G
xe' : x ∈ e'.source
hf : f ∈ maximalAtlas M' G'
xf : g x ∈ f.source
hf' : f' ∈ maximalAtlas M' G'
xf' : g x ∈ f'.source
hgs : ContinuousWithinAt g s x
⊢ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (↑f' ∘ g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)

Tactic:
rw [← Function.comp_assoc, hG.liftPropWithinAt_indep_chart_source_aux (f ∘ g) he xe he' xe',
  Function.comp_assoc, hG.liftPropWithinAt_indep_chart_target_aux xe' hf xf hf' xf' hgs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_eq_some_get! [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] :
    m.contains a = true → m.get? a = some (m.get! a)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
a : α
inst✝ : Inhabited (β a)
⊢ m.contains a = true → m.get? a = some (m.get! a)

Tactic:
simp_to_model using List.getValueCast?_eq_some_getValueCast!

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
@[simp]
lemma symmetric_apply_eq_iff {α : Sort*} {f : α → α} : Symmetric (f · = ·) ↔ Involutive f

Proof state:
α : Sort u_1
f : α → α
⊢ (Symmetric fun x1 x2 => f x1 = x2) ↔ Involutive f

Tactic:
simp [Symmetric, Involutive]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Opposites.lean
theorem leadingCoeff_opRingEquiv (p : R[X]ᵐᵒᵖ) :
    (opRingEquiv R p).leadingCoeff = op (unop p).leadingCoeff

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
⊢ ((opRingEquiv R) p).leadingCoeff = op (unop p).leadingCoeff

Tactic:
rw [leadingCoeff, coeff_opRingEquiv, natDegree_opRingEquiv, leadingCoeff]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Basic.lean
theorem tsub_eq_zero_iff_le : a - b = 0 ↔ a ≤ b

Proof state:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a - b = 0 ↔ a ≤ b

Tactic:
rw [← nonpos_iff_eq_zero, tsub_le_iff_left, add_zero]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive (attr := simp) enorm_neg]
lemma enorm_inv' (a : E) : ‖a⁻¹‖ₑ = ‖a‖ₑ

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ ‖a⁻¹‖ₑ = ‖a‖ₑ

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Representable.lean
/-- In the case of a representable morphism `f' : F.obj Y ⟶ G`, whose codomain lies
in the image of `F`, we get that two morphism `a b : Z ⟶ hf.pullback g` are equal if
* Their compositions (in `C`) with `hf'.snd g : hf.pullback  ⟶ X` are equal.
* Their compositions (in `C`) with `hf'.fst' g : hf.pullback  ⟶ Y` are equal. -/
@[ext]
lemma hom_ext' [Full F] [Faithful F] {c : C} {a b : c ⟶ hf'.pullback g}
    (h₁ : a ≫ hf'.fst' g = b ≫ hf'.fst' g)
    (h₂ : a ≫ hf'.snd g = b ≫ hf'.snd g) : a = b :=
  hf'.hom_ext (by simpa [map_fst'] using F.congr_map h₁) h₂

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b✝ : C
f' : F.obj b✝ ⟶ Y
hf' : F.relativelyRepresentable f'
a✝ : C
g : F.obj a✝ ⟶ Y
inst✝¹ : F.Full
inst✝ : F.Faithful
c : C
a b : c ⟶ hf'.pullback g
h₁ : a ≫ hf'.fst' g = b ≫ hf'.fst' g
h₂ : a ≫ hf'.snd g = b ≫ hf'.snd g
⊢ F.map a ≫ hf'.fst g = F.map b ≫ hf'.fst g

Tactic:
simpa [map_fst'] using F.congr_map h₁

Result:
no goals
-- Mathlib/Data/Multiset/Lattice.lean
theorem le_inf {s : Multiset α} {a : α} : a ≤ s.inf ↔ ∀ b ∈ s, a ≤ b :=
  Multiset.induction_on s (by simp)
    (by simp +contextual [or_imp, forall_and])

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s : Multiset α
a : α
⊢ ∀ (a_1 : α) (s : Multiset α), (a ≤ s.inf ↔ ∀ b ∈ s, a ≤ b) → (a ≤ (a_1 ::ₘ s).inf ↔ ∀ b ∈ a_1 ::ₘ s, a ≤ b)

Tactic:
simp +contextual [or_imp, forall_and]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s : Multiset α
a : α
⊢ a ≤ inf 0 ↔ ∀ b ∈ 0, a ≤ b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem isCauSeq_re (f : CauSeq ℂ (‖·‖)) : IsCauSeq abs fun n ↦ (f n).re := fun _ ε0 ↦
  (f.cauchy ε0).imp fun i H j ij ↦
    lt_of_le_of_lt (by simpa using abs_re_le_norm (f j - f i)) (H _ ij)

Proof state:
f : CauSeq ℂ fun x => ‖x‖
x✝ : ℝ
ε0 : x✝ > 0
i : ℕ
H : ∀ j ≥ i, ‖↑f j - ↑f i‖ < x✝
j : ℕ
ij : j ≥ i
⊢ |(fun n => (↑f n).re) j - (fun n => (↑f n).re) i| ≤ ‖↑f j - ↑f i‖

Tactic:
simpa using abs_re_le_norm (f j - f i)

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem compl_iSup₂ (f : ∀ i, κ i → UpperSet α) :
    (⨆ (i) (j), f i j).compl = ⨆ (i) (j), (f i j).compl

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
f : (i : ι) → κ i → UpperSet α
⊢ (⨆ i, ⨆ j, f i j).compl = ⨆ i, ⨆ j, (f i j).compl

Tactic:
simp_rw [UpperSet.compl_iSup]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_ne_zero : s.encard ≠ 0 ↔ s.Nonempty

Proof state:
α : Type u_1
s : Set α
⊢ s.encard ≠ 0 ↔ s.Nonempty

Tactic:
rw [ne_eq, encard_eq_zero, nonempty_iff_ne_empty]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpIndL1_of_not_measurableSet (hs : ¬MeasurableSet s) (x : G) :
    condExpIndL1 hm μ s x = 0

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : ¬MeasurableSet s
x : G
⊢ condExpIndL1 hm μ s x = 0

Tactic:
simp only [condExpIndL1, hs, dif_neg, not_false_iff, false_and]

Result:
no goals
-- Mathlib/Order/Bounded.lean
theorem unbounded_le_iff [LinearOrder α] : Unbounded (· ≤ ·) s ↔ ∀ a, ∃ b ∈ s, a < b

Proof state:
α : Type u_1
s : Set α
inst✝ : LinearOrder α
⊢ Unbounded (fun x1 x2 => x1 ≤ x2) s ↔ ∀ (a : α), ∃ b ∈ s, a < b

Tactic:
simp only [Unbounded, not_le]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Basic.lean
theorem LinearMap.id_moduleCat_comp
    {R} [Ring R] {G : Type u} [AddCommGroup G] [Module R G] {H : ModuleCat.{u} R} (f : G →ₗ[R] H) :
    LinearMap.comp (𝟙 H : H ⟶ H).hom f = f

Proof state:
R : Type u_1
inst✝² : Ring R
G : Type u
inst✝¹ : AddCommGroup G
inst✝ : Module R G
H : ModuleCat R
f : G →ₗ[R] ↑H
⊢ Hom.hom (𝟙 H) ∘ₗ f = f

Tactic:
simp

Result:
no goals