harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Bases.lean
lemma IsTopologicalBasis.eq_of_forall_subset_iff {t : Set α} (hB : IsTopologicalBasis B)
    (hs : IsOpen s) (ht : IsOpen t) (h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t) : s = t

Proof state:
α : Type u
t✝ : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen s
ht : IsOpen t
h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t
⊢ s = t

Tactic:
rw [hB.open_eq_sUnion' hs, hB.open_eq_sUnion' ht]

Result:
α : Type u
t✝ : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen s
ht : IsOpen t
h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t
⊢ ⋃₀ {s_1 | s_1 ∈ B ∧ s_1 ⊆ s} = ⋃₀ {s | s ∈ B ∧ s ⊆ t}

Proof state:
α : Type u
t✝ : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen s
ht : IsOpen t
h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t
⊢ ⋃₀ {s_1 | s_1 ∈ B ∧ s_1 ⊆ s} = ⋃₀ {s | s ∈ B ∧ s ⊆ t}

Tactic:
exact congr_arg _ (Set.ext fun U ↦ and_congr_right <| h _)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_eq_of_eq_det_one_mul {A B : Matrix n n R} (C : Matrix n n R) (hC : det C = 1)
    (hA : A = C * B) : det A = det B :=
  calc
    det A = det (C * B) := congr_arg _ hA
    _ = det C * det B := det_mul _ _
    _ = det B

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A B C : Matrix n n R
hC : C.det = 1
hA : A = C * B
⊢ C.det * B.det = B.det

Tactic:
rw [hC, one_mul]

Result:
no goals
-- Mathlib/GroupTheory/Perm/ClosureSwap.lean
theorem Equiv.Perm.IsSwap.finite_compl_fixedBy {σ : Perm α} (h : σ.IsSwap) :
    (fixedBy α σ)ᶜ.Finite

Proof state:
α : Type u_2
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsSwap
⊢ (fixedBy α σ)ᶜ.Finite

Tactic:
obtain ⟨x, y, -, rfl⟩ := h

Result:
case intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
x y : α
⊢ (fixedBy α (swap x y))ᶜ.Finite

Proof state:
case intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
x y : α
⊢ (fixedBy α (swap x y))ᶜ.Finite

Tactic:
exact finite_compl_fixedBy_swap

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem hasLineDerivAt_iff_tendsto_slope_zero :
    HasLineDerivAt 𝕜 f f' x v ↔
      Tendsto (fun (t : 𝕜) ↦ t⁻¹ • (f (x + t • v) - f x)) (𝓝[≠] 0) (𝓝 f')

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
f' : F
x v : E
⊢ HasLineDerivAt 𝕜 f f' x v ↔ Tendsto (fun t => t⁻¹ • (f (x + t • v) - f x)) (𝓝[≠] 0) (𝓝 f')

Tactic:
simp only [HasLineDerivAt, hasDerivAt_iff_tendsto_slope_zero, zero_add,
  zero_smul, add_zero]

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem neg_one_lt_goldConj : -1 < ψ

Proof state:
⊢ φ⁻¹ < 1

Tactic:
exact inv_lt_one_of_one_lt₀ one_lt_gold

Result:
no goals

Proof state:
⊢ -1 < ψ

Tactic:
rw [neg_lt, ← inv_gold]

Result:
⊢ φ⁻¹ < 1
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem dist : LipschitzWith 2 (Function.uncurry <| @dist α _)

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ LipschitzWith 2 (uncurry dist)

Tactic:
rw [← one_add_one_eq_two]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ LipschitzWith (1 + 1) (uncurry dist)

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ LipschitzWith (1 + 1) (uncurry dist)

Tactic:
exact LipschitzWith.uncurry LipschitzWith.dist_left LipschitzWith.dist_right

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem append_copy_copy {u v w u' v' w'} (p : G.Walk u v) (q : G.Walk v w)
    (hu : u = u') (hv : v = v') (hw : w = w') :
    (p.copy hu hv).append (q.copy hv hw) = (p.append q).copy hu hw

Proof state:
V : Type u
G : SimpleGraph V
u' v' w' : V
p : G.Walk u' v'
q : G.Walk v' w'
⊢ (p.copy ⋯ ⋯).append (q.copy ⋯ ⋯) = (p.append q).copy ⋯ ⋯

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w u' v' w' : V
p : G.Walk u v
q : G.Walk v w
hu : u = u'
hv : v = v'
hw : w = w'
⊢ (p.copy hu hv).append (q.copy hv hw) = (p.append q).copy hu hw

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
u' v' w' : V
p : G.Walk u' v'
q : G.Walk v' w'
⊢ (p.copy ⋯ ⋯).append (q.copy ⋯ ⋯) = (p.append q).copy ⋯ ⋯
-- Mathlib/Topology/GDelta/Basic.lean
/-- If a set `s` is nowhere dense, so is its closure. -/
protected lemma IsNowhereDense.closure {s : Set X} (hs : IsNowhereDense s) :
    IsNowhereDense (closure s)

Proof state:
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
hs : IsNowhereDense s
⊢ IsNowhereDense (closure s)

Tactic:
rwa [IsNowhereDense, closure_closure]

Result:
no goals
-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem trinomial_leading_coeff' (hkm : k < m) (hmn : m < n) :
    (trinomial k m n u v w).coeff n = w

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
⊢ (trinomial k m n u v w).coeff n = w

Tactic:
rw [trinomial_def, coeff_add, coeff_add, coeff_C_mul_X_pow, coeff_C_mul_X_pow, coeff_C_mul_X_pow,
  if_neg (hkm.trans hmn).ne', if_neg hmn.ne', if_pos rfl, zero_add, zero_add]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem mul_pos_of_neg_of_neg [ExistsAddOfLE α] [MulPosStrictMono α]
    [AddRightStrictMono α] [AddRightReflectLT α]
    {a b : α} (ha : a < 0) (hb : b < 0) : 0 < a * b

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
a b : α
ha : a < 0
hb : b < 0
⊢ 0 < a * b

Tactic:
simpa only [zero_mul] using mul_lt_mul_of_neg_right ha hb

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem prod_cons (i) (m : M i) (w : Word M) (h1 : m ≠ 1) (h2 : w.fstIdx ≠ some i) :
    prod (cons m w h2 h1) = of m * prod w

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
m : M i
w : Word M
h1 : m ≠ 1
h2 : w.fstIdx ≠ some i
⊢ (cons m w h2 h1).prod = of m * w.prod

Tactic:
simp [cons, prod, List.map_cons, List.prod_cons]

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem mem_centralizer_iff {s : Set A} {z : A} :
    z ∈ centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
s : Set A
z : A
⊢ z ∈ centralizer R s ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g

Tactic:
simp [← SetLike.mem_coe, centralizer_union, ← image_star, mem_centralizer_iff, forall_and]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem finrank_directSum {ι : Type v} [Fintype ι] (M : ι → Type w) [∀ i : ι, AddCommMonoid (M i)]
    [∀ i : ι, Module R (M i)] [∀ i : ι, Module.Free R (M i)] [∀ i : ι, Module.Finite R (M i)] :
    finrank R (⨁ i, M i) = ∑ i, finrank R (M i)

Proof state:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : StrongRankCondition R
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ finrank R (⨁ (i : ι), M i) = ∑ i : ι, finrank R (M i)

Tactic:
simp only [finrank, fun i => rank_eq_card_chooseBasisIndex R (M i), rank_directSum, ← mk_sigma,
  mk_toNat_eq_card, card_sigma]

Result:
no goals

Proof state:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : StrongRankCondition R
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
⊢ finrank R (⨁ (i : ι), M i) = ∑ i : ι, finrank R (M i)

Tactic:
letI := nontrivial_of_invariantBasisNumber R

Result:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : StrongRankCondition R
ι : Type v
inst✝⁴ : Fintype ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Free R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
this : Nontrivial R := nontrivial_of_invariantBasisNumber R
⊢ finrank R (⨁ (i : ι), M i) = ∑ i : ι, finrank R (M i)
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem vectorSpan_eq_top_of_affineSpan_eq_top {s : Set P} (h : affineSpan k s = ⊤) :
    vectorSpan k s = ⊤

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h : affineSpan k s = ⊤
⊢ vectorSpan k s = ⊤

Tactic:
rw [← direction_affineSpan, h, direction_top]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_add_right (x y y' : M) : polar Q x (y + y') = polar Q x y + polar Q x y'

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x y y' : M
⊢ polar (⇑Q) x (y + y') = polar (⇑Q) x y + polar (⇑Q) x y'

Tactic:
rw [polar_comm Q x, polar_comm Q x, polar_comm Q x, polar_add_left]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_smul_ofReal_right (x y : F) {t : ℝ} : ⟪x, (t : 𝕜) • y⟫ = ⟪x, y⟫ * t

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ ⟪x, ↑t • y⟫_𝕜 = ⟪x, y⟫_𝕜 * ↑t

Tactic:
rw [inner_smul_right, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_eq_filterMap_iff {f : α → Option β} :
    L₁ ++ L₂ = filterMap f l ↔
      ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Proof state:
α : Type u_1
β : Type u_2
L₁ L₂ : Array β
l : Array α
f : α → Option β
⊢ L₁ ++ L₂ = filterMap f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ filterMap f l₁ = L₁ ∧ filterMap f l₂ = L₂

Tactic:
rw [eq_comm, filterMap_eq_append_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma neg_of_Z_eq_zero [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.neg P = -P y • ![0, 1, 0]

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.neg P = -P y • ![0, 1, 0]

Tactic:
erw [neg, X_eq_zero_of_Z_eq_zero hP hPz, negY_of_Z_eq_zero hP hPz, hPz, smul_fin3, mul_zero,
  mul_one]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
theorem isAcyclic_iff_forall_edge_isBridge :
    G.IsAcyclic ↔ ∀ ⦃e⦄, e ∈ (G.edgeSet) → G.IsBridge e

Proof state:
V : Type u
G : SimpleGraph V
⊢ G.IsAcyclic ↔ ∀ ⦃e : Sym2 V⦄, e ∈ G.edgeSet → G.IsBridge e

Tactic:
simp [isAcyclic_iff_forall_adj_isBridge, Sym2.forall]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem All.setRed {t : RBNode α} (h : t.All p) : (setRed t).All p

Proof state:
α : Type u_1
p : α → Prop
t : RBNode α
h : All p t
⊢ All p t.setRed

Tactic:
unfold setRed

Result:
α : Type u_1
p : α → Prop
t : RBNode α
h : All p t
⊢ All p
    (match t with
    | node c a v b => node red a v b
    | nil => nil)

Proof state:
α : Type u_1
p : α → Prop
t : RBNode α
h : All p t
⊢ All p
    (match t with
    | node c a v b => node red a v b
    | nil => nil)

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
lemma sum_mul_boole (s : Finset ι) (f : ι → α) (i : ι) :
    ∑ j ∈ s, f j * ite (i = j) 1 0 = ite (i ∈ s) (f i) 0

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : ι
⊢ (∑ j ∈ s, f j * if i = j then 1 else 0) = if i ∈ s then f i else 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem filter_apply_pos [∀ i, Zero (β i)] {p : ι → Prop} [DecidablePred p] (f : Π₀ i, β i) {i : ι}
    (h : p i) : f.filter p i = f i

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : ι
h : p i
⊢ (filter p f) i = f i

Tactic:
simp only [filter_apply, if_pos h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lintegral_eq_lmarginal_univ [Fintype δ] {f : (∀ i, π i) → ℝ≥0∞} (x : ∀ i, π i) :
    ∫⁻ x, f x ∂Measure.pi μ = (∫⋯∫⁻_univ, f ∂μ) x

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝³ : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
f : ((i : δ) → π i) → ℝ≥0∞
x : (i : δ) → π i
⊢ ∫⁻ (x : (i : δ) → π i), f x ∂Measure.pi μ = (∫⋯∫⁻_Finset.univ, f ∂μ) x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldl_map_hom (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
    (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
    (l.map g).foldl f' (g a) = g (l.foldl f a)

Proof state:
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
a : α
l : List α
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
⊢ foldl f' (g a) (map g l) = g (foldl f a l)

Tactic:
induction l generalizing a

Result:
case nil
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
a : α
⊢ foldl f' (g a) (map g []) = g (foldl f a [])

case cons
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (a : α), foldl f' (g a) (map g tail✝) = g (foldl f a tail✝)
a : α
⊢ foldl f' (g a) (map g (head✝ :: tail✝)) = g (foldl f a (head✝ :: tail✝))

Proof state:
case nil
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
a : α
⊢ foldl f' (g a) (map g []) = g (foldl f a [])

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
g : α → β
f : α → α → α
f' : β → β → β
h : ∀ (x y : α), f' (g x) (g y) = g (f x y)
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (a : α), foldl f' (g a) (map g tail✝) = g (foldl f a tail✝)
a : α
⊢ foldl f' (g a) (map g (head✝ :: tail✝)) = g (foldl f a (head✝ :: tail✝))

Tactic:
simp [*, h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblXYZ_of_Y_eq' [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 = Q y * P z ^ 3)
    (hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3) :
    W'.dblXYZ P = ![W'.dblU P ^ 2, W'.dblU P ^ 3, 0]

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ W'.dblXYZ P = ![W'.dblU P ^ 2, W'.dblU P ^ 3, 0]

Tactic:
rw [dblXYZ, dblX_of_Y_eq hQz hx hy hy', dblY_of_Y_eq hQz hx hy hy', dblZ_of_Y_eq hQz hx hy hy']

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
protected lemma existsUnique_congr_right : (∃! a, q (e a)) ↔ ∃! b, q b :=
  e.exists_congr <| by simpa using fun _ _ ↦ e.forall_congr (by simp)

Proof state:
α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
⊢ ∀ (a : α),
    ((fun a => q (e a)) a ∧ ∀ (y : α), (fun a => q (e a)) y → y = a) ↔
      (fun b => q b) (e a) ∧ ∀ (y : β), (fun b => q b) y → y = e a

Tactic:
simpa using fun _ _ ↦ e.forall_congr (by simp)

Result:
no goals

Proof state:
α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
x✝¹ : α
x✝ : q (e x✝¹)
⊢ ∀ (a : α), q (e a) → a = x✝¹ ↔ q (e a) → e a = e x✝¹

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendsto_prod_top_iff {c : β} :
    Tendsto (↿F) (p ×ˢ ⊤) (𝓝 c) ↔ TendstoUniformly F (fun _ => c) p

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
c : β
⊢ Tendsto (↿F) (p ×ˢ ⊤) (𝓝 c) ↔ TendstoUniformly F (fun x => c) p

Tactic:
rw [tendstoUniformly_iff_tendstoUniformlyOnFilter]

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
c : β
⊢ Tendsto (↿F) (p ×ˢ ⊤) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun x => c) p ⊤

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
c : β
⊢ Tendsto (↿F) (p ×ˢ ⊤) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun x => c) p ⊤

Tactic:
exact tendsto_prod_filter_iff

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem findSomeRev?_eq_findSome?_reverse (f : α → Option β) (as : Vector α n) :
    findSomeRev? f as = findSome? f as.reverse

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
as : Vector α n
⊢ findSomeRev? f as = findSome? f as.reverse

Tactic:
simp [findSomeRev?, findSome?]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem liftRel_think_left (R : α → β → Prop) (s t) : LiftRel R (think s) t ↔ LiftRel R s t

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ LiftRel R s.think t ↔ LiftRel R s t

Tactic:
rw [liftRel_destruct_iff, liftRel_destruct_iff]

Result:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.think.destruct t.destruct ↔
    Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.think.destruct t.destruct ↔
    Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem mem_of_mem_odd (a : α) (s : Stream' α) : a ∈ odd s → a ∈ s := fun ⟨n, h⟩ =>
  Exists.intro (2 * n + 1) (by rw [h, get_odd])

Proof state:
α : Type u
a : α
s : Stream' α
x✝ : a ∈ s.odd
n : ℕ
h : (fun b => a = b) (s.odd.get n)
⊢ (fun b => a = b) (s.get (2 * n + 1))

Tactic:
rw [h, get_odd]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem moebius_apply_prime {p : ℕ} (hp : p.Prime) : μ p = -1

Proof state:
p : ℕ
hp : Nat.Prime p
⊢ μ p = -1

Tactic:
rw [moebius_apply_of_squarefree hp.squarefree, cardFactors_apply_prime hp, pow_one]

Result:
no goals
-- Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean
theorem smul_prod
    [CommMonoid β] [Monoid α] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β]
    (s : Finset β) (b : α) (f : β → β) :
    b ^ s.card • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid β
inst✝³ : Monoid α
inst✝² : MulAction α β
inst✝¹ : IsScalarTower α β β
inst✝ : SMulCommClass α β β
s : Finset β
b : α
f : β → β
⊢ Multiset.map (fun x => b • f x) s.val = Multiset.map (fun x => b • x) (Multiset.map f s.val)

Tactic:
simp only [Multiset.map_map, Function.comp_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid β
inst✝³ : Monoid α
inst✝² : MulAction α β
inst✝¹ : IsScalarTower α β β
inst✝ : SMulCommClass α β β
s : Finset β
b : α
f : β → β
⊢ b ^ #s • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x

Tactic:
have : Multiset.map (fun (x : β) ↦ b • f x) s.val =
    Multiset.map (fun x ↦ b • x) (Multiset.map f s.val) := by
  simp only [Multiset.map_map, Function.comp_apply]

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid β
inst✝³ : Monoid α
inst✝² : MulAction α β
inst✝¹ : IsScalarTower α β β
inst✝ : SMulCommClass α β β
s : Finset β
b : α
f : β → β
this : Multiset.map (fun x => b • f x) s.val = Multiset.map (fun x => b • x) (Multiset.map f s.val)
⊢ b ^ #s • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid β
inst✝³ : Monoid α
inst✝² : MulAction α β
inst✝¹ : IsScalarTower α β β
inst✝ : SMulCommClass α β β
s : Finset β
b : α
f : β → β
this : Multiset.map (fun x => b • f x) s.val = Multiset.map (fun x => b • x) (Multiset.map f s.val)
⊢ b ^ #s • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x

Tactic:
simp_rw [prod_eq_multiset_prod, card_def, this, ← Multiset.smul_prod _ b, Multiset.card_map]

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem add_modEq_right : a + n ≡ a [ZMOD n] := ModEq.symm <| modEq_iff_dvd.2 <| by simp

Proof state:
n a : ℤ
⊢ n ∣ a + n - a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem iff_and_self : ∀ {a b : Bool}, (b = (a && b)) ↔ (b → a)

Proof state:
⊢ ∀ {a b : Bool}, b = (a && b) ↔ b = true → a = true

Tactic:
decide

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
lemma le_sdiff_iff : a ≤ b \ c ↔ ∀ d, b ≤ c ⊔ d → a ≤ d

Proof state:
α : Type u
inst✝ : Coframe α
a b c : α
⊢ a ≤ b \ c ↔ ∀ (d : α), b ≤ c ⊔ d → a ≤ d

Tactic:
simp [sdiff_eq_sInf]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem abs_integral_le_integral_abs (hab : a ≤ b) :
    |∫ x in a..b, f x ∂μ| ≤ ∫ x in a..b, |f x| ∂μ

Proof state:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
⊢ |∫ (x : ℝ) in a..b, f x ∂μ| ≤ ∫ (x : ℝ) in a..b, |f x| ∂μ

Tactic:
simpa only [← Real.norm_eq_abs] using norm_integral_le_integral_norm hab

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
    m.1.size ≤ (m.erase k).1.size + 1

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
⊢ m.val.size ≤ (m.erase k).val.size + 1

Tactic:
simp_to_model [erase] using List.length_le_length_eraseKey

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem not_any_eq_all_not (l : List α) (p : α → Bool) : (!l.any p) = l.all fun a => !p a

Proof state:
α : Type u_1
l : List α
p : α → Bool
⊢ (!l.any p) = l.all fun a => !p a

Tactic:
induction l with simp | cons _ _ ih => rw [ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
ih : (!tail✝.any p) = tail✝.all fun a => !p a
⊢ (!p head✝ && !tail✝.any p) = (!p head✝ && tail✝.all fun a => !p a)

Tactic:
rw [ih]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem augment_hom_zero (X : SimplicialObject C) (X₀ : C) (f : X _⦋0⦌ ⟶ X₀) (w) :
    (X.augment X₀ f w).hom.app (op ⦋0⦌) = f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
⊢ (X.augment X₀ f w).hom.app (op ⦋0⦌) = f

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_self_ofReal_norm (x : E) : (‖⟪x, x⟫‖ : 𝕜) = ⟪x, x⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ↑(re ⟪x, x⟫_𝕜) = ⟪x, x⟫_𝕜

Tactic:
exact inner_self_ofReal_re _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ↑‖⟪x, x⟫_𝕜‖ = ⟪x, x⟫_𝕜

Tactic:
rw [← inner_self_re_eq_norm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E
⊢ ↑(re ⟪x, x⟫_𝕜) = ⟪x, x⟫_𝕜
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem isMaximal_comap_iff_of_bijective : IsMaximal (comap f K) ↔ IsMaximal K

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
hf : Function.Bijective ⇑f
K : Ideal S
⊢ (comap f K).IsMaximal ↔ K.IsMaximal

Tactic:
simpa only [isMaximal_def] using (relIsoOfBijective _ hf).isCoatom_iff _

Result:
no goals
-- Mathlib/RingTheory/RingHom/FiniteType.lean
theorem finiteType_stableUnderComposition : StableUnderComposition @FiniteType

Proof state:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FiniteType
hg : g.FiniteType
⊢ (g.comp f).FiniteType

Tactic:
exact hg.comp hf

Result:
no goals

Proof state:
⊢ StableUnderComposition @FiniteType

Tactic:
introv R hf hg

Result:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FiniteType
hg : g.FiniteType
⊢ (g.comp f).FiniteType