harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/AEDisjoint.lean
theorem iUnion_right_iff {ι : Sort*} [Countable ι] {t : ι → Set α} :
    AEDisjoint μ s (⋃ i, t i) ↔ ∀ i, AEDisjoint μ s (t i)

Proof state:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set α
ι : Sort u_3
inst✝ : Countable ι
t : ι → Set α
⊢ AEDisjoint μ s (⋃ i, t i) ↔ ∀ (i : ι), AEDisjoint μ s (t i)

Tactic:
simp only [AEDisjoint, inter_iUnion, measure_iUnion_null_iff]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem sum_fiberwise {α M} [AddCommMonoid M] (π : Prepartition I) (f : Box ι → α) (g : Box ι → M) :
    (∑ y ∈ π.boxes.image f, ∑ J ∈ (π.filter fun J => f J = y).boxes, g J) =
      ∑ J ∈ π.boxes, g J

Proof state:
ι : Type u_1
I : Box ι
α : Type u_2
M : Type u_3
inst✝ : AddCommMonoid M
π : Prepartition I
f : Box ι → α
g : Box ι → M
⊢ ∑ y ∈ Finset.image f π.boxes, ∑ J ∈ (π.filter fun J => f J = y).boxes, g J = ∑ J ∈ π.boxes, g J

Tactic:
convert sum_fiberwise_of_maps_to (fun _ => Finset.mem_image_of_mem f) g

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem geom_mean_le_arith_mean2_weighted (w₁ w₂ p₁ p₂ : ℝ≥0) :
    w₁ + w₂ = 1 → p₁ ^ (w₁ : ℝ) * p₂ ^ (w₂ : ℝ) ≤ w₁ * p₁ + w₂ * p₂

Proof state:
w₁ w₂ p₁ p₂ : ℝ≥0
⊢ w₁ + w₂ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ ≤ w₁ * p₁ + w₂ * p₂

Tactic:
simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty,
  Finset.univ_eq_empty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one] using
  geom_mean_le_arith_mean_weighted univ ![w₁, w₂] ![p₁, p₂]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
lemma cfcHom_nnreal_eq_restrict {a : A} (ha : 0 ≤ a) :
    cfcHom ha = (SpectrumRestricts.nnreal_of_nonneg ha).starAlgHom
      (cfcHom (IsSelfAdjoint.of_nonneg ha))

Proof state:
A : Type u_1
inst✝⁹ : TopologicalSpace A
inst✝⁸ : Ring A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : IsTopologicalRing A
inst✝² : T2Space A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ cfcHom ha = SpectrumRestricts.starAlgHom (cfcHom ⋯) ⋯

Tactic:
apply (SpectrumRestricts.nnreal_of_nonneg ha).cfcHom_eq_restrict _ isUniformEmbedding_subtype_val

Result:
no goals
-- Mathlib/Computability/TuringMachine.lean
theorem stmts₁_self {q : Stmt Γ Λ σ} : q ∈ stmts₁ q

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q : Stmt Γ Λ σ
⊢ q ∈ stmts₁ q

Tactic:
cases q <;> simp only [Finset.mem_insert_self, Finset.mem_singleton_self, stmts₁]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_rotate_iff [NoZeroSMulDivisors R V] (x : P) {y z : P} :
    Wbtw R x y z ∧ Wbtw R z x y ↔ x = y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y z : P
⊢ Wbtw R x y z ∧ Wbtw R z x y ↔ x = y

Tactic:
rw [wbtw_comm, wbtw_swap_right_iff, eq_comm]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem image_subset_iff : s.image f ⊆ t ↔ ∀ x ∈ s, f x ∈ t :=
  calc
    s.image f ⊆ t ↔ f '' ↑s ⊆ ↑t

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
⊢ image f s ⊆ t ↔ f '' ↑s ⊆ ↑t

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem DiscreteTopology.of_predOrder_succOrder [PredOrder α] [SuccOrder α] :
    DiscreteTopology α

Proof state:
α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
⊢ 𝓝 a = pure a

Tactic:
rw [← nhdsWithin_univ, ← Iic_union_Ioi, nhdsWithin_union, PredOrder.nhdsLE, SuccOrder.nhdsGT,
  sup_bot_eq]

Result:
no goals

Proof state:
α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
⊢ DiscreteTopology α

Tactic:
refine discreteTopology_iff_nhds.mpr fun a ↦ ?_

Result:
α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderClosedTopology α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
⊢ 𝓝 a = pure a
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sin_coe_pi : sin (π : Angle) = 0

Proof state:
⊢ (↑π).sin = 0

Tactic:
rw [sin_coe, Real.sin_pi]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem or_self_left  : ∀ (a b : Bool), (a || (a || b)) = (a || b)

Proof state:
⊢ ∀ (a b : Bool), (a || (a || b)) = (a || b)

Tactic:
decide

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem tendsto_pi {β : Type*} {m : β → ∀ i, α i} {l : Filter β} :
    Tendsto m l (pi f) ↔ ∀ i, Tendsto (fun x => m x i) l (f i)

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : Type u_3
m : β → (i : ι) → α i
l : Filter β
⊢ Tendsto m l (pi f) ↔ ∀ (i : ι), Tendsto (fun x => m x i) l (f i)

Tactic:
simp only [pi, tendsto_iInf, tendsto_comap_iff]

Result:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : Type u_3
m : β → (i : ι) → α i
l : Filter β
⊢ (∀ (i : ι), Tendsto (eval i ∘ m) l (f i)) ↔ ∀ (i : ι), Tendsto (fun x => m x i) l (f i)

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
β : Type u_3
m : β → (i : ι) → α i
l : Filter β
⊢ (∀ (i : ι), Tendsto (eval i ∘ m) l (f i)) ↔ ∀ (i : ι), Tendsto (fun x => m x i) l (f i)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Option.lean
theorem some_mem_insertNone {s : Finset α} {a : α} : some a ∈ insertNone s ↔ a ∈ s

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ some a ∈ insertNone s ↔ a ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrix_toLin (M : Matrix m n R) :
    LinearMap.toMatrix v₁ v₂ (Matrix.toLin v₁ v₂ M) = M

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M : Matrix m n R
⊢ (toMatrix v₁ v₂) ((toLin v₁ v₂) M) = M

Tactic:
rw [← Matrix.toLin_symm, LinearEquiv.symm_apply_apply]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem orthonormal_adjustToOrientation : Orthonormal ℝ (e.toBasis.adjustToOrientation x)

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst✝ : Nonempty ι
⊢ Orthonormal ℝ ⇑(e.toBasis.adjustToOrientation x)

Tactic:
apply e.orthonormal.orthonormal_of_forall_eq_or_eq_neg

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst✝ : Nonempty ι
⊢ ∀ (i : ι), (e.toBasis.adjustToOrientation x) i = e i ∨ (e.toBasis.adjustToOrientation x) i = -e i

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst✝ : Nonempty ι
⊢ ∀ (i : ι), (e.toBasis.adjustToOrientation x) i = e i ∨ (e.toBasis.adjustToOrientation x) i = -e i

Tactic:
simpa using e.toBasis.adjustToOrientation_apply_eq_or_eq_neg x

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_id (P : W'⟮F⟯) : map (Algebra.ofId F F) P = P

Proof state:
R : Type r
F : Type u
inst✝² : CommRing R
inst✝¹ : Field F
W' : Affine R
inst✝ : Algebra R F
P : W'⟮F⟯
⊢ (map (Algebra.ofId F F)) P = P

Tactic:
cases P <;> rfl

Result:
no goals
-- Mathlib/Data/PNat/Xgcd.lean
theorem v_eq_succ_vp : u.v = succ₂ u.vp

Proof state:
u : XgcdType
⊢ u.v = succ₂ u.vp

Tactic:
ext <;> dsimp [v, vp, w, z, a, b, succ₂] <;> ring_nf

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic_two (R : Type*) [Ring R] : cyclotomic 2 R = X + 1

Proof state:
R : Type u_1
inst✝ : Ring R
⊢ cyclotomic 2 R = X + 1

Tactic:
simp [cyclotomic_prime]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_monomial_single (i : σ) {e : ℕ} {r : R} (he : e ≠ 0) (hr : r ≠ 0) :
    (monomial (Finsupp.single i e) r).vars = {i}

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
e : ℕ
r : R
he : e ≠ 0
hr : r ≠ 0
⊢ ((monomial (Finsupp.single i e)) r).vars = {i}

Tactic:
rw [vars_monomial hr, Finsupp.support_single_ne_zero _ he]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearMap.lean
theorem flip_inj {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (H : flip f = flip g) : f = g :=
  ext₂ fun m n => show flip f n m = flip g n m by rw [H]

Proof state:
R : Type u_1
inst✝¹¹ : Semiring R
S : Type u_2
inst✝¹⁰ : Semiring S
R₂ : Type u_3
inst✝⁹ : Semiring R₂
S₂ : Type u_4
inst✝⁸ : Semiring S₂
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module S N
inst✝² : Module R₂ P
inst✝¹ : Module S₂ P
inst✝ : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
H : f.flip = g.flip
m : M
n : N
⊢ (f.flip n) m = (g.flip n) m

Tactic:
rw [H]

Result:
no goals
-- Mathlib/RingTheory/Valuation/AlgebraInstances.lean
theorem isIntegral_of_mem_ringOfIntegers {x : L} (hx : x ∈ integralClosure v.valuationSubring L) :
    IsIntegral v.valuationSubring (⟨x, hx⟩ : integralClosure v.valuationSubring L)

Proof state:
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : x ∈ integralClosure (↥v.valuationSubring) L
⊢ IsIntegral ↥v.valuationSubring ⟨x, hx⟩

Tactic:
obtain ⟨P, hPm, hP⟩ := hx

Result:
case intro.intro
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
P : Polynomial ↥v.valuationSubring
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap (↥v.valuationSubring) L) x P = 0
⊢ IsIntegral ↥v.valuationSubring ⟨x, ⋯⟩

Proof state:
case intro.intro
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
P : Polynomial ↥v.valuationSubring
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap (↥v.valuationSubring) L) x P = 0
⊢ IsIntegral ↥v.valuationSubring ⟨x, ⋯⟩

Tactic:
refine ⟨P, hPm, ?_⟩

Result:
case intro.intro
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
P : Polynomial ↥v.valuationSubring
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap (↥v.valuationSubring) L) x P = 0
⊢ Polynomial.eval₂ (algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L)) ⟨x, ⋯⟩ P = 0

Proof state:
case intro.intro
K : Type u_1
inst✝² : Field K
v : Valuation K ℤₘ₀
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
P : Polynomial ↥v.valuationSubring
hPm : P.Monic
hP : Polynomial.eval₂ (algebraMap (↥v.valuationSubring) L) x P = 0
⊢ Polynomial.eval₂ (algebraMap ↥v.valuationSubring ↥(integralClosure (↥v.valuationSubring) L)) ⟨x, ⋯⟩ P = 0

Tactic:
rw [← Polynomial.aeval_def, ← Subalgebra.coe_eq_zero, Polynomial.aeval_subalgebra_coe,
  Polynomial.aeval_def, Subtype.coe_mk, hP]

Result:
no goals
-- Mathlib/Data/Finsupp/Order.lean
lemma mapDomain_nonneg (hg : 0 ≤ g) : 0 ≤ g.mapDomain f

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : OrderedAddCommMonoid α
f : ι → κ
g : ι →₀ α
hg : 0 ≤ g
⊢ 0 ≤ mapDomain f g

Tactic:
simpa using mapDomain_mono hg

Result:
no goals
-- Mathlib/Logic/Denumerable.lean
theorem coe_comp_ofNat_range : Set.range ((↑) ∘ ofNat s : ℕ → ℕ) = s

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
⊢ Set.range (Subtype.val ∘ ofNat s) = s

Tactic:
rw [Set.range_comp Subtype.val, ofNat_range, Set.image_univ, Subtype.range_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem extractLsb'_and {x y : BitVec w} {start len : Nat} :
   (x &&& y).extractLsb' start len = (x.extractLsb' start len) &&& (y.extractLsb' start len)

Proof state:
case pred
w : Nat
x y : BitVec w
start len i : Nat
hi : i < len
⊢ (extractLsb' start len (x &&& y)).getLsbD i = (extractLsb' start len x &&& extractLsb' start len y).getLsbD i

Tactic:
simp [hi]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
start len : Nat
⊢ extractLsb' start len (x &&& y) = extractLsb' start len x &&& extractLsb' start len y

Tactic:
ext i hi

Result:
case pred
w : Nat
x y : BitVec w
start len i : Nat
hi : i < len
⊢ (extractLsb' start len (x &&& y)).getLsbD i = (extractLsb' start len x &&& extractLsb' start len y).getLsbD i
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean
lemma ext_mk₀_f_comp_ext_mk₀_g : (Ext.mk₀ S.f).comp (Ext.mk₀ S.g) (zero_add 0) = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
⊢ (Ext.mk₀ S.f).comp (Ext.mk₀ S.g) ⋯ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[simp]
lemma ofZeros_g' (hf : S.f = 0) (hg : S.g = 0) :
    (ofZeros S hf hg).g' = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
hg : S.g = 0
⊢ (ofZeros S hf hg).g' = 0

Tactic:
rw [← cancel_epi ((ofZeros S hf hg).p), comp_zero, p_g', hg]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem mem_split_iff' : J ∈ split I i x ↔
    (J : Set (ι → ℝ)) = ↑I ∩ { y | y i ≤ x } ∨ (J : Set (ι → ℝ)) = ↑I ∩ { y | x < y i }

Proof state:
ι : Type u_1
I J : Box ι
i : ι
x : ℝ
⊢ J ∈ split I i x ↔ ↑J = ↑I ∩ {y | y i ≤ x} ∨ ↑J = ↑I ∩ {y | x < y i}

Tactic:
simp [mem_split_iff, ← Box.withBotCoe_inj]

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem prod_top (s : Subring R) : s.prod (⊤ : Subring S) = s.comap (RingHom.fst R S) :=
  ext fun x => by simp [mem_prod, MonoidHom.coe_fst]

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
s : Subring R
x : R × S
⊢ x ∈ s.prod ⊤ ↔ x ∈ comap (RingHom.fst R S) s

Tactic:
simp [mem_prod, MonoidHom.coe_fst]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean
theorem Sphere.secondInter_smul (s : Sphere P) (p : P) (v : V) {r : ℝ} (hr : r ≠ 0) :
    s.secondInter p (r • v) = s.secondInter p v

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
r : ℝ
hr : r ≠ 0
⊢ (-2 * (r * inner v (p -ᵥ s.center)) / r / r / inner v v * r) • v +ᵥ p =
    (-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p

Tactic:
rw [mul_comm, ← mul_div_assoc, ← mul_div_assoc, mul_div_cancel_left₀ _ hr, mul_comm, mul_assoc,
  mul_div_cancel_left₀ _ hr, mul_comm]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
r : ℝ
hr : r ≠ 0
⊢ s.secondInter p (r • v) = s.secondInter p v

Tactic:
simp_rw [Sphere.secondInter, real_inner_smul_left, inner_smul_right, smul_smul,
  div_mul_eq_div_div]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
v : V
r : ℝ
hr : r ≠ 0
⊢ (-2 * (r * inner v (p -ᵥ s.center)) / r / r / inner v v * r) • v +ᵥ p =
    (-2 * inner v (p -ᵥ s.center) / inner v v) • v +ᵥ p
-- Mathlib/Data/Finset/Preimage.lean
theorem sigma_preimage_mk_of_subset {β : α → Type*} [DecidableEq α] (s : Finset (Σa, β a))
    {t : Finset α} (ht : s.image Sigma.fst ⊆ t) :
    (t.sigma fun a => s.preimage (Sigma.mk a) sigma_mk_injective.injOn) = s

Proof state:
α : Type u
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
ht : image Sigma.fst s ⊆ t
⊢ (t.sigma fun a => s.preimage (Sigma.mk a) ⋯) = s

Tactic:
rw [sigma_preimage_mk, filter_true_of_mem <| image_subset_iff.1 ht]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem span_singleton_mul_right_mono [IsDomain R] {x : R} (hx : x ≠ 0) :
    span {x} * I ≤ span {x} * J ↔ I ≤ J

Proof state:
R : Type u
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
⊢ span {x} * I ≤ span {x} * J ↔ I ≤ J

Tactic:
simp_rw [span_singleton_mul_le_span_singleton_mul, mul_right_inj' hx,
  exists_eq_right', SetLike.le_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_concat (x : BitVec w) (b : Bool) : ~~~(concat x b) = concat (~~~x) !b

Proof state:
w : Nat
x : BitVec w
b : Bool
⊢ ~~~x.concat b = (~~~x).concat !b

Tactic:
ext (_ | i) h <;> simp [getLsbD_concat]

Result:
no goals
-- Mathlib/Analysis/BoundedVariation.lean
theorem ae_differentiableAt {f : ℝ → V} (h : LocallyBoundedVariationOn f univ) :
    ∀ᵐ x, DifferentiableAt ℝ f x

Proof state:
case h
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
h : LocallyBoundedVariationOn f univ
x : ℝ
hx : x ∈ univ → DifferentiableWithinAt ℝ f univ x
⊢ DifferentiableAt ℝ f x

Tactic:
rw [differentiableWithinAt_univ] at hx

Result:
case h
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
h : LocallyBoundedVariationOn f univ
x : ℝ
hx : x ∈ univ → DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ f x

Proof state:
case h
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
h : LocallyBoundedVariationOn f univ
x : ℝ
hx : x ∈ univ → DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ f x

Tactic:
exact hx (mem_univ _)

Result:
no goals

Proof state:
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
h : LocallyBoundedVariationOn f univ
⊢ ∀ᵐ (x : ℝ), DifferentiableAt ℝ f x

Tactic:
filter_upwards [h.ae_differentiableWithinAt_of_mem] with x hx

Result:
case h
V : Type u_3
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
f : ℝ → V
h : LocallyBoundedVariationOn f univ
x : ℝ
hx : x ∈ univ → DifferentiableWithinAt ℝ f univ x
⊢ DifferentiableAt ℝ f x
-- Mathlib/Data/Set/Finite/Basic.lean
theorem coeSort_toFinset : ↥hs.toFinset = ↥s

Proof state:
α : Type u
s : Set α
hs : s.Finite
⊢ { x // x ∈ hs.toFinset } = ↑s

Tactic:
rw [← Finset.coe_sort_coe _, hs.coe_toFinset]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
theorem pullbackZeroZeroIso_hom_fst (X Y : C) [HasBinaryProduct X Y] :
    (pullbackZeroZeroIso X Y).hom ≫ prod.fst = pullback.fst 0 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).hom ≫ prod.fst = pullback.fst 0 0

Tactic:
simp [← Iso.eq_inv_comp]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma sub_nonneg {x y : EReal} (h_top : x ≠ ⊤ ∨ y ≠ ⊤) (h_bot : x ≠ ⊥ ∨ y ≠ ⊥) :
    0 ≤ x - y ↔ y ≤ x

Proof state:
x y : EReal
h_top : x ≠ ⊤ ∨ y ≠ ⊤
h_bot : x ≠ ⊥ ∨ y ≠ ⊥
⊢ 0 ≤ x - y ↔ y ≤ x

Tactic:
cases x <;> cases y <;> simp_all [← EReal.coe_sub]

Result:
no goals
-- Mathlib/GroupTheory/Perm/ConjAct.lean
theorem mem_conj_support (k : ConjAct (Perm α)) (g : Perm α) (a : α) :
    a ∈ (k • g).support ↔ ConjAct.ofConjAct k⁻¹ a ∈ g.support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (ConjAct.ofConjAct k) (g ((ConjAct.ofConjAct k)⁻¹ a)) = a ↔ g ((ConjAct.ofConjAct k)⁻¹ a) = (ConjAct.ofConjAct k)⁻¹ a

Tactic:
apply Equiv.apply_eq_iff_eq_symm_apply

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ a ∈ (k • g).support ↔ (ConjAct.ofConjAct k⁻¹) a ∈ g.support

Tactic:
simp only [mem_support, ConjAct.smul_def, not_iff_not, coe_mul,
  Function.comp_apply, ConjAct.ofConjAct_inv]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g : Perm α
a : α
⊢ (ConjAct.ofConjAct k) (g ((ConjAct.ofConjAct k)⁻¹ a)) = a ↔ g ((ConjAct.ofConjAct k)⁻¹ a) = (ConjAct.ofConjAct k)⁻¹ a
-- Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean
theorem ne_zero_of_mem_factors {p a : α} (h : p ∈ factors a) : a ≠ 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p a : α
h : p ∈ factors a
⊢ a ≠ 0

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p : α
h : p ∈ factors 0
⊢ False

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p : α
h : p ∈ factors 0
⊢ False

Tactic:
simp at h

Result:
no goals
-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma δAux_C (r) :
    δAux R Q (C r) = 1 ⊗ₜ D R S r

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
r : S
⊢ (δAux R Q) (C r) = 1 ⊗ₜ[S] (D R S) r

Tactic:
rw [← monomial_zero', δAux_monomial, Finsupp.prod_zero_index]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem clauses_insertRupUnits {n : Nat} (f : DefaultFormula n)
    (units : CNF.Clause (PosFin n)) :
    (f.insertRupUnits units).1.clauses = f.clauses

Proof state:
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
⊢ (f.insertRupUnits units).fst.clauses = f.clauses

Tactic:
rw [insertRupUnits]

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem clog_of_two_le {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) :
    clog b n = clog b ((n + b - 1) / b) + 1

Proof state:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ clog b n = clog b ((n + b - 1) / b) + 1

Tactic:
rw [clog, dif_pos (⟨hb, hn⟩ : 1 < b ∧ 1 < n)]

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_conjTranspose [InvolutiveStar α] (M : Matrix m n α) : Mᴴᴴ = M :=
  Matrix.ext <| by simp

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝ : InvolutiveStar α
M : Matrix m n α
⊢ ∀ (i : m) (j : n), Mᴴᴴ i j = M i j

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem ext {x y : ReaderT ρ m α} (h : ∀ ctx, x.run ctx = y.run ctx) : x = y

Proof state:
ρ : Type u_1
m : Type u_1 → Type u_2
α : Type u_1
x y : ReaderT ρ m α
h : ∀ (ctx : ρ), x ctx = y ctx
⊢ x = y

Tactic:
exact funext h

Result:
no goals

Proof state:
ρ : Type u_1
m : Type u_1 → Type u_2
α : Type u_1
x y : ReaderT ρ m α
h : ∀ (ctx : ρ), x.run ctx = y.run ctx
⊢ x = y

Tactic:
simp [run] at h

Result:
ρ : Type u_1
m : Type u_1 → Type u_2
α : Type u_1
x y : ReaderT ρ m α
h : ∀ (ctx : ρ), x ctx = y ctx
⊢ x = y
-- Mathlib/GroupTheory/PGroup.lean
theorem of_bot : IsPGroup p (⊥ : Subgroup G) :=
  of_card (n := 0) (by rw [Subgroup.card_bot, pow_zero])

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥⊥ = p ^ 0

Tactic:
rw [Subgroup.card_bot, pow_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/GetElem.lean
theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a

Proof state:
α : Type u_1
a : α
as : List α
h : 0 < (a :: as).length
⊢ getElem (a :: as) 0 h = a

Tactic:
rfl

Result:
no goals