harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Extension.lean
@[simp]
lemma σ_smul (x y) : P.σ x • y = x * y

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x y : S
⊢ P.σ x • y = x * y

Tactic:
rw [Algebra.smul_def, algebraMap_σ]

Result:
no goals
-- Mathlib/RingTheory/Trace/Defs.lean
theorem trace_eq_matrix_trace [DecidableEq ι] (b : Basis ι R S) (s : S) :
    trace R S s = Matrix.trace (Algebra.leftMulMatrix b s)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ (trace R S) s = ((leftMulMatrix b) s).trace

Tactic:
rw [trace_apply, LinearMap.trace_eq_matrix_trace _ b, ← toMatrix_lmul_eq]

Result:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ ((toMatrix b b) ((lmul R S) s)).trace = ((toMatrix b b) (mulLeft R s)).trace

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι : Type w
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι R S
s : S
⊢ ((toMatrix b b) ((lmul R S) s)).trace = ((toMatrix b b) (mulLeft R s)).trace

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem IsLindelof.induction_on (hs : IsLindelof s) {p : Set X → Prop}
    (hmono : ∀ ⦃s t⦄, s ⊆ t → p t → p s)
    (hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S))
    (hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t) : p s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
p : Set X → Prop
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := ofCountableUnion p hcountable_union ⋯
this : sᶜ ∈ f
⊢ p s

Tactic:
rwa [← compl_compl s]

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
p : Set X → Prop
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := ofCountableUnion p hcountable_union ⋯
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f

Tactic:
simpa [f] using hnhds

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
p : Set X → Prop
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := ofCountableUnion p hcountable_union ⋯
⊢ p s

Tactic:
have : sᶜ ∈ f := hs.compl_mem_sets_of_nhdsWithin (by simpa [f] using hnhds)

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
p : Set X → Prop
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := ofCountableUnion p hcountable_union ⋯
this : sᶜ ∈ f
⊢ p s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
p : Set X → Prop
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
⊢ p s

Tactic:
let f : Filter X := ofCountableUnion p hcountable_union (fun t ht _ hsub ↦ hmono hsub ht)

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsLindelof s
p : Set X → Prop
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := ofCountableUnion p hcountable_union ⋯
⊢ p s
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem laverage_union (hd : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) :
    ⨍⁻ x in s ∪ t, f x ∂μ =
      μ s / (μ s + μ t) * ⨍⁻ x in s, f x ∂μ + μ t / (μ s + μ t) * ⨍⁻ x in t, f x ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ =
    μ s / (μ s + μ t) * ⨍⁻ (x : α) in s, f x ∂μ + μ t / (μ s + μ t) * ⨍⁻ (x : α) in t, f x ∂μ

Tactic:
rw [restrict_union₀ hd ht, laverage_add_measure, restrict_apply_univ, restrict_apply_univ]

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Tuple.lean
lemma cons_add_cons (x : α) (v : Fin n → α) (y : α) (w : Fin n → α) :
    vecCons x v + vecCons y w = vecCons (x + y) (v + w)

Proof state:
α : Type u_1
n : ℕ
inst✝ : Add α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v + vecCons y w = vecCons (x + y) (v + w)

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem le_iff_forall_lf {x y : PGame} :
    x ≤ y ↔ (∀ i, x.moveLeft i ⧏ y) ∧ ∀ j, x ⧏ y.moveRight j

Proof state:
x y : PGame
⊢ x ≤ y ↔ (∀ (i : x.LeftMoves), x.moveLeft i ⧏ y) ∧ ∀ (j : y.RightMoves), x ⧏ y.moveRight j

Tactic:
unfold LE.le le

Result:
x y : PGame
⊢ {
          le :=
            Sym2.GameAdd.fix wf_isOption fun x y le =>
              (∀ (i : x.LeftMoves), ¬le y (x.moveLeft i) ⋯) ∧ ∀ (j : y.RightMoves), ¬le (y.moveRight j) x ⋯ }.1
      x y ↔
    (∀ (i : x.LeftMoves), x.moveLeft i ⧏ y) ∧ ∀ (j : y.RightMoves), x ⧏ y.moveRight j

Proof state:
x y : PGame
⊢ {
          le :=
            Sym2.GameAdd.fix wf_isOption fun x y le =>
              (∀ (i : x.LeftMoves), ¬le y (x.moveLeft i) ⋯) ∧ ∀ (j : y.RightMoves), ¬le (y.moveRight j) x ⋯ }.1
      x y ↔
    (∀ (i : x.LeftMoves), x.moveLeft i ⧏ y) ∧ ∀ (j : y.RightMoves), x ⧏ y.moveRight j

Tactic:
simp only

Result:
x y : PGame
⊢ Sym2.GameAdd.fix wf_isOption
      (fun x y le => (∀ (i : x.LeftMoves), ¬le y (x.moveLeft i) ⋯) ∧ ∀ (j : y.RightMoves), ¬le (y.moveRight j) x ⋯) x
      y ↔
    (∀ (i : x.LeftMoves), x.moveLeft i ⧏ y) ∧ ∀ (j : y.RightMoves), x ⧏ y.moveRight j

Proof state:
x y : PGame
⊢ ((∀ (i : x.LeftMoves),
        ¬(fun a' b' x =>
              Sym2.GameAdd.fix wf_isOption
                (fun x y le =>
                  (∀ (i : x.LeftMoves), ¬le y (x.moveLeft i) ⋯) ∧ ∀ (j : y.RightMoves), ¬le (y.moveRight j) x ⋯)
                a' b')
            y (x.moveLeft i) ⋯) ∧
      ∀ (j : y.RightMoves),
        ¬(fun a' b' x =>
              Sym2.GameAdd.fix wf_isOption
                (fun x y le =>
                  (∀ (i : x.LeftMoves), ¬le y (x.moveLeft i) ⋯) ∧ ∀ (j : y.RightMoves), ¬le (y.moveRight j) x ⋯)
                a' b')
            (y.moveRight j) x ⋯) ↔
    (∀ (i : x.LeftMoves), x.moveLeft i ⧏ y) ∧ ∀ (j : y.RightMoves), x ⧏ y.moveRight j

Tactic:
rfl

Result:
no goals

Proof state:
x y : PGame
⊢ Sym2.GameAdd.fix wf_isOption
      (fun x y le => (∀ (i : x.LeftMoves), ¬le y (x.moveLeft i) ⋯) ∧ ∀ (j : y.RightMoves), ¬le (y.moveRight j) x ⋯) x
      y ↔
    (∀ (i : x.LeftMoves), x.moveLeft i ⧏ y) ∧ ∀ (j : y.RightMoves), x ⧏ y.moveRight j

Tactic:
rw [Sym2.GameAdd.fix_eq]

Result:
x y : PGame
⊢ ((∀ (i : x.LeftMoves),
        ¬(fun a' b' x =>
              Sym2.GameAdd.fix wf_isOption
                (fun x y le =>
                  (∀ (i : x.LeftMoves), ¬le y (x.moveLeft i) ⋯) ∧ ∀ (j : y.RightMoves), ¬le (y.moveRight j) x ⋯)
                a' b')
            y (x.moveLeft i) ⋯) ∧
      ∀ (j : y.RightMoves),
        ¬(fun a' b' x =>
              Sym2.GameAdd.fix wf_isOption
                (fun x y le =>
                  (∀ (i : x.LeftMoves), ¬le y (x.moveLeft i) ⋯) ∧ ∀ (j : y.RightMoves), ¬le (y.moveRight j) x ⋯)
                a' b')
            (y.moveRight j) x ⋯) ↔
    (∀ (i : x.LeftMoves), x.moveLeft i ⧏ y) ∧ ∀ (j : y.RightMoves), x ⧏ y.moveRight j
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_X_empty (H : (1 : R) = 0) : (X : R[X]).support = ∅

Proof state:
R : Type u
inst✝ : Semiring R
H : 1 = 0
⊢ X.support = ∅

Tactic:
rw [X, H, monomial_zero_right, support_zero]

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Submodule.eq_bot_of_isLocalized'_span {N : Submodule R M}
    (h : ∀ r : s, N.localized' (Rₚ r) (.powers r.1) (f r) = ⊥) : N = ⊥ :=
  eq_of_isLocalized'_span s span_eq Rₚ Mₚ f fun _ ↦ by simp only [h, Submodule.localized'_bot]

Proof state:
R : Type u_1
M : Type u_2
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Rₚ : ↑s → Type u_4
inst✝⁷ : (r : ↑s) → CommSemiring (Rₚ r)
inst✝⁶ : (r : ↑s) → Algebra R (Rₚ r)
inst✝⁵ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rₚ r)
Mₚ : ↑s → Type u_5
inst✝⁴ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝³ : (r : ↑s) → Module R (Mₚ r)
inst✝² : (r : ↑s) → Module (Rₚ r) (Mₚ r)
inst✝¹ : ∀ (r : ↑s), IsScalarTower R (Rₚ r) (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
N : Submodule R M
h : ∀ (r : ↑s), localized' (Rₚ r) (Submonoid.powers ↑r) (f r) N = ⊥
x✝ : ↑s
⊢ localized' (Rₚ x✝) (Submonoid.powers ↑x✝) (f x✝) N = localized' (Rₚ x✝) (Submonoid.powers ↑x✝) (f x✝) ⊥

Tactic:
simp only [h, Submodule.localized'_bot]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {v : β k} :
    (m.insertIfNew k v).contains a = (k == a || m.contains a)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).contains a = (k == a || m.contains a)

Tactic:
simp_to_raw using Raw₀.contains_insertIfNew

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
lemma sin_half_eq_neg_sqrt {x : ℝ} (hl : -(2 * π) ≤ x) (hr : x ≤ 0) :
    sin (x / 2) = -sqrt ((1 - cos x) / 2)

Proof state:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
⊢ sin (x / 2) ≤ 0

Tactic:
apply sin_nonpos_of_nonnpos_of_neg_pi_le <;> linarith

Result:
no goals

Proof state:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
⊢ sin (x / 2) = -√((1 - cos x) / 2)

Tactic:
rw [← abs_sin_half, abs_of_nonpos, neg_neg]

Result:
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
⊢ sin (x / 2) ≤ 0
-- Mathlib/Data/Finset/Max.lean
theorem map_ofDual_max (s : Finset αᵒᵈ) : s.max.map ofDual = (s.image ofDual).min

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithBot.map (⇑ofDual) s.max = s.inf (WithTop.some ∘ ⇑ofDual)

Tactic:
exact congr_fun Option.map_id _

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithBot.map (⇑ofDual) s.max = (image (⇑ofDual) s).min

Tactic:
rw [min_eq_inf_withTop, inf_image]

Result:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithBot.map (⇑ofDual) s.max = s.inf (WithTop.some ∘ ⇑ofDual)
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem nhds_zero : 𝓝 (0 : ℝ≥0∞) = ⨅ (a) (_ : a ≠ 0), 𝓟 (Iio a) :=
  nhds_bot_order.trans <| by simp [pos_iff_ne_zero, Iio]

Proof state:
⊢ ⨅ l, ⨅ (_ : ⊥ < l), 𝓟 (Iio l) = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Iio a)

Tactic:
simp [pos_iff_ne_zero, Iio]

Result:
no goals
-- Mathlib/Analysis/Convex/Topology.lean
theorem Convex.isPathConnected {s : Set E} (hconv : Convex ℝ s) (hne : s.Nonempty) :
    IsPathConnected s

Proof state:
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : s.Nonempty
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
⊢ JoinedIn s x y

Tactic:
exact JoinedIn.of_segment_subset ((segment_subset_iff ℝ).2 (hconv x_in y_in))

Result:
no goals

Proof state:
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : s.Nonempty
⊢ IsPathConnected s

Tactic:
refine isPathConnected_iff.mpr ⟨hne, ?_⟩

Result:
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : s.Nonempty
⊢ ∀ x ∈ s, ∀ y ∈ s, JoinedIn s x y

Proof state:
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : s.Nonempty
⊢ ∀ x ∈ s, ∀ y ∈ s, JoinedIn s x y

Tactic:
intro x x_in y y_in

Result:
E : Type u_3
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
s : Set E
hconv : Convex ℝ s
hne : s.Nonempty
x : E
x_in : x ∈ s
y : E
y_in : y ∈ s
⊢ JoinedIn s x y
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
@[simp] lemma lineMap_lineMap_left (p₀ p₁ : P1) (c d : k) :
    lineMap (lineMap p₀ p₁ c) p₁ d = lineMap p₀ p₁ (1 - (1 - d) * (1 - c))

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V1
inst✝¹ : Module k V1
inst✝ : AffineSpace V1 P1
p₀ p₁ : P1
c d : k
⊢ (lineMap ((lineMap p₀ p₁) c) p₁) d = (lineMap p₀ p₁) (1 - (1 - d) * (1 - c))

Tactic:
simp_rw [lineMap_apply_one_sub, ← lineMap_apply_one_sub p₁, lineMap_lineMap_right]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem exp_mul_I_antiperiodic : Function.Antiperiodic (fun x => exp (x * I)) π

Proof state:
⊢ Function.Antiperiodic (fun x => cexp (x * I)) ↑π

Tactic:
simpa only [mul_inv_cancel_right₀ I_ne_zero] using exp_antiperiodic.mul_const I_ne_zero

Result:
no goals
-- Mathlib/Algebra/Quandle.lean
theorem fix_inv {x : Q} : x ◃⁻¹ x = x

Proof state:
Q : Type u_1
inst✝ : Quandle Q
x : Q
⊢ x ◃ x ◃⁻¹ x = x ◃ x

Tactic:
simp

Result:
no goals

Proof state:
Q : Type u_1
inst✝ : Quandle Q
x : Q
⊢ x ◃⁻¹ x = x

Tactic:
rw [← left_cancel x]

Result:
Q : Type u_1
inst✝ : Quandle Q
x : Q
⊢ x ◃ x ◃⁻¹ x = x ◃ x
-- Mathlib/Data/Num/Lemmas.lean
theorem sub_to_nat (m n) : ((m - n : Num) : ℕ) = m - n :=
  show (ofZNum _ : ℕ) = _ by
    rw [ofZNum_toNat, cast_sub', ← to_nat_to_int, ← to_nat_to_int, Int.toNat_sub]

Proof state:
m n : Num
⊢ ↑(ofZNum (m.sub' n)) = ↑m - ↑n

Tactic:
rw [ofZNum_toNat, cast_sub', ← to_nat_to_int, ← to_nat_to_int, Int.toNat_sub]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem mem_nthRoots {n : ℕ} (hn : 0 < n) {a x : R} : x ∈ nthRoots n a ↔ x ^ n = a

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
hn : 0 < n
a x : R
⊢ x ∈ nthRoots n a ↔ x ^ n = a

Tactic:
rw [nthRoots, mem_roots (X_pow_sub_C_ne_zero hn a), IsRoot.def, eval_sub, eval_C, eval_pow,
  eval_X, sub_eq_zero]

Result:
no goals
-- Mathlib/Order/Heyting/Hom.lean
theorem map_bihimp (a b : α) : f (a ⇔ b) = f a ⇔ f b

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
a b : α
⊢ f (a ⇔ b) = f a ⇔ f b

Tactic:
simp_rw [bihimp, map_inf, map_himp]

Result:
no goals
-- Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean
lemma isCardinalFiltered_preorder (J : Type w) [Preorder J]
    (κ : Cardinal.{w}) [Fact κ.IsRegular]
    (h : ∀ ⦃K : Type w⦄ (s : K → J) (_ : Cardinal.mk K < κ),
      ∃ (j : J), ∀ (k : K), s k ≤ j) :
    IsCardinalFiltered J κ where
  nonempty_cocone {A _ F hA}

Proof state:
case intro
J : Type w
inst✝¹ : Preorder J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ ⦃K : Type w⦄ (s : K → J), Cardinal.mk K < κ → ∃ j, ∀ (k : K), s k ≤ j
A : Type w
x✝ : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
j : J
hj : ∀ (k : A), F.obj k ≤ j
⊢ Nonempty (Cocone F)

Tactic:
exact ⟨Cocone.mk j
  { app a := homOfLE (hj a)
    naturality _ _ _ := rfl }⟩

Result:
no goals

Proof state:
J : Type w
inst✝¹ : Preorder J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ ⦃K : Type w⦄ (s : K → J), Cardinal.mk K < κ → ∃ j, ∀ (k : K), s k ≤ j
A : Type w
x✝ : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
⊢ Nonempty (Cocone F)

Tactic:
obtain ⟨j, hj⟩ := h F.obj (by simpa only [hasCardinalLT_iff_cardinal_mk_lt] using
    hasCardinalLT_of_hasCardinalLT_arrow hA)

Result:
case intro
J : Type w
inst✝¹ : Preorder J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ ⦃K : Type w⦄ (s : K → J), Cardinal.mk K < κ → ∃ j, ∀ (k : K), s k ≤ j
A : Type w
x✝ : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
j : J
hj : ∀ (k : A), F.obj k ≤ j
⊢ Nonempty (Cocone F)

Proof state:
J : Type w
inst✝¹ : Preorder J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ ⦃K : Type w⦄ (s : K → J), Cardinal.mk K < κ → ∃ j, ∀ (k : K), s k ≤ j
A : Type w
x✝ : SmallCategory A
F : A ⥤ J
hA : HasCardinalLT (Arrow A) κ
⊢ Cardinal.mk A < κ

Tactic:
simpa only [hasCardinalLT_iff_cardinal_mk_lt] using
hasCardinalLT_of_hasCardinalLT_arrow hA

Result:
no goals
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem pNilradical_eq_nilradical {R : Type*} [CommSemiring R] {p : ℕ} (hp : 1 < p) :
    pNilradical R p = nilradical R

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
hp : 1 < p
⊢ pNilradical R p = nilradical R

Tactic:
rw [pNilradical, if_pos hp]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem continuous_prod_of_dense_continuous_lipschitzWith [PseudoEMetricSpace α]
    [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : ℝ≥0) {s : Set α}
    (hs : Dense s) (ha : ∀ a ∈ s, Continuous fun y => f (a, y))
    (hb : ∀ b, LipschitzWith K fun x => f (x, b)) : Continuous f

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
s : Set α
hs : Dense s
ha : ∀ a ∈ s, Continuous fun y => f (a, y)
hb : ∀ (b : β), LipschitzWith K fun x => f (x, b)
⊢ Continuous f

Tactic:
simp only [continuous_iff_continuousOn_univ, ← univ_prod_univ, ← lipschitzOnWith_univ] at *

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
s : Set α
hs : Dense s
ha : ∀ a ∈ s, ContinuousOn (fun y => f (a, y)) univ
hb : ∀ (b : β), LipschitzOnWith K (fun x => f (x, b)) univ
⊢ ContinuousOn f (univ ×ˢ univ)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
s : Set α
hs : Dense s
ha : ∀ a ∈ s, ContinuousOn (fun y => f (a, y)) univ
hb : ∀ (b : β), LipschitzOnWith K (fun x => f (x, b)) univ
⊢ ContinuousOn f (univ ×ˢ univ)

Tactic:
exact continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith f (subset_univ _)
  hs.closure_eq.ge K ha fun b _ => hb b

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiffWithinAt.sub {s : Set E} {f g : E → F} (hf : ContDiffWithinAt 𝕜 n f s x)
    (hg : ContDiffWithinAt 𝕜 n g s x) : ContDiffWithinAt 𝕜 n (fun x => f x - g x) s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : WithTop ℕ∞
s : Set E
f g : E → F
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
⊢ ContDiffWithinAt 𝕜 n (fun x => f x - g x) s x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem IsNormal.vertexSubgroup (Sn : IsNormal S) (c : C) (cS : c ∈ S.objs) :
    (S.vertexSubgroup cS).Normal where
  conj_mem x hx y

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c : C
cS : c ∈ S.objs
x : c ⟶ c
hx : x ∈ S.vertexSubgroup cS
y : c ⟶ c
⊢ y * x * y⁻¹ ∈ S.vertexSubgroup cS

Tactic:
rw [mul_assoc]

Result:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c : C
cS : c ∈ S.objs
x : c ⟶ c
hx : x ∈ S.vertexSubgroup cS
y : c ⟶ c
⊢ y * (x * y⁻¹) ∈ S.vertexSubgroup cS

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
Sn : S.IsNormal
c : C
cS : c ∈ S.objs
x : c ⟶ c
hx : x ∈ S.vertexSubgroup cS
y : c ⟶ c
⊢ y * (x * y⁻¹) ∈ S.vertexSubgroup cS

Tactic:
exact Sn.conj' y hx

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem one_le_encard_iff_nonempty : 1 ≤ s.encard ↔ s.Nonempty

Proof state:
α : Type u_1
s : Set α
⊢ 1 ≤ s.encard ↔ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty, Ne, ← encard_eq_zero, ENat.one_le_iff_ne_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
theorem integral_comp_mul_left (g : ℝ → F) (a : ℝ) :
    (∫ x : ℝ, g (a * x)) = |a⁻¹| • ∫ y : ℝ, g y

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
g : ℝ → F
a : ℝ
⊢ ∫ (x : ℝ), g (a * x) = |a⁻¹| • ∫ (y : ℝ), g y

Tactic:
simp_rw [← smul_eq_mul, Measure.integral_comp_smul, Module.finrank_self, pow_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem atLeastTwo_true_left   : atLeastTwo true b c  = (b || c)

Proof state:
b c : Bool
⊢ true.atLeastTwo b c = (b || c)

Tactic:
cases b <;> cases c <;> simp [atLeastTwo]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem eventuallyEq_of_toReal_eventuallyEq {l : Filter α} {f g : α → ℝ≥0∞}
    (hfi : ∀ᶠ x in l, f x ≠ ∞) (hgi : ∀ᶠ x in l, g x ≠ ∞)
    (hfg : (fun x => (f x).toReal) =ᶠ[l] fun x => (g x).toReal) : f =ᶠ[l] g

Proof state:
α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ⊤
hgi : ∀ᶠ (x : α) in l, g x ≠ ⊤
hfg : (fun x => (f x).toReal) =ᶠ[l] fun x => (g x).toReal
⊢ f =ᶠ[l] g

Tactic:
filter_upwards [hfi, hgi, hfg] with _ hfx hgx _

Result:
case h
α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ⊤
hgi : ∀ᶠ (x : α) in l, g x ≠ ⊤
hfg : (fun x => (f x).toReal) =ᶠ[l] fun x => (g x).toReal
a✝¹ : α
hfx : f a✝¹ ≠ ⊤
hgx : g a✝¹ ≠ ⊤
a✝ : (f a✝¹).toReal = (g a✝¹).toReal
⊢ f a✝¹ = g a✝¹

Proof state:
case h
α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ⊤
hgi : ∀ᶠ (x : α) in l, g x ≠ ⊤
hfg : (fun x => (f x).toReal) =ᶠ[l] fun x => (g x).toReal
a✝¹ : α
hfx : f a✝¹ ≠ ⊤
hgx : g a✝¹ ≠ ⊤
a✝ : (f a✝¹).toReal = (g a✝¹).toReal
⊢ f a✝¹ = g a✝¹

Tactic:
rwa [← ENNReal.toReal_eq_toReal hfx hgx]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem abs_cos_int_mul_pi (k : ℤ) : |cos (k * π)| = 1

Proof state:
k : ℤ
⊢ |cos (↑k * π)| = 1

Tactic:
simp [abs_cos_eq_sqrt_one_sub_sin_sq]

Result:
no goals
-- Mathlib/Analysis/Complex/CauchyIntegral.lean
theorem integral_boundary_rect_eq_zero_of_differentiable_on_off_countable (f : ℂ → E) (z w : ℂ)
    (s : Set ℂ) (hs : s.Countable) (Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]]))
    (Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im) \ s,
      DifferentiableAt ℂ f x) :
    (∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
      I • (∫ y : ℝ in z.im..w.im, f (re w + y * I)) -
      I • (∫ y : ℝ in z.im..w.im, f (re z + y * I)) = 0

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
z w : ℂ
s : Set ℂ
hs : s.Countable
Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]])
Hd : ∀ x ∈ Ioo (z.re ⊓ w.re) (z.re ⊔ w.re) ×ℂ Ioo (z.im ⊓ w.im) (z.im ⊔ w.im) \ s, DifferentiableAt ℂ f x
⊢ (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * I)) +
        I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) =
    0

Tactic:
refine (integral_boundary_rect_of_hasFDerivAt_real_off_countable f
  (fun z => (fderiv ℂ f z).restrictScalars ℝ) z w s hs Hc
  (fun x hx => (Hd x hx).hasFDerivAt.restrictScalars ℝ) ?_).trans ?_ <;>
    simp [← ContinuousLinearMap.map_smul]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Basic.lean
lemma _root_.nsmul_eq_mul' (a : α) (n : ℕ) : n • a = a * n

Proof state:
case succ
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * ↑n
⊢ (n + 1) • a = a * ↑(n + 1)

Tactic:
rw [succ_nsmul, ih, Nat.cast_succ, mul_add, mul_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
⊢ n • a = a * ↑n

Tactic:
induction n with
| zero => rw [zero_nsmul, Nat.cast_zero, mul_zero]
| succ n ih => rw [succ_nsmul, ih, Nat.cast_succ, mul_add, mul_one]

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
⊢ 0 • a = a * ↑0

Tactic:
rw [zero_nsmul, Nat.cast_zero, mul_zero]

Result:
no goals