harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/ByCases.lean
theorem apply_dite (f : α → β) (P : Prop) [Decidable P] (x : P → α) (y : ¬P → α) :
    f (dite P x y) = dite P (fun h => f (x h)) (fun h => f (y h))

Proof state:
α : Sort u_1
β : Sort u_2
f : α → β
P : Prop
inst✝ : Decidable P
x : P → α
y : ¬P → α
⊢ f (dite P x y) = if h : P then f (x h) else f (y h)

Tactic:
by_cases h : P <;> simp [h]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem mem_ite_empty_left (p : Prop) [Decidable p] (t : Set α) (x : α) :
    x ∈ ite p ∅ t ↔ ¬p ∧ x ∈ t :=
  (mem_dite_empty_left p (fun _ => t) x).trans (by simp)

Proof state:
α : Type u
p : Prop
inst✝ : Decidable p
t : Set α
x : α
⊢ (∃ (_ : ¬p), x ∈ t) ↔ ¬p ∧ x ∈ t

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem embDomainRingHom_C [NonAssocSemiring R] {f : Γ →+ Γ'} {hfi : Function.Injective f}
    {hf : ∀ g g' : Γ, f g ≤ f g' ↔ g ≤ g'} {r : R} : embDomainRingHom f hfi hf (C r) = C r :=
  embDomain_single.trans (by simp)

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : OrderedCancelAddCommMonoid Γ
Γ' : Type u_6
inst✝¹ : OrderedCancelAddCommMonoid Γ'
inst✝ : NonAssocSemiring R
f : Γ →+ Γ'
hfi : Injective ⇑f
hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g'
r : R
⊢ (single ({ toFun := ⇑f, inj' := hfi, map_rel_iff' := ⋯ } 0)) r = C r

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/LiftingProperties/Basic.lean
theorem op (h : HasLiftingProperty i p) : HasLiftingProperty p.op i.op :=
  ⟨fun {f} {g} sq => by
    simp only [CommSq.HasLift.iff_unop, Quiver.Hom.unop_op]
    infer_instance⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.op Y ⟶ Opposite.op B
g : Opposite.op X ⟶ Opposite.op A
sq : CommSq f p.op i.op g
⊢ ⋯.HasLift

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.op Y ⟶ Opposite.op B
g : Opposite.op X ⟶ Opposite.op A
sq : CommSq f p.op i.op g
⊢ sq.HasLift

Tactic:
simp only [CommSq.HasLift.iff_unop, Quiver.Hom.unop_op]

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.op Y ⟶ Opposite.op B
g : Opposite.op X ⟶ Opposite.op A
sq : CommSq f p.op i.op g
⊢ ⋯.HasLift
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal'_one [∀ i, DecidableEq (m' i)] [One α] :
    blockDiagonal' (1 : ∀ i, Matrix (m' i) (m' i) α) = 1 :=
  show (blockDiagonal' fun i : o => diagonal fun _ : m' i => (1 : α)) = diagonal fun _ => 1 by
    rw [blockDiagonal'_diagonal]

Proof state:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : (i : o) → DecidableEq (m' i)
inst✝ : One α
⊢ (blockDiagonal' fun i => diagonal fun x => 1) = diagonal fun x => 1

Tactic:
rw [blockDiagonal'_diagonal]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem mul_omega0_dvd (a0 : 0 < a) (ha : a < ω) : ∀ {b}, ω ∣ b → a * b = b
  | _, ⟨b, rfl⟩ => by rw [← mul_assoc, mul_omega0 a0 ha]

Proof state:
a : Ordinal.{u}
a0 : 0 < a
ha : a < ω
b : Ordinal.{u}
⊢ a * (ω * b) = ω * b

Tactic:
rw [← mul_assoc, mul_omega0 a0 ha]

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma CorepresentableBy.homEquiv_eq {F : C ⥤ Type v} {X : C} (e : F.CorepresentableBy X)
    {Y : C} (f : X ⟶ Y) :
    e.homEquiv f = F.map f (e.homEquiv (𝟙 X))

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : F.CorepresentableBy X
Y : C
f : X ⟶ Y
⊢ e.homEquiv f = F.map f (e.homEquiv (𝟙 X))

Tactic:
conv_lhs => rw [← Category.id_comp f, e.homEquiv_comp]

Result:
no goals
-- Mathlib/Dynamics/FixedPoints/Basic.lean
theorem Commute.right_bijOn_fixedPoints_comp (h : Commute f g) :
    Set.BijOn g (fixedPoints <| f ∘ g) (fixedPoints <| f ∘ g)

Proof state:
α : Type u
f g : α → α
h : Function.Commute f g
⊢ Set.BijOn g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
simpa only [h.comp_eq] using bijOn_fixedPoints_comp f g

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
lemma integral_add_const (f : X →ᵇ ℝ) (c : ℝ) :
    ∫ x, (f + const X c) x ∂μ = ∫ x, f x ∂μ + ENNReal.toReal (μ (Set.univ)) • c

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
inst✝¹ : OpensMeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ
c : ℝ
⊢ ∫ (x : X), (f + const X c) x ∂μ = ∫ (x : X), f x ∂μ + (μ Set.univ).toReal • c

Tactic:
simp [integral_add (f.integrable _) (integrable_const c)]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem IsOpen.inter_frontier_eq (hs : IsOpen s) : s ∩ frontier s = ∅

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
hs : IsOpen s
⊢ s ∩ frontier s = ∅

Tactic:
rw [hs.frontier_eq, inter_diff_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftLeft_eq_concat_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
    x <<< n = (x.extractLsb' 0 (w - n) ++ 0#n).cast (by omega)

Proof state:
case neg
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
hi' : ¬i < n
⊢ x.getLsbD (i - n) = true → i - n < w - n

Tactic:
omega

Result:
no goals

Proof state:
case pos
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
hi' : i < n
⊢ (!decide (i < n) && x.getLsbD (i - n)) = (!decide (i < n) && (decide (i - n < w - n) && x.getLsbD (i - n)))

Tactic:
simp [hi']

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
⊢ (x <<< n).getLsbD i = (BitVec.cast ⋯ (extractLsb' 0 (w - n) x ++ 0#n)).getLsbD i

Tactic:
simp only [getLsbD_shiftLeft, hi, decide_true, Bool.true_and, getLsbD_cast, getLsbD_append,
  getLsbD_zero, getLsbD_extractLsb', Nat.zero_add, Bool.if_false_left]

Result:
case pred
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
⊢ (!decide (i < n) && x.getLsbD (i - n)) = (!decide (i < n) && (decide (i - n < w - n) && x.getLsbD (i - n)))

Proof state:
case pred
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
⊢ (!decide (i < n) && x.getLsbD (i - n)) = (!decide (i < n) && (decide (i - n < w - n) && x.getLsbD (i - n)))

Tactic:
by_cases hi' : i < n

Result:
case pos
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
hi' : i < n
⊢ (!decide (i < n) && x.getLsbD (i - n)) = (!decide (i < n) && (decide (i - n < w - n) && x.getLsbD (i - n)))

case neg
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
hi' : ¬i < n
⊢ (!decide (i < n) && x.getLsbD (i - n)) = (!decide (i < n) && (decide (i - n < w - n) && x.getLsbD (i - n)))

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : n < w
⊢ w - n + n = w

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : n < w
⊢ x <<< n = BitVec.cast ⋯ (extractLsb' 0 (w - n) x ++ 0#n)

Tactic:
ext i hi

Result:
case pred
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
⊢ (x <<< n).getLsbD i = (BitVec.cast ⋯ (extractLsb' 0 (w - n) x ++ 0#n)).getLsbD i

Proof state:
case neg
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
hi' : ¬i < n
⊢ (!decide (i < n) && x.getLsbD (i - n)) = (!decide (i < n) && (decide (i - n < w - n) && x.getLsbD (i - n)))

Tactic:
simp [hi']

Result:
case neg
w : Nat
x : BitVec w
n : Nat
hn : n < w
i : Nat
hi : i < w
hi' : ¬i < n
⊢ x.getLsbD (i - n) = true → i - n < w - n
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
lemma smul_coe (m : R) (g : SpecialLinearGroup n R) (A : FixedDetMatrix n R m) :
    (g • A).1 = g * A.1

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
g : SpecialLinearGroup n R
A : FixedDetMatrix n R m
⊢ ↑(g • A) = ↑g * ↑A

Tactic:
rw [smul_def]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem prod_iUnion {s : Set α} {t : ι → Set β} : (s ×ˢ ⋃ i, t i) = ⋃ i, s ×ˢ t i

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
⊢ s ×ˢ ⋃ i, t i = ⋃ i, s ×ˢ t i

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
x✝ : α × β
⊢ x✝ ∈ s ×ˢ ⋃ i, t i ↔ x✝ ∈ ⋃ i, s ×ˢ t i

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
s : Set α
t : ι → Set β
x✝ : α × β
⊢ x✝ ∈ s ×ˢ ⋃ i, t i ↔ x✝ ∈ ⋃ i, s ×ˢ t i

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblU_eq (P : Fin 3 → R) : W'.dblU P =
    W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ W'.dblU P = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)

Tactic:
rw [dblU, eval_polynomialX]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma ringEquivCongr_symm {a b : ℕ} (hab : a = b) :
    (ringEquivCongr hab).symm = ringEquivCongr hab.symm

Proof state:
a b : ℕ
hab : a = b
⊢ (ringEquivCongr hab).symm = ringEquivCongr ⋯

Tactic:
subst hab

Result:
a : ℕ
⊢ (ringEquivCongr ⋯).symm = ringEquivCongr ⋯

Proof state:
a : ℕ
⊢ (ringEquivCongr ⋯).symm = ringEquivCongr ⋯

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem coe_sum' {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) :
    ⇑(∑ d ∈ t, f d) = ∑ d ∈ t, ⇑(f d)

Proof state:
R₁ : Type u_1
R₂ : Type u_2
inst✝⁸ : Semiring R₁
inst✝⁷ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : ContinuousAdd M₂
ι : Type u_9
t : Finset ι
f : ι → M₁ →SL[σ₁₂] M₂
⊢ ⇑(∑ d ∈ t, f d) = ∑ d ∈ t, ⇑(f d)

Tactic:
simp only [← coe_coe, coe_sum, LinearMap.coeFn_sum]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem map (hφ : IsSymmetric φ) (f : R →+* S) : IsSymmetric (map f φ) := fun e => by
  rw [← map_rename, hφ]

Proof state:
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
f : R →+* S
e : Perm σ
⊢ (rename ⇑e) ((MvPolynomial.map f) φ) = (MvPolynomial.map f) φ

Tactic:
rw [← map_rename, hφ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem empty_eq_append_iff : #[] = a ++ b ↔ a = #[] ∧ b = #[]

Proof state:
α✝ : Type u_1
a b : Array α✝
⊢ #[] = a ++ b ↔ a = #[] ∧ b = #[]

Tactic:
rw [eq_comm, append_eq_empty_iff]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem isUnit_coe : IsUnit (s : Set α) ↔ IsUnit s

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit ↑s ↔ IsUnit s

Tactic:
simp_rw [isUnit_iff, Set.isUnit_iff, coe_eq_singleton]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem PredOrder.nhdsGE_eq_nhds [PredOrder α] (a : α) : 𝓝[≥] a = 𝓝 a

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : PredOrder α
a : α
⊢ 𝓝[≥] a = 𝓝 a

Tactic:
rw [← nhdsLT_sup_nhdsGE, PredOrder.nhdsLT, bot_sup_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_ge_of_const_le {c : ℝ} (hs : MeasurableSet s) (hμs : μ s ≠ ∞)
    (hf : ∀ x ∈ s, c ≤ f x) (hfint : IntegrableOn (fun x : X => f x) s μ) :
    c * (μ s).toReal ≤ ∫ x in s, f x ∂μ

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
c : ℝ
hs : MeasurableSet s
hμs : μ s ≠ ⊤
hf : ∀ x ∈ s, c ≤ f x
hfint : IntegrableOn (fun x => f x) s μ
⊢ ∫ (x : X) in s, c ∂μ ≤ ∫ (x : X) in s, f x ∂μ

Tactic:
exact setIntegral_mono_on (integrableOn_const.2 (Or.inr hμs.lt_top)) hfint hs hf

Result:
no goals

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
c : ℝ
hs : MeasurableSet s
hμs : μ s ≠ ⊤
hf : ∀ x ∈ s, c ≤ f x
hfint : IntegrableOn (fun x => f x) s μ
⊢ c * (μ s).toReal ≤ ∫ (x : X) in s, f x ∂μ

Tactic:
rw [mul_comm, ← smul_eq_mul, ← setIntegral_const c]

Result:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
c : ℝ
hs : MeasurableSet s
hμs : μ s ≠ ⊤
hf : ∀ x ∈ s, c ≤ f x
hfint : IntegrableOn (fun x => f x) s μ
⊢ ∫ (x : X) in s, c ∂μ ≤ ∫ (x : X) in s, f x ∂μ
-- Mathlib/CategoryTheory/Shift/Basic.lean
@[simp]
lemma map_zero_inv_app (X : C) :
    F.map ((zero hF s i).inv.app X) =
      (shiftFunctorZero D A).inv.app (F.obj X) ≫ (i 0).inv.app X

Proof state:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
X : C
⊢ F.map ((zero hF s i).inv.app X) = (shiftFunctorZero D A).inv.app (F.obj X) ≫ (i 0).inv.app X

Tactic:
simp [zero]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem mk_zero [∀ i, Zero (β i)] {s : Finset ι} : mk s (0 : ∀ i : (↑s : Set ι), β i.1) = 0 :=
  ext fun i => by simp only [mk_apply]; split_ifs <;> rfl

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
i : ι
⊢ (mk s 0) i = 0 i

Tactic:
simp only [mk_apply]

Result:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
i : ι
⊢ (if H : i ∈ s then 0 ⟨i, H⟩ else 0) = 0 i

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
s : Finset ι
i : ι
⊢ (if H : i ∈ s then 0 ⟨i, H⟩ else 0) = 0 i

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem reverse_suffix : reverse l₁ <:+ reverse l₂ ↔ l₁ <+: l₂ :=
  ⟨fun ⟨r, e⟩ => ⟨reverse r, by rw [← reverse_reverse l₁, ← reverse_append, e, reverse_reverse]⟩,
   fun ⟨r, e⟩ => ⟨reverse r, by rw [← reverse_append, e]⟩⟩

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
x✝ : l₁.reverse <:+ l₂.reverse
r : List α✝
e : r ++ l₁.reverse = l₂.reverse
⊢ l₁ ++ r.reverse = l₂

Tactic:
rw [← reverse_reverse l₁, ← reverse_append, e, reverse_reverse]

Result:
no goals

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
x✝ : l₁ <+: l₂
r : List α✝
e : l₁ ++ r = l₂
⊢ r.reverse ++ l₁.reverse = l₂.reverse

Tactic:
rw [← reverse_append, e]

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem computable_iff_re_compl_re' {p : α → Prop} :
    ComputablePred p ↔ REPred p ∧ REPred fun a => ¬p a

Proof state:
α : Type u_1
inst✝ : Primcodable α
p : α → Prop
⊢ ComputablePred p ↔ REPred p ∧ REPred fun a => ¬p a

Tactic:
classical exact computable_iff_re_compl_re

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Primcodable α
p : α → Prop
⊢ ComputablePred p ↔ REPred p ∧ REPred fun a => ¬p a

Tactic:
exact computable_iff_re_compl_re

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_alter_self [LawfulBEq α] {k : α} [Inhabited (β k)] {f : Option (β k) → Option (β k)}
    (h : m.WF) : (m.alter k f).get! k = (f (m.get? k)).get!

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
k : α
inst✝ : Inhabited (β k)
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).get! k = (f (m.get? k)).get!

Tactic:
simp [get!_alter h, Option.map_cast_apply]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[bound]
lemma inv_mul_le_one_of_le₀ (h : a ≤ b) (hb : 0 ≤ b) : b⁻¹ * a ≤ 1 :=
  inv_mul_le_of_le_mul₀ hb zero_le_one <| by rwa [mul_one]

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulMono G₀
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ b * 1

Tactic:
rwa [mul_one]

Result:
no goals
-- Mathlib/Computability/PostTuringMachine.lean
theorem trTape_mk' (L R : ListBlank Γ) : trTape enc0 (Tape.mk' L R) = trTape' enc0 L R

Proof state:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = Vector.replicate n false
L R : ListBlank Γ
⊢ trTape enc0 (Tape.mk' L R) = trTape' enc0 L R

Tactic:
simp only [trTape, Tape.mk'_left, Tape.mk'_right₀]

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem neg_mul_comm (a b : α) : -a * b = a * -b

Proof state:
α : Type u
inst✝¹ : Mul α
inst✝ : HasDistribNeg α
a b : α
⊢ -a * b = a * -b

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Partition/Finpartition.lean
lemma exists_enumeration : ∃ f : s ≃ Σ t : P.parts, Fin #t.1,
    ∀ a b : s, P.part a = P.part b ↔ (f a).1 = (f b).1

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∀ (a b : { x // x ∈ s }),
    P.part ↑a = P.part ↑b ↔
      ((P.equivSigmaParts.trans ((Equiv.refl { x // x ∈ P.parts }).sigmaCongr fun t => (↑t).equivFin)) a).fst =
        ((P.equivSigmaParts.trans ((Equiv.refl { x // x ∈ P.parts }).sigmaCongr fun t => (↑t).equivFin)) b).fst

Tactic:
simp [equivSigmaParts, Equiv.sigmaCongr, Equiv.sigmaCongrLeft]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst

Tactic:
use P.equivSigmaParts.trans ((Equiv.refl _).sigmaCongr (fun t ↦ t.1.equivFin))

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ ∀ (a b : { x // x ∈ s }),
    P.part ↑a = P.part ↑b ↔
      ((P.equivSigmaParts.trans ((Equiv.refl { x // x ∈ P.parts }).sigmaCongr fun t => (↑t).equivFin)) a).fst =
        ((P.equivSigmaParts.trans ((Equiv.refl { x // x ∈ P.parts }).sigmaCongr fun t => (↑t).equivFin)) b).fst
-- Mathlib/Algebra/Ring/Basic.lean
lemma inv_neg_one : (-1 : R)⁻¹ = -1

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
⊢ (-1)⁻¹ = -1

Tactic:
rw [← neg_inv, inv_one]

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
lemma div_apply' (ψ χ : AddChar A M) (a : A) : (ψ / χ) a = ψ a / χ a

Proof state:
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ χ : AddChar A M
a : A
⊢ (ψ / χ) a = ψ a / χ a

Tactic:
rw [div_apply, map_neg_eq_inv, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem pmap_cons' {p : α → Prop} (f : (a : α) → p a → β) (a : α) (v : Vector α n)
    (ha : p a) (hp : ∀ x ∈ v.toList, p x) :
    cons (f a ha) (v.pmap f hp) = (cons a v).pmap f (by simpa [ha]) := rfl

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
a : α
v : Vector α n
ha : p a
hp : ∀ x ∈ v.toList, p x
⊢ ∀ x ∈ (a ::ᵥ v).toList, p x

Tactic:
simpa [ha]

Result:
no goals
-- Mathlib/Tactic/NormNum/DivMod.lean
lemma isNat_neg_of_isNegNat {a : ℤ} {b : ℕ} (h : IsInt a (.negOfNat b)) : IsNat (-a) b :=
  ⟨by simp [h.out]⟩

Proof state:
a : ℤ
b : ℕ
h : IsInt a (Int.negOfNat b)
⊢ -a = ↑b

Tactic:
simp [h.out]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem one_lt_two : (1 : Cardinal) < 2

Proof state:
⊢ 1 < 2

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Analysis/Complex/TaylorSeries.lean
/-- A function that is complex differentiable on the open ball of radius `r ≤ ∞` around `c`
is given by evaluating its Taylor series at `c` on this open ball. -/
lemma taylorSeries_eq_on_emetric_ball' {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (EMetric.ball c r)) :
    ∑' n : ℕ, (n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Proof state:
c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ EMetric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (EMetric.ball c r)
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Tactic:
convert taylorSeries_eq_on_emetric_ball hf hz using 3 with n

Result:
case h.e'_2.h.e'_5.h
c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ EMetric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (EMetric.ball c r)
n : ℕ
⊢ (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c

Proof state:
case h.e'_2.h.e'_5.h
c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ EMetric.ball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (EMetric.ball c r)
n : ℕ
⊢ (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c

Tactic:
rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem lc_coeffs (m : M) : DualBases.lc e (h.coeffs m) = m

Proof state:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
m : M
i : ι
⊢ (ε i) (lc e (h.coeffs m) - m) = 0

Tactic:
simp [LinearMap.map_sub, h.dual_lc, sub_eq_zero]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
m : M
⊢ lc e (h.coeffs m) = m

Tactic:
refine eq_of_sub_eq_zero <| h.total fun i ↦ ?_

Result:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
m : M
i : ι
⊢ (ε i) (lc e (h.coeffs m) - m) = 0
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem gradient_const : ∇ (fun _ => c) x = 0

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

Tactic:
rw [gradient, fderiv_const, Pi.zero_apply, map_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List ((a : α) × β a)} {k : α} :
    k ∈ (m.insertMany l) ↔ k ∈ m ∨ (l.map Sigma.fst).contains k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List ((a : α) × β a)
k : α
⊢ k ∈ m.insertMany l ↔ k ∈ m ∨ (List.map Sigma.fst l).contains k = true

Tactic:
simp [mem_iff_contains, contains_insertMany_list h]

Result:
no goals
-- Mathlib/Order/Cover.lean
lemma transGen_wcovBy_eq_reflTransGen_covBy [PartialOrder α] :
    TransGen ((· : α) ⩿ ·) = ReflTransGen (· ⋖ ·)

Proof state:
α : Type u_1
inst✝ : PartialOrder α
⊢ (TransGen fun x1 x2 => x1 ⩿ x2) = ReflTransGen fun x1 x2 => x1 ⋖ x2

Tactic:
rw [wcovBy_eq_reflGen_covBy, transGen_reflGen]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem generateFrom_singleton_univ : generateFrom {Set.univ} = (⊥ : MeasurableSpace α) :=
  bot_unique <| generateFrom_le <| by simp

Proof state:
α : Type u_1
⊢ ∀ t ∈ {univ}, MeasurableSet t

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem lt_total (f g : CauSeq α abs) : f < g ∨ f ≈ g ∨ g < f :=
  (trichotomy (g - f)).imp_right fun h =>
    h.imp (fun h => Setoid.symm h) fun h => by rwa [neg_sub] at h

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
h✝ : (g - f).LimZero ∨ (-(g - f)).Pos
h : (-(g - f)).Pos
⊢ g < f

Tactic:
rwa [neg_sub] at h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem nil_add (xs : IntList) : [] + xs = xs

Proof state:
xs : IntList
⊢ [] + xs = xs

Tactic:
simp [add_def]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma odd_sub' (h : n ≤ m) : Odd (m - n) ↔ (Odd n ↔ Even m)

Proof state:
m n : ℕ
h : n ≤ m
⊢ Odd (m - n) ↔ (Odd n ↔ Even m)

Tactic:
rw [← not_even_iff_odd, even_sub h, not_iff, not_iff_comm, ← not_even_iff_odd]

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem length_sigmaCompositionAux (a : Composition n) (b : Composition a.length)
    (i : Fin b.length) :
    Composition.length (Composition.sigmaCompositionAux a b ⟨i, (length_gather a b).symm ▸ i.2⟩) =
      Composition.blocksFun b i :=
  show List.length ((splitWrtComposition a.blocks b)[i.1]) = blocksFun b i by
    rw [getElem_map_rev List.length, getElem_of_eq (map_length_splitWrtComposition _ _), blocksFun,
      get_eq_getElem]

Proof state:
n : ℕ
a : Composition n
b : Composition a.length
i : Fin b.length
⊢ (a.blocks.splitWrtComposition b)[↑i].length = b.blocksFun i

Tactic:
rw [getElem_map_rev List.length, getElem_of_eq (map_length_splitWrtComposition _ _), blocksFun,
  get_eq_getElem]

Result:
no goals