harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Process/Stopping.lean
theorem stoppedProcess_eq_of_le {u : ι → Ω → β} {τ : Ω → ι} {i : ι} {ω : Ω} (h : i ≤ τ ω) :
    stoppedProcess u τ i ω = u i ω

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : LinearOrder ι
u : ι → Ω → β
τ : Ω → ι
i : ι
ω : Ω
h : i ≤ τ ω
⊢ stoppedProcess u τ i ω = u i ω

Tactic:
simp [stoppedProcess, min_eq_left h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_mkArray_of_pos (h : p a) :
    find? p (mkArray n a) = if n = 0 then none else some a

Proof state:
α✝ : Type u_1
p : α✝ → Bool
n : Nat
a : α✝
h : p a = true
⊢ find? p (mkArray n a) = if n = 0 then none else some a

Tactic:
simp [find?_mkArray, h]

Result:
no goals
-- Mathlib/SetTheory/Lists.lean
theorem Subset.refl {l : Lists' α true} : l ⊆ l

Proof state:
α : Type u_1
l : Lists' α true
⊢ ofList l.toList ⊆ ofList l.toList

Tactic:
exact ofList_subset (List.Subset.refl _)

Result:
no goals

Proof state:
α : Type u_1
l : Lists' α true
⊢ l ⊆ l

Tactic:
rw [← Lists'.of_toList l]

Result:
α : Type u_1
l : Lists' α true
⊢ ofList l.toList ⊆ ofList l.toList
-- Mathlib/Data/Set/Lattice.lean
theorem sigmaToiUnion_surjective : Surjective (sigmaToiUnion t)
  | ⟨b, hb⟩ =>
    have : ∃ a, b ∈ t a

Proof state:
α : Type u_1
β : Type u_2
t : α → Set β
b : β
hb : b ∈ ⋃ i, t i
⊢ ∃ a, b ∈ t a

Tactic:
simpa using hb

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem DirectSum.coeLinearMap_eq_dfinsupp_sum [DecidableEq σ] [DecidableEq R] [DecidableEq M]
    (x : DirectSum M fun i : M => ↥(weightedHomogeneousSubmodule R w i)) :
    (coeLinearMap fun i : M => weightedHomogeneousSubmodule R w i) x =
      DFinsupp.sum x (fun _ x => ↑x)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
σ : Type u_3
inst✝³ : AddCommMonoid M
w : σ → M
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq R
inst✝ : DecidableEq M
x : ⨁ (i : M), ↥(weightedHomogeneousSubmodule R w i)
⊢ (coeLinearMap fun i => weightedHomogeneousSubmodule R w i) x = DFinsupp.sum x fun x x_1 => ↑x_1

Tactic:
rw [_root_.DirectSum.coeLinearMap_eq_dfinsupp_sum]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
@[to_additive] lemma of_mul_right [Semigroup α] [MulLeftMono α] {a b : α}
    (h : MulLECancellable (a * b)) : MulLECancellable b :=
  fun c d hcd ↦ h <| by rw [mul_assoc, mul_assoc]; exact mul_le_mul_left' hcd _

Proof state:
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : MulLeftMono α
a b : α
h : MulLECancellable (a * b)
c d : α
hcd : b * c ≤ b * d
⊢ a * b * c ≤ a * b * d

Tactic:
rw [mul_assoc, mul_assoc]

Result:
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : MulLeftMono α
a b : α
h : MulLECancellable (a * b)
c d : α
hcd : b * c ≤ b * d
⊢ a * (b * c) ≤ a * (b * d)

Proof state:
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : MulLeftMono α
a b : α
h : MulLECancellable (a * b)
c d : α
hcd : b * c ≤ b * d
⊢ a * (b * c) ≤ a * (b * d)

Tactic:
exact mul_le_mul_left' hcd _

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma lieBracket_smul_right {c : 𝕜} (hW : DifferentiableAt 𝕜 W x) :
    lieBracket 𝕜 V (c • W) x = c • lieBracket 𝕜 V W x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
c : 𝕜
hW : DifferentiableAt 𝕜 W x
⊢ lieBracket 𝕜 V (c • W) x = c • lieBracket 𝕜 V W x

Tactic:
simp only [← differentiableWithinAt_univ, ← lieBracketWithin_univ] at hW ⊢

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
c : 𝕜
hW : DifferentiableWithinAt 𝕜 W univ x
⊢ lieBracketWithin 𝕜 V (c • W) univ x = c • lieBracketWithin 𝕜 V W univ x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
c : 𝕜
hW : DifferentiableWithinAt 𝕜 W univ x
⊢ lieBracketWithin 𝕜 V (c • W) univ x = c • lieBracketWithin 𝕜 V W univ x

Tactic:
exact lieBracketWithin_smul_right hW uniqueDiffWithinAt_univ

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma negMap_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.negMap ⟦P⟧ = ⟦![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1]⟧

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.negMap ⟦P⟧ = ⟦![P x / P z ^ 2, (toAffine W).negY (P x / P z ^ 2) (P y / P z ^ 3), 1]⟧

Tactic:
rw [negMap_eq, neg_of_Z_ne_zero hPz, smul_eq _ <| Ne.isUnit hPz]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
theorem CostructuredArrow.overEquivPresheafCostructuredArrow_functor_map_toOverCompYoneda
    {A : Cᵒᵖ ⥤ Type v} {T : Over A} {X : CostructuredArrow yoneda A}
    (f : yoneda.obj X ⟶ (overEquivPresheafCostructuredArrow A).functor.obj T) :
    (overEquivPresheafCostructuredArrow A).functor.map
      (((CostructuredArrow.toOverCompYoneda A T).inv.app (op X) f)) =
      (CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).hom.app X ≫ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
T : Over A
X : CostructuredArrow yoneda A
f : yoneda.obj X ⟶ (overEquivPresheafCostructuredArrow A).functor.obj T
⊢ (overEquivPresheafCostructuredArrow A).functor.map ((toOverCompYoneda A T).inv.app (op X) f) =
    (toOverCompOverEquivPresheafCostructuredArrow A).hom.app X ≫ f

Tactic:
simp [CostructuredArrow.toOverCompYoneda]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsInfix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <:+: l₂ → l₂ <:+: l₃ → l₁ <:+: l₃
  | l, _, _, ⟨l₁, r₁, rfl⟩, ⟨l₂, r₂, rfl⟩ => ⟨l₂ ++ l₁, r₁ ++ r₂, by simp only [append_assoc]⟩

Proof state:
α : Type u_1
l l₁ r₁ l₂ r₂ : List α
⊢ l₂ ++ l₁ ++ l ++ (r₁ ++ r₂) = l₂ ++ (l₁ ++ l ++ r₁) ++ r₂

Tactic:
simp only [append_assoc]

Result:
no goals
-- Mathlib/InformationTheory/Hamming.lean
theorem hammingDist_lt_one {x y : ∀ i, β i} : hammingDist x y < 1 ↔ x = y

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y : (i : ι) → β i
⊢ hammingDist x y < 1 ↔ x = y

Tactic:
rw [Nat.lt_one_iff, hammingDist_eq_zero]

Result:
no goals
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem dist_div_right [DivInvMonoid M] [PseudoMetricSpace M] [IsometricSMul Mᵐᵒᵖ M]
    (a b c : M) : dist (a / c) (b / c) = dist a b

Proof state:
M : Type u
inst✝² : DivInvMonoid M
inst✝¹ : PseudoMetricSpace M
inst✝ : IsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ dist (a / c) (b / c) = dist a b

Tactic:
simp only [div_eq_mul_inv, dist_mul_right]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma WithBot.lt_toDual_iff {x : WithTop αᵒᵈ} {y : WithBot α} :
    x < y.toDual ↔ y < WithTop.ofDual x

Proof state:
α : Type u_1
inst✝ : LT α
x : WithTop αᵒᵈ
y : WithBot α
⊢ x < WithBot.toDual y ↔ y < WithTop.ofDual x

Tactic:
cases x <;> cases y <;> simp [lt_toDual]

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem preimage_coe_Ioo_top : (some : α → WithTop α) ⁻¹' Ioo a ⊤ = Ioi a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some ⁻¹' Ioo ↑a ⊤ = Ioi a

Tactic:
simp [← Ioi_inter_Iio]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem and_allOnes {x : BitVec w} : x &&& allOnes w = x

Proof state:
w : Nat
x : BitVec w
⊢ x &&& allOnes w = x

Tactic:
ext i h

Result:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (x &&& allOnes w).getLsbD i = x.getLsbD i

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (x &&& allOnes w).getLsbD i = x.getLsbD i

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem iUnion_inter_closedBall_nat (s : Set α) (x : α) : ⋃ n : ℕ, s ∩ closedBall x n = s

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ ⋃ n, s ∩ closedBall x ↑n = s

Tactic:
rw [← inter_iUnion, iUnion_closedBall_nat, inter_univ]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma spanning_iff_ground_subset_closure (hS : S ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
S : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ M.Spanning S ↔ M.E ⊆ M.closure S

Tactic:
rw [spanning_iff_closure_eq, subset_antisymm_iff, and_iff_right (closure_subset_ground _ _)]

Result:
no goals
-- Mathlib/Data/Complex/BigOperators.lean
@[simp]
lemma im_balance [Fintype α] (f : α → ℂ) (a : α) : im (balance f a) = balance (im ∘ f) a

Proof state:
α : Type u_1
inst✝ : Fintype α
f : α → ℂ
a : α
⊢ (balance f a).im = balance (im ∘ f) a

Tactic:
simp [balance]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
theorem Finset.hasProd (s : Finset β) (f : β → α) :
    HasProd (f ∘ (↑) : (↑s : Set β) → α) (∏ b ∈ s, f b)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ HasProd (f ∘ Subtype.val) (∏ b ∈ s, f b)

Tactic:
rw [← prod_attach]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ HasProd (f ∘ Subtype.val) (∏ x ∈ s.attach, f ↑x)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ HasProd (f ∘ Subtype.val) (∏ x ∈ s.attach, f ↑x)

Tactic:
exact hasProd_fintype _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_true_and_eq_false_self : ∀ (b : Bool), (b = true ∧ b = false) ↔ False

Proof state:
⊢ ∀ (b : Bool), b = true ∧ b = false ↔ False

Tactic:
decide

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma coe_norm_smul_basis (p q : R[X]) :
    Algebra.norm R[X] (p • (1 : W.CoordinateRing) + q • mk W Y) =
      mk W ((C p + C q * X) * (C p + C q * (-(Y : R[X][Y]) - C (C W.a₁ * X + C W.a₃)))) :=
  AdjoinRoot.mk_eq_mk.mpr
    ⟨C q ^ 2, by simp only [norm_smul_basis, polynomial]; C_simp; ring1⟩

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
⊢ C p ^ 2 - C p * C q * (C (C W.a₁) * C X + C (C W.a₃)) -
        C q ^ 2 * (C X ^ 3 + C (C W.a₂) * C X ^ 2 + C (C W.a₄) * C X + C (C W.a₆)) -
      (C p + C q * Y) * (C p + C q * (-Y - (C (C W.a₁) * C X + C (C W.a₃)))) =
    (Y ^ 2 + (C (C W.a₁) * C X + C (C W.a₃)) * Y - (C X ^ 3 + C (C W.a₂) * C X ^ 2 + C (C W.a₄) * C X + C (C W.a₆))) *
      C q ^ 2

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
⊢ C (p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) -
      (C p + C q * Y) * (C p + C q * (-Y - C (C W.a₁ * X + C W.a₃))) =
    (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) * C q ^ 2

Tactic:
C_simp

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
⊢ C p ^ 2 - C p * C q * (C (C W.a₁) * C X + C (C W.a₃)) -
        C q ^ 2 * (C X ^ 3 + C (C W.a₂) * C X ^ 2 + C (C W.a₄) * C X + C (C W.a₆)) -
      (C p + C q * Y) * (C p + C q * (-Y - (C (C W.a₁) * C X + C (C W.a₃)))) =
    (Y ^ 2 + (C (C W.a₁) * C X + C (C W.a₃)) * Y - (C X ^ 3 + C (C W.a₂) * C X ^ 2 + C (C W.a₄) * C X + C (C W.a₆))) *
      C q ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
⊢ C ((Algebra.norm R[X]) (p • 1 + q • (mk W) Y)) - (C p + C q * Y) * (C p + C q * (-Y - C (C W.a₁ * X + C W.a₃))) =
    W.polynomial * C q ^ 2

Tactic:
simp only [norm_smul_basis, polynomial]

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
p q : R[X]
⊢ C (p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) -
      (C p + C q * Y) * (C p + C q * (-Y - C (C W.a₁ * X + C W.a₃))) =
    (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) * C q ^ 2
-- Mathlib/Computability/TuringMachine.lean
theorem stmts_supportsStmt {M : Λ → Stmt Γ Λ σ} {S : Finset Λ} {q : Stmt Γ Λ σ}
    (ss : Supports M S) : some q ∈ stmts M S → SupportsStmt S q

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : Inhabited Λ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q : Stmt Γ Λ σ
ss : Supports M S
⊢ ∀ x ∈ S, q ∈ stmts₁ (M x) → SupportsStmt S q

Tactic:
exact fun l ls h ↦ stmts₁_supportsStmt_mono h (ss.2 _ ls)

Result:
no goals

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : Inhabited Λ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q : Stmt Γ Λ σ
ss : Supports M S
⊢ some q ∈ stmts M S → SupportsStmt S q

Tactic:
simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
  forall_eq', exists_imp, and_imp]

Result:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : Inhabited Λ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q : Stmt Γ Λ σ
ss : Supports M S
⊢ ∀ x ∈ S, q ∈ stmts₁ (M x) → SupportsStmt S q
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem leadingCoeff_C_mul_X (a : R) : leadingCoeff (C a * X) = a

Proof state:
R : Type u
inst✝ : Semiring R
a : R
⊢ (C a * X).leadingCoeff = a

Tactic:
simpa only [pow_one] using leadingCoeff_C_mul_X_pow a 1

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem IsUniformInducing.isUniformInducing_comp_iff {f : α → β} {g : β → γ}
    (hg : IsUniformInducing g) : IsUniformInducing (g ∘ f) ↔ IsUniformInducing f

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : IsUniformInducing g
⊢ IsUniformInducing (g ∘ f) ↔ IsUniformInducing f

Tactic:
simp only [isUniformInducing_iff, ← hg.comap_uniformity, comap_comap, Function.comp_def]

Result:
no goals
-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma restrict_equiv (f : X.PartialMap Y) (U : X.Opens)
    (hU : Dense (U : Set X)) (hU' : U ≤ f.domain) : (f.restrict U hU hU').equiv f :=
  ⟨U, hU, le_rfl, hU', by simp⟩

Proof state:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
⊢ ((f.restrict U hU hU').restrict U hU ⋯).hom = (f.restrict U hU hU').hom

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
/-- A fixed block is a block. -/
@[to_additive "A fixed block is a block."]
lemma IsFixedBlock.isBlock (hfB : IsFixedBlock G B) : IsBlock G B

Proof state:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
hfB : IsFixedBlock G B
⊢ IsBlock G B

Tactic:
simp [IsBlock, hfB _]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem exists_and_right : (∃ x, p x ∧ b) ↔ (∃ x, p x) ∧ b

Proof state:
α : Sort u_1
p : α → Prop
b : Prop
⊢ (∃ x, p x ∧ b) ↔ (∃ x, p x) ∧ b

Tactic:
simp [And.comm]

Result:
no goals
-- Mathlib/Data/Fintype/Pi.lean
lemma piFinset_update_singleton_eq_filter_piFinset_eq (s : ∀ i, Finset (δ i)) (i : α) {a : δ i}
    (ha : a ∈ s i) :
    piFinset (Function.update s i {a}) = {f ∈ piFinset s | f i = a}

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
s : (i : α) → Finset (δ i)
i : α
a : δ i
ha : a ∈ s i
⊢ piFinset (update s i {a}) = filter (fun f => f i = a) (piFinset s)

Tactic:
simp [piFinset_update_eq_filter_piFinset_mem, ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.ro_ro (u w v k₁ k₂ : Nat) : u ≤ w + k₁ → w ≤ v + k₂ → u ≤ v + (k₁ + k₂)

Proof state:
u w v k₁ k₂ : Nat
⊢ u ≤ w + k₁ → w ≤ v + k₂ → u ≤ v + (k₁ + k₂)

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem mul_self_sqrt (h : 0 ≤ x) : √x * √x = x

Proof state:
x : ℝ
h : 0 ≤ x
⊢ √x * √x = x

Tactic:
rw [Real.sqrt, ← NNReal.coe_mul, NNReal.mul_self_sqrt, Real.coe_toNNReal _ h]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem mem_sInf {S : Set (NonUnitalStarSubalgebra R A)} {x : A} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
S : Set (NonUnitalStarSubalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

Result:
no goals
-- Mathlib/Topology/Exterior.lean
@[simp] lemma nhdsSet_exterior (s : Set X) : 𝓝ˢ (exterior s) = 𝓝ˢ s

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ 𝓝ˢ (exterior s) = 𝓝ˢ s

Tactic:
refine le_antisymm ((hasBasis_nhdsSet _).ge_iff.2 ?_) (nhdsSet_mono subset_exterior)

Result:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ ∀ (i' : Set X), IsOpen i' ∧ s ⊆ i' → i' ∈ 𝓝ˢ (exterior s)

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ ∀ (i' : Set X), IsOpen i' ∧ s ⊆ i' → i' ∈ 𝓝ˢ (exterior s)

Tactic:
exact fun U ⟨hUo, hsU⟩ ↦ hUo.mem_nhdsSet.2 <| hUo.exterior_subset.2 hsU

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
lemma mem_fromIdeal {I : Ideal R} {x : R} :
    x ∈ fromIdeal I ↔ x ∈ span I

Proof state:
R : Type u_1
inst✝ : Ring R
I : Ideal R
x : R
⊢ x ∈ fromIdeal I ↔ x ∈ span ↑I

Tactic:
simp [fromIdeal]

Result:
no goals
-- Mathlib/Analysis/Complex/CauchyIntegral.lean
theorem circleIntegral_sub_inv_smul_of_differentiable_on_off_countable {R : ℝ} {c w : ℂ} {f : ℂ → E}
    {s : Set ℂ} (hs : s.Countable) (hw : w ∈ ball c R) (hc : ContinuousOn f (closedBall c R))
    (hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x) :
    (∮ z in C(c, R), (z - w)⁻¹ • f z) = (2 * π * I : ℂ) • f w

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
⊢ (∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z) = (2 * ↑π * I) • f w

Tactic:
rw [← two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
  hs hw hc hd, smul_inv_smul₀]

Result:
case ha
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
⊢ 2 * ↑π * I ≠ 0

Proof state:
case ha
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
R : ℝ
c w : ℂ
f : ℂ → E
s : Set ℂ
hs : s.Countable
hw : w ∈ ball c R
hc : ContinuousOn f (closedBall c R)
hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x
⊢ 2 * ↑π * I ≠ 0

Tactic:
simp [Real.pi_ne_zero, I_ne_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
lemma swap_comm (i j : n) :
    swap R i j = swap R j i

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Zero R
inst✝¹ : One R
inst✝ : DecidableEq n
i j : n
⊢ swap R i j = swap R j i

Tactic:
simp only [swap, Equiv.swap_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_alter_eq_isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α}
    {f : Option β → Option β} (h : m.WF) :
    (Const.alter m k f).isEmpty = ((m.erase k).isEmpty && (f (Const.get? m k)).isNone)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
h : m.WF
⊢ (alter m k f).isEmpty = ((m.erase k).isEmpty && (f (get? m k)).isNone)

Tactic:
simp_to_raw using Raw₀.Const.isEmpty_alter_eq_isEmpty_erase

Result:
no goals
-- Mathlib/Algebra/Lie/Quotient.lean
theorem range_mk' : LieModuleHom.range (mk' N) = ⊤

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
N : LieSubmodule R L M
inst✝¹ : LieAlgebra R L
inst✝ : LieModule R L M
⊢ (mk' N).range = ⊤

Tactic:
simp [LieModuleHom.range_eq_top]

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
lemma wInner_cWeight_eq_expect (f g : ∀ i, E i) : ⟪f, g⟫ₙ_[𝕜] = 𝔼 i, inner (f i) (g i)

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
f g : (i : ι) → E i
⊢ wInner cWeight f g = 𝔼 i : ι, inner (f i) (g i)

Tactic:
simp [wInner, expect, smul_sum, ← NNRat.cast_smul_eq_nnqsmul ℝ]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
lemma pmul_assoc [CommMonoidWithZero R] (f₁ f₂ f₃ : ArithmeticFunction R) :
    pmul (pmul f₁ f₂) f₃ = pmul f₁ (pmul f₂ f₃)

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
f₁ f₂ f₃ : ArithmeticFunction R
⊢ (f₁.pmul f₂).pmul f₃ = f₁.pmul (f₂.pmul f₃)

Tactic:
ext

Result:
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
f₁ f₂ f₃ : ArithmeticFunction R
x✝ : ℕ
⊢ ((f₁.pmul f₂).pmul f₃) x✝ = (f₁.pmul (f₂.pmul f₃)) x✝

Proof state:
case h
R : Type u_1
inst✝ : CommMonoidWithZero R
f₁ f₂ f₃ : ArithmeticFunction R
x✝ : ℕ
⊢ ((f₁.pmul f₂).pmul f₃) x✝ = (f₁.pmul (f₂.pmul f₃)) x✝

Tactic:
simp only [pmul_apply, mul_assoc]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem HasMFDerivWithinAt.mul' (hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p')
    (hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q') :
    HasMFDerivWithinAt I 𝓘(𝕜, F') (p * q) s z (p z • q' + p'.smulRight (q z) : E →L[𝕜] F') :=
  ⟨hp.1.mul hq.1, by simpa only [mfld_simps] using hp.2.mul' hq.2⟩

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
z : M
F' : Type u_21
inst✝¹ : NormedRing F'
inst✝ : NormedAlgebra 𝕜 F'
p q : M → F'
p' q' : TangentSpace I z →L[𝕜] F'
hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'
hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q'
⊢ HasFDerivWithinAt (writtenInExtChartAt I 𝓘(𝕜, F') z (p * q)) (p z • q' + p'.smulRight (q z))
    (↑(extChartAt I z).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I z) z)

Tactic:
simpa only [mfld_simps] using hp.2.mul' hq.2

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem toList_pow_apply_eq_rotate (p : Perm α) (x : α) (k : ℕ) :
    p.toList ((p ^ k) x) = (p.toList x).rotate k

Proof state:
case hl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k : ℕ
⊢ (p.toList ((p ^ k) x)).length = ((p.toList x).rotate k).length

Tactic:
simp only [length_toList, cycleOf_self_apply_pow, length_rotate]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k : ℕ
⊢ p.toList ((p ^ k) x) = (p.toList x).rotate k

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k : ℕ
⊢ (p.toList ((p ^ k) x)).length = ((p.toList x).rotate k).length

case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k : ℕ
⊢ ∀ (i : ℕ) (h₁ : i < (p.toList ((p ^ k) x)).length) (h₂ : i < ((p.toList x).rotate k).length),
    (p.toList ((p ^ k) x))[i] = ((p.toList x).rotate k)[i]

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k n : ℕ
hn : n < (p.toList ((p ^ k) x)).length
hn' : n < ((p.toList x).rotate k).length
⊢ (p.toList ((p ^ k) x))[n] = ((p.toList x).rotate k)[n]

Tactic:
rw [getElem_toList, getElem_rotate, getElem_toList, length_toList,
  pow_mod_card_support_cycleOf_self_apply, pow_add, mul_apply]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k : ℕ
⊢ ∀ (i : ℕ) (h₁ : i < (p.toList ((p ^ k) x)).length) (h₂ : i < ((p.toList x).rotate k).length),
    (p.toList ((p ^ k) x))[i] = ((p.toList x).rotate k)[i]

Tactic:
intro n hn hn'

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
k n : ℕ
hn : n < (p.toList ((p ^ k) x)).length
hn' : n < ((p.toList x).rotate k).length
⊢ (p.toList ((p ^ k) x))[n] = ((p.toList x).rotate k)[n]