harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_smul_right (x y : V) (r : ℝ) :
    (o.oangle x (r • y)).sign = SignType.sign r * (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
⊢ (o.oangle x (r • y)).sign = SignType.sign r * (o.oangle x y).sign

Tactic:
rcases lt_trichotomy r 0 with (h | h | h) <;> simp [h]

Result:
no goals
-- Mathlib/Data/List/Lattice.lean
theorem inter_cons_of_not_mem (l₁ : List α) (h : a ∉ l₂) : (a :: l₁) ∩ l₂ = l₁ ∩ l₂

Proof state:
α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = l₁ ∩ l₂

Tactic:
simp [Inter.inter, List.inter, h]

Result:
no goals
-- Mathlib/Algebra/IsPrimePow.lean
theorem isPrimePow_iff_pow_succ : IsPrimePow n ↔ ∃ (p : R) (k : ℕ), Prime p ∧ p ^ (k + 1) = n :=
  (isPrimePow_def _).trans
    ⟨fun ⟨p, k, hp, hk, hn⟩ => ⟨p, k - 1, hp, by rwa [Nat.sub_add_cancel hk]⟩, fun ⟨_, _, hp, hn⟩ =>
      ⟨_, _, hp, Nat.succ_pos', hn⟩⟩

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : R
x✝ : ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
p : R
k : ℕ
hp : Prime p
hk : 0 < k
hn : p ^ k = n
⊢ p ^ (k - 1 + 1) = n

Tactic:
rwa [Nat.sub_add_cancel hk]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean
theorem mk_reindex_fin_cast {n m : ℕ} (h : n = m) (x : ⨂[R]^n M) :
    GradedMonoid.mk (A := fun i => (⨂[R]^i) M) m
    (PiTensorProduct.reindex R (fun _ ↦ M) (finCongr h) x) = GradedMonoid.mk n x

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n m : ℕ
h : n = m
x : ⨂[R]^n M
⊢ GradedMonoid.mk m ((PiTensorProduct.reindex R (fun x => M) (finCongr h)) x) = GradedMonoid.mk n x

Tactic:
rw [finCongr_eq_equivCast, mk_reindex_cast h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_subtype_comap {α} [MeasurableSpace α] {μ : Measure α} {s : Set α}
    (hs : MeasurableSet s) (f : α → G) :
    ∫ x : s, f (x : α) ∂(Measure.comap Subtype.val μ) = ∫ x in s, f x ∂μ

Proof state:
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
α : Type u_7
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → G
⊢ ∫ (x : ↑s), f ↑x ∂Measure.comap Subtype.val μ = ∫ (x : α) in s, f x ∂μ

Tactic:
rw [← map_comap_subtype_coe hs]

Result:
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
α : Type u_7
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → G
⊢ ∫ (x : ↑s), f ↑x ∂Measure.comap Subtype.val μ = ∫ (x : α), f x ∂Measure.map Subtype.val (Measure.comap Subtype.val μ)

Proof state:
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
α : Type u_7
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → G
⊢ ∫ (x : ↑s), f ↑x ∂Measure.comap Subtype.val μ = ∫ (x : α), f x ∂Measure.map Subtype.val (Measure.comap Subtype.val μ)

Tactic:
exact ((MeasurableEmbedding.subtype_coe hs).integral_map _).symm

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_eq_sum_filter [DecidablePred fun x ↦ x ≠ (0 : F)]
    {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') (f : α →ₛ F) :
    setToSimpleFunc T f = ∑ x ∈ f.range with x ≠ 0, T (f ⁻¹' {x}) x

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : DecidablePred fun x => x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
x : F
x✝ : x ∈ f.range
hx0 : x = 0
⊢ (T (⇑f ⁻¹' {x})) x = 0

Tactic:
rw [hx0]

Result:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : DecidablePred fun x => x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
x : F
x✝ : x ∈ f.range
hx0 : x = 0
⊢ (T (⇑f ⁻¹' {0})) 0 = 0

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : DecidablePred fun x => x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ setToSimpleFunc T f = ∑ x ∈ filter (fun x => x ≠ 0) f.range, (T (⇑f ⁻¹' {x})) x

Tactic:
symm

Result:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : DecidablePred fun x => x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x ∈ filter (fun x => x ≠ 0) f.range, (T (⇑f ⁻¹' {x})) x = setToSimpleFunc T f

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : DecidablePred fun x => x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
x : F
x✝ : x ∈ f.range
hx0 : x = 0
⊢ (T (⇑f ⁻¹' {0})) 0 = 0

Tactic:
exact ContinuousLinearMap.map_zero _

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : DecidablePred fun x => x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x ∈ filter (fun x => x ≠ 0) f.range, (T (⇑f ⁻¹' {x})) x = setToSimpleFunc T f

Tactic:
refine sum_filter_of_ne fun x _ => mt fun hx0 => ?_

Result:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : DecidablePred fun x => x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
x : F
x✝ : x ∈ f.range
hx0 : x = 0
⊢ (T (⇑f ⁻¹' {x})) x = 0
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem num_le (I : FractionalIdeal S P) :
    (I.num : FractionalIdeal S P) ≤ I

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ ↑I.num ≤ I

Tactic:
rw [← I.den_mul_self_eq_num', spanSingleton_mul_le_iff]

Result:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ ∀ z ∈ I, (algebraMap R P) ↑I.den * z ∈ I

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
z✝ : P
h : z✝ ∈ I
⊢ ↑I.den • z✝ ∈ I

Tactic:
exact Submodule.smul_mem _ _ h

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
⊢ ∀ z ∈ I, (algebraMap R P) ↑I.den * z ∈ I

Tactic:
intro _ h

Result:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
z✝ : P
h : z✝ ∈ I
⊢ (algebraMap R P) ↑I.den * z✝ ∈ I

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
z✝ : P
h : z✝ ∈ I
⊢ (algebraMap R P) ↑I.den * z✝ ∈ I

Tactic:
rw [← Algebra.smul_def]

Result:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
I : FractionalIdeal S P
z✝ : P
h : z✝ ∈ I
⊢ ↑I.den • z✝ ∈ I
-- Mathlib/CategoryTheory/Category/ReflQuiv.lean
theorem freeRefl_naturality {X Y} [ReflQuiver X] [ReflQuiver Y] (f : X ⥤rq Y) :
    free.map (X := Quiv.of X) (Y := Quiv.of Y) f.toPrefunctor ⋙
    FreeRefl.quotientFunctor ↑Y =
    FreeRefl.quotientFunctor ↑X ⋙ freeRefl.map (X := ReflQuiv.of X) (Y := ReflQuiv.of Y) f

Proof state:
X Y : Type u_1
inst✝¹ : ReflQuiver X
inst✝ : ReflQuiver Y
f : X ⥤rq Y
⊢ free.map f.toPrefunctor ⋙ Quotient.functor FreeReflRel =
    Quotient.functor FreeReflRel ⋙ Quotient.lift FreeReflRel (free.map f.toPrefunctor ⋙ Quotient.functor FreeReflRel) ⋯

Tactic:
rw [Quotient.lift_spec]

Result:
no goals

Proof state:
X Y : Type u_1
inst✝¹ : ReflQuiver X
inst✝ : ReflQuiver Y
f : X ⥤rq Y
⊢ free.map f.toPrefunctor ⋙ FreeRefl.quotientFunctor Y = FreeRefl.quotientFunctor X ⋙ freeRefl.map f

Tactic:
simp only [free_obj, FreeRefl.quotientFunctor, freeRefl, ReflQuiv.of_val]

Result:
X Y : Type u_1
inst✝¹ : ReflQuiver X
inst✝ : ReflQuiver Y
f : X ⥤rq Y
⊢ free.map f.toPrefunctor ⋙ Quotient.functor FreeReflRel =
    Quotient.functor FreeReflRel ⋙ Quotient.lift FreeReflRel (free.map f.toPrefunctor ⋙ Quotient.functor FreeReflRel) ⋯
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_addXYZ (P Q : Fin 3 → R) :
    (W'.map f).toProjective.addXYZ (f ∘ P) (f ∘ Q) = f ∘ addXYZ W' P Q

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P Q : Fin 3 → R
⊢ (map W' f).toProjective.addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W'.addXYZ P Q

Tactic:
simp only [addXYZ, map_addX, map_addY, map_addZ, comp_fin3]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem orthogonalProjectionFn_mem {s : AffineSubspace ℝ P} [Nonempty s]
    [HasOrthogonalProjection s.direction] (p : P) : orthogonalProjectionFn s p ∈ s

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ orthogonalProjectionFn s p ∈ s

Tactic:
rw [← mem_coe, ← Set.singleton_subset_iff, ← inter_eq_singleton_orthogonalProjectionFn]

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ ↑s ∩ ↑(mk' p s.directionᗮ) ⊆ ↑s

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
⊢ ↑s ∩ ↑(mk' p s.directionᗮ) ⊆ ↑s

Tactic:
exact Set.inter_subset_left

Result:
no goals
-- Mathlib/Control/Traversable/Lemmas.lean
theorem comp_sequence (x : t (F (G α))) :
    sequence (Comp.mk <$> x) = Comp.mk (sequence <$> sequence x)

Proof state:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ sequence (Comp.mk <$> x) = Comp.mk (sequence <$> sequence x)

Tactic:
simp only [sequence, traverse_map, id_comp]

Result:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ traverse Comp.mk x = Comp.mk (traverse id <$> traverse id x)

Proof state:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ traverse Comp.mk x = Comp.mk (traverse id <$> traverse id x)

Tactic:
rw [← comp_traverse]

Result:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ traverse Comp.mk x = traverse (Comp.mk ∘ map id ∘ id) x

Proof state:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u
x : t (F (G α))
⊢ traverse Comp.mk x = traverse (Comp.mk ∘ map id ∘ id) x

Tactic:
simp [map_id]

Result:
no goals
-- Mathlib/Topology/LocallyClosed.lean
theorem coborder_eq_union_closure_compl {s : Set X} : coborder s = s ∪ (closure s)ᶜ

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s ∩ sᶜ = closure s \ s

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ coborder s = s ∪ (closure s)ᶜ

Tactic:
rw [coborder, compl_eq_comm, compl_union, compl_compl, inter_comm]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s ∩ sᶜ = closure s \ s
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_zero_X : coeff R 0 (X : R⟦X⟧) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ (coeff R 0) X = 0

Tactic:
rw [coeff, Finsupp.single_zero, X, MvPowerSeries.coeff_zero_X]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m

Proof state:
m x✝ y x : Nat
⊢ (m * (x + 1) + y) % m = y % m

Tactic:
simp [Nat.mul_succ, Nat.add_assoc _ m, mul_add_mod _ x]

Result:
no goals

Proof state:
m x y : Nat
⊢ (m * 0 + y) % m = y % m

Tactic:
simp

Result:
no goals

Proof state:
m x y : Nat
⊢ (m * x + y) % m = y % m

Tactic:
match x with
| 0 => simp
| x + 1 =>
  simp [Nat.mul_succ, Nat.add_assoc _ m, mul_add_mod _ x]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem iteratedFDeriv_succ_apply_right {n : ℕ} (m : Fin (n + 1) → E) :
    (iteratedFDeriv 𝕜 (n + 1) f x : (Fin (n + 1) → E) → F) m =
      iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x (init m) (m (last n))

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ (iteratedFDeriv 𝕜 (n + 1) f x) m = ((iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x) (init m)) (m (last n))

Tactic:
rw [← iteratedFDerivWithin_univ, ← iteratedFDerivWithin_univ, ← fderivWithin_univ]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) f univ x) m =
    ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f univ y) univ x) (init m)) (m (last n))

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ
m : Fin (n + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (n + 1) f univ x) m =
    ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f univ y) univ x) (init m)) (m (last n))

Tactic:
exact iteratedFDerivWithin_succ_apply_right uniqueDiffOn_univ (mem_univ _) _

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem filter_le_lt_eq_Ico [DecidablePred fun j => a ≤ j ∧ j < b] :
    ({j | a ≤ j ∧ j < b} : Finset _) = Ico a b

Proof state:
case h
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a ≤ j ∧ j < b
a✝ : α
⊢ a✝ ∈ filter (fun j => a ≤ j ∧ j < b) univ ↔ a✝ ∈ Ico a b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a ≤ j ∧ j < b
⊢ filter (fun j => a ≤ j ∧ j < b) univ = Ico a b

Tactic:
ext

Result:
case h
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a ≤ j ∧ j < b
a✝ : α
⊢ a✝ ∈ filter (fun j => a ≤ j ∧ j < b) univ ↔ a✝ ∈ Ico a b
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem closedBall_mul_singleton : closedBall x δ * {y} = closedBall (x * y) δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ closedBall x δ * {y} = closedBall (x * y) δ

Tactic:
simp [mul_comm _ {y}, mul_comm y]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem vector_tail {n} : Primrec (@List.Vector.tail α n) :=
  vector_toList_iff.1 <| (list_tail.comp vector_toList).of_eq fun ⟨l, h⟩ => by cases l <;> rfl

Proof state:
α : Type u_1
inst✝ : Primcodable α
n : ℕ
x✝ : List.Vector α n
l : List α
h : l.length = n
⊢ (Vector.toList ⟨l, h⟩).tail = (List.Vector.tail ⟨l, h⟩).toList

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Directed.lean
theorem iSupLift_of_mem {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
    {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)}
    {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (x : T) (hx : (x : A) ∈ K i) :
    iSupLift K dir f hf T hT x = f i ⟨x, hx⟩

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
x : ↥T
hx : ↑x ∈ K i
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑T ⋯ x = (f i) ⟨↑x, hx⟩

Tactic:
rw [Set.iUnionLift_of_mem]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
x : ↥T
hx : ↑x ∈ K i
⊢ (iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩

Tactic:
dsimp [iSupLift, inclusion]

Result:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
x : ↥T
hx : ↑x ∈ K i
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑T ⋯ x = (f i) ⟨↑x, hx⟩
-- Mathlib/Order/Birkhoff.lean
lemma infIrredUpperSet_surjective : Surjective (infIrredUpperSet (α := α))

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : Finite α
⊢ Surjective ⇑infIrredUpperSet

Tactic:
aesop (add simp Surjective)

Result:
no goals
-- Mathlib/GroupTheory/Submonoid/Inverses.lean
theorem fromLeftInv_mul (x : S.leftInv) : (S.fromLeftInv x : M) * x = 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x : ↥S.leftInv
⊢ ↑(S.fromLeftInv x) * ↑x = 1

Tactic:
rw [mul_comm, mul_fromLeftInv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem length_append (as bs : List α) : (as ++ bs).length = as.length + bs.length

Proof state:
α : Type u
as bs : List α
⊢ (as ++ bs).length = as.length + bs.length

Tactic:
induction as with
| nil => simp
| cons _ as ih => simp [ih, Nat.succ_add]

Result:
no goals

Proof state:
case cons
α : Type u
bs : List α
head✝ : α
as : List α
ih : (as ++ bs).length = as.length + bs.length
⊢ (head✝ :: as ++ bs).length = (head✝ :: as).length + bs.length

Tactic:
simp [ih, Nat.succ_add]

Result:
no goals

Proof state:
case nil
α : Type u
bs : List α
⊢ (nil ++ bs).length = nil.length + bs.length

Tactic:
simp

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem factorMultiset_pow (n : ℕ+) (m : ℕ) :
    factorMultiset (n ^ m) = m • factorMultiset n

Proof state:
n : ℕ+
m : ℕ
⊢ (n ^ m).factorMultiset = m • n.factorMultiset

Tactic:
let u := factorMultiset n

Result:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
⊢ (n ^ m).factorMultiset = m • n.factorMultiset

Proof state:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (m • u).prod.factorMultiset = m • u.prod.factorMultiset

Tactic:
repeat' rw [PrimeMultiset.factorMultiset_prod]

Result:
no goals

Proof state:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
⊢ (n ^ m).factorMultiset = m • n.factorMultiset

Tactic:
have : n = u.prod := (prod_factorMultiset n).symm

Result:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (n ^ m).factorMultiset = m • n.factorMultiset

Proof state:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (n ^ m).factorMultiset = m • n.factorMultiset

Tactic:
rw [this, ← PrimeMultiset.prod_smul]

Result:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (m • u).prod.factorMultiset = m • u.prod.factorMultiset

Proof state:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ m • u = m • u.prod.factorMultiset

Tactic:
rw [PrimeMultiset.factorMultiset_prod]

Result:
no goals
-- Mathlib/Algebra/CharP/Invertible.lean
theorem not_ringChar_dvd_of_invertible {t : ℕ} [Invertible (t : K)] : ¬ringChar K ∣ t

Proof state:
K : Type u_1
inst✝¹ : Field K
t : ℕ
inst✝ : Invertible ↑t
⊢ ↑t ≠ 0

Tactic:
exact Invertible.ne_zero (t : K)

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
t : ℕ
inst✝ : Invertible ↑t
⊢ ¬ringChar K ∣ t

Tactic:
rw [← ringChar.spec, ← Ne]

Result:
K : Type u_1
inst✝¹ : Field K
t : ℕ
inst✝ : Invertible ↑t
⊢ ↑t ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem ratUnits_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
    (insert f c).ratUnits = f.ratUnits

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
      | none =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }
      | some (l, true) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addPosAssignment }
      | some (l, false) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addNegAssignment }).ratUnits =
    f.ratUnits

Tactic:
split <;> simp only

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (f.insert c).ratUnits = f.ratUnits

Tactic:
simp only [insert]

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
      | none =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }
      | some (l, true) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addPosAssignment }
      | some (l, false) =>
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.val addNegAssignment }).ratUnits =
    f.ratUnits
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem ne_zero_of_isUnit [Nontrivial Γ₀] (v : Valuation K Γ₀) (x : K) (hx : IsUnit x) :
    v x ≠ (0 : Γ₀)

Proof state:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : Nontrivial Γ₀
v : Valuation K Γ₀
x : K
hx : IsUnit x
⊢ v x ≠ 0

Tactic:
simpa [hx.choose_spec] using ne_zero_of_unit v hx.choose

Result:
no goals