harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/Mul.lean
theorem mulVec_vecMul [Fintype n] [Fintype o] (A : Matrix m n α) (B : Matrix o n α) (x : o → α) :
    A *ᵥ (x ᵥ* B) = (A * Bᵀ) *ᵥ x

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalCommSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
A : Matrix m n α
B : Matrix o n α
x : o → α
⊢ A *ᵥ x ᵥ* B = (A * Bᵀ) *ᵥ x

Tactic:
rw [← mulVec_mulVec, mulVec_transpose]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem toNNReal_eq_zero {r : ℝ} : Real.toNNReal r = 0 ↔ r ≤ 0

Proof state:
r : ℝ
⊢ r.toNNReal = 0 ↔ r ≤ 0

Tactic:
simpa [-toNNReal_pos] using not_iff_not.2 (@toNNReal_pos r)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem mul_pred (n m : Nat) : n * pred m = n * m - n

Proof state:
n m : Nat
⊢ n * m.pred = n * m - n

Tactic:
rw [Nat.mul_comm, pred_mul, Nat.mul_comm]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
protected lemma IsInducing.comp (hg : IsInducing g) (hf : IsInducing f) :
    IsInducing (g ∘ f) :=
  ⟨by rw [hf.eq_induced, hg.eq_induced, induced_compose]⟩

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
hf : IsInducing f
⊢ inst✝¹ = induced (g ∘ f) inst✝

Tactic:
rw [hf.eq_induced, hg.eq_induced, induced_compose]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem lt_mul_iff_one_lt_right [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) :
    a < a * b ↔ 1 < b :=
  Iff.trans (by rw [mul_one]) (mul_lt_mul_left a0)

Proof state:
α : Type u_3
a b : α
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : PosMulStrictMono α
inst✝ : PosMulReflectLT α
a0 : 0 < a
⊢ a < a * b ↔ a * 1 < a * b

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C (q : ℕ) [hF : ExpChar F q] :
    IsPurelyInseparable F E ↔ ∀ x : E, ∃ (n : ℕ) (y : F), minpoly F x = X ^ q ^ n - C y

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n y, minpoly F x = X ^ q ^ n - C y

Tactic:
simp_rw [isPurelyInseparable_iff_natSepDegree_eq_one,
  minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C q]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem ne_nil_of_mem {a : α} {l : List α} (h : a ∈ l) : l ≠ []

Proof state:
α : Type u_1
a : α
l : List α
h : a ∈ l
⊢ l ≠ []

Tactic:
cases h <;> nofun

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem foldl_eq {f : δ → (a : α) → β a → δ} {init : δ} {l : AssocList α β} :
    l.foldl f init = l.toList.foldl (fun d p => f d p.1 p.2) init

Proof state:
α : Type u
β : α → Type v
δ : Type w
f : δ → (a : α) → β a → δ
init : δ
l : AssocList α β
⊢ foldl f init l = List.foldl (fun d p => f d p.fst p.snd) init l.toList

Tactic:
induction l generalizing init <;> simp_all [foldl, Id.run, foldlM]

Result:
no goals
-- Mathlib/GroupTheory/Transfer.lean
lemma coe_transferFunction (q : G ⧸ H) : ↑(transferFunction H g q) = q

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ ↑(H.transferFunction g q) = q

Tactic:
rw [transferFunction_apply, ← smul_eq_mul, Quotient.coe_smul_out,
  ← quotientEquivSigmaZMod_symm_apply, Sigma.eta, symm_apply_apply]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[simp, norm_cast] lemma coe_le_enorm : r ≤ ‖x‖ₑ ↔ r ≤ ‖x‖₊

Proof state:
E : Type u_8
inst✝ : NNNorm E
x : E
r : ℝ≥0
⊢ ↑r ≤ ‖x‖ₑ ↔ r ≤ ‖x‖₊

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
@[simp]
lemma nonempty_iff : Nonempty U.toScheme ↔ (U : Set X).Nonempty

Proof state:
X : Scheme
U : X.Opens
⊢ Nonempty ↑↑(↑U).toPresheafedSpace ↔ (↑U).Nonempty

Tactic:
simp only [toScheme_carrier, SetLike.coe_sort_coe, nonempty_subtype]

Result:
X : Scheme
U : X.Opens
⊢ (∃ x, x ∈ U) ↔ (↑U).Nonempty

Proof state:
X : Scheme
U : X.Opens
⊢ (∃ x, x ∈ U) ↔ (↑U).Nonempty

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem lt_add_one {x : PartENat} (hx : x ≠ ⊤) : x < x + 1

Proof state:
x : PartENat
hx : x ≠ ⊤
⊢ 0 < 1

Tactic:
norm_cast

Result:
no goals

Proof state:
x : PartENat
hx : x ≠ ⊤
⊢ x < x + 1

Tactic:
rw [PartENat.lt_add_iff_pos_right hx]

Result:
x : PartENat
hx : x ≠ ⊤
⊢ 0 < 1
-- Mathlib/Data/NNReal/Defs.lean
lemma toNNReal_lt_natCast {r : ℝ} {n : ℕ} (hn : n ≠ 0) : r.toNNReal < n ↔ r < n

Proof state:
r : ℝ
n : ℕ
hn : n ≠ 0
⊢ r.toNNReal < ↑n ↔ r < ↑n

Tactic:
simp [hn]

Result:
no goals
-- Mathlib/Topology/Category/Stonean/Limits.lean
lemma extremallyDisconnected_pullback : ExtremallyDisconnected {xy : X × Y | f xy.1 = i xy.2} :=
  have := extremallyDisconnected_preimage i hi
  let e := (TopCat.pullbackHomeoPreimage i i.hom.2 f hi.isEmbedding).symm
  let e' : {xy : X × Y | f xy.1 = i xy.2} ≃ₜ {xy : Y × X | i xy.1 = f xy.2}

Proof state:
X Y Z : Stonean
f : X ⟶ Z
i : Y ⟶ Z
hi : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : ExtremallyDisconnected ↑(⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f))
e : ↑(⇑(ConcreteCategory.hom i) ⁻¹' Set.range ⇑(ConcreteCategory.hom f)) ≃ₜ
  { p // (ConcreteCategory.hom i) p.1 = (ConcreteCategory.hom f) p.2 } :=
  (TopCat.pullbackHomeoPreimage ⇑(ConcreteCategory.hom i) ⋯ ⇑(ConcreteCategory.hom f) ⋯).symm
⊢ ↑{xy | (ConcreteCategory.hom f) xy.1 = (ConcreteCategory.hom i) xy.2} ≃ₜ
    ↑{xy | (ConcreteCategory.hom i) xy.1 = (ConcreteCategory.hom f) xy.2}

Tactic:
exact TopCat.homeoOfIso
  ((TopCat.pullbackIsoProdSubtype f i).symm ≪≫ pullbackSymmetry _ _ ≪≫
    (TopCat.pullbackIsoProdSubtype i f))

Result:
no goals
-- Mathlib/Probability/Distributions/Pareto.lean
lemma isProbabilityMeasure_paretoMeasure (ht : 0 < t) (hr : 0 < r) :
    IsProbabilityMeasure (paretoMeasure t r) where
  measure_univ

Proof state:
t r : ℝ
ht : 0 < t
hr : 0 < r
⊢ (paretoMeasure t r) univ = 1

Tactic:
simp [paretoMeasure, lintegral_paretoPDF_eq_one ht hr]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integrableOn_Ioi_comp_rpow_iff' [NormedSpace ℝ E] (f : ℝ → E) {p : ℝ} (hp : p ≠ 0) :
    IntegrableOn (fun x => x ^ (p - 1) • f (x ^ p)) (Ioi 0) ↔ IntegrableOn f (Ioi 0)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
p : ℝ
hp : p ≠ 0
⊢ IntegrableOn (fun x => x ^ (p - 1) • f (x ^ p)) (Ioi 0) volume ↔ IntegrableOn f (Ioi 0) volume

Tactic:
simpa only [← integrableOn_Ioi_comp_rpow_iff f hp, mul_smul] using
  (integrable_smul_iff (abs_pos.mpr hp).ne' _).symm

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem rename_polynomial_aeval_X {σ τ : Type*} (f : σ → τ) (i : σ) (p : R[X]) :
    rename f (Polynomial.aeval (X i) p) = Polynomial.aeval (X (f i) : MvPolynomial τ R) p

Proof state:
R : Type u
inst✝ : CommSemiring R
σ : Type u_2
τ : Type u_3
f : σ → τ
i : σ
p : R[X]
⊢ (rename f) ((Polynomial.aeval (X i)) p) = (Polynomial.aeval (X (f i))) p

Tactic:
rw [← aeval_algHom_apply, rename_X]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/WithTop.lean
@[simp] lemma mul_bot (h : a ≠ 0) : a * ⊥ = ⊥

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a : WithBot α
h : a ≠ 0
⊢ a * ⊥ = ⊥

Tactic:
rw [mul_bot', if_neg h]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem coe_iInf {ι : Sort*} {S : ι → Subalgebra R A} : (↑(⨅ i, S i) : Set A) = ⋂ i, S i

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem transnumAuxSeq_zero : f.transnumAuxSeq 0 = f 0

Proof state:
f : CircleDeg1Lift
⊢ f.transnumAuxSeq 0 = f 0

Tactic:
simp [transnumAuxSeq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem isNone_attach (o : Option α) : o.attach.isNone = o.isNone

Proof state:
α : Type u_1
o : Option α
⊢ o.attach.isNone = o.isNone

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma ofENat_lt_lift {x : Cardinal.{v}} {m : ℕ∞} : m < lift.{u} x ↔ m < x

Proof state:
x : Cardinal.{v}
m : ℕ∞
⊢ ↑m < lift.{u, v} x ↔ ↑m < x

Tactic:
rw [← lift_ofENat.{u, v}, lift_lt]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem exists_measurable_superset (μ : Measure α) (s : Set α) :
    ∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = μ s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = μ s

Tactic:
simpa only [← measure_eq_trim] using μ.toOuterMeasure.exists_measurable_superset_eq_trim s

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.or_eq_of_eq_true_right {a b : Bool} (h : b = true) : (a || b) = true

Proof state:
a b : Bool
h : b = true
⊢ (a || b) = true

Tactic:
simp [h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma add_of_Z_eq_zero_left {P Q : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) (hQz : Q z ≠ 0) :
    W'.add P Q = (P x * Q z) • Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
hQz : Q z ≠ 0
⊢ W'.add P Q = (P x * Q z) • Q

Tactic:
rw [add, if_neg <| not_equiv_of_Z_eq_zero_left hPz hQz, addXYZ_of_Z_eq_zero_left hP hPz]

Result:
no goals
-- Mathlib/Topology/Algebra/WithZeroTopology.lean
theorem singleton_mem_nhds_of_ne_zero (h : γ ≠ 0) : ({γ} : Set Γ₀) ∈ 𝓝 (γ : Γ₀)

Proof state:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ {γ} ∈ 𝓝 γ

Tactic:
simp [h]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma δ_snd (X Y : C) : OplaxMonoidal.δ F X Y ≫ snd _ _ = F.map (snd _ _)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ChosenFiniteProducts C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : ChosenFiniteProducts D
F : C ⥤ D
X Y : C
⊢ OplaxMonoidal.δ F X Y ≫ snd (F.obj X) (F.obj Y) = F.map (snd X Y)

Tactic:
simp [δ_of_chosenFiniteProducts]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem minpoly_gen (α : E) :
    minpoly F (AdjoinSimple.gen F α) = minpoly F α

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
⊢ minpoly F (AdjoinSimple.gen F α) = minpoly F α

Tactic:
rw [← minpoly.algebraMap_eq (algebraMap F⟮α⟯ E).injective, AdjoinSimple.algebraMap_gen]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem indicator_ae_eq_restrict (hs : MeasurableSet s) : indicator s f =ᵐ[μ.restrict s] f

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
⊢ s.indicator f =ᶠ[ae (μ.restrict s)] f

Tactic:
classical exact piecewise_ae_eq_restrict hs

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
hs : MeasurableSet s
⊢ s.indicator f =ᶠ[ae (μ.restrict s)] f

Tactic:
exact piecewise_ae_eq_restrict hs

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem IsHermitian.zpow [Fintype m] [DecidableEq m] {A : Matrix m m α} (h : A.IsHermitian)
    (k : ℤ) :
    (A ^ k).IsHermitian

Proof state:
α : Type u_1
m : Type u_3
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
h : A.IsHermitian
k : ℤ
⊢ (A ^ k).IsHermitian

Tactic:
rw [IsHermitian, conjTranspose_zpow, h]

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Pi.lean
theorem piQuotientLift_mk [Fintype ι] [DecidableEq ι] (p : ∀ i, Submodule R (Ms i))
    (q : Submodule R N) (f : ∀ i, Ms i →ₗ[R] N) (hf : ∀ i, p i ≤ q.comap (f i)) (x : ∀ i, Ms i) :
    (piQuotientLift p q f hf fun i => Quotient.mk (x i)) = Quotient.mk (lsum _ _ R f x)

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
x : (i : ι) → Ms i
⊢ (∑ d : ι, ((p d).mapQ q (f d) ⋯ ∘ₗ proj d) fun i => Quotient.mk (x i)) = ∑ x_1 : ι, q.mkQ ((f x_1 ∘ₗ proj x_1) x)

Tactic:
simp only [coe_proj, mapQ_apply, mkQ_apply, comp_apply]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
x : (i : ι) → Ms i
⊢ ((piQuotientLift p q f hf) fun i => Quotient.mk (x i)) = Quotient.mk (((lsum R Ms R) f) x)

Tactic:
rw [piQuotientLift, lsum_apply, sum_apply, ← mkQ_apply, lsum_apply, sum_apply, _root_.map_sum]

Result:
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
x : (i : ι) → Ms i
⊢ (∑ d : ι, ((p d).mapQ q (f d) ⋯ ∘ₗ proj d) fun i => Quotient.mk (x i)) = ∑ x_1 : ι, q.mkQ ((f x_1 ∘ₗ proj x_1) x)
-- Mathlib/Data/Nat/Init.lean
/-- If a small natural number is divisible by a larger natural number,
the small number is zero. -/
lemma eq_zero_of_dvd_of_lt (w : a ∣ b) (h : b < a) : b = 0 :=
  Nat.eq_zero_of_dvd_of_div_eq_zero w (by simp [h])

Proof state:
a b : ℕ
w : a ∣ b
h : b < a
⊢ b / a = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_self_mul_conjTranspose (A : Matrix m n R) : (A * Aᴴ).rank = A.rank

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : Field R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (A * Aᴴ).rank = A.rank

Tactic:
simpa only [rank_conjTranspose, conjTranspose_conjTranspose] using
  rank_conjTranspose_mul_self Aᴴ

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem tail_zip_fst {l : List (α × β)} : l.unzip.1.tail = l.tail.unzip.1

Proof state:
α : Type u_1
β : Type u_2
l : List (α × β)
⊢ l.unzip.fst.tail = l.tail.unzip.fst

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
@[fun_prop]
lemma continuous_multichoose (k : ℕ) : Continuous (fun x : ℤ_[p] ↦ Ring.multichoose x k)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ Continuous (Subtype.val ∘ fun x => ⟨↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) / ↑k.factorial, ⋯⟩)

Tactic:
fun_prop

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ Continuous fun x => Ring.multichoose x k

Tactic:
simp only [Ring.multichoose, BinomialRing.multichoose, continuous_induced_rng]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ Continuous (Subtype.val ∘ fun x => ⟨↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) / ↑k.factorial, ⋯⟩)
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_bot : a ∆ ⊥ = a

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a : α
⊢ a ∆ ⊥ = a

Tactic:
rw [symmDiff, sdiff_bot, bot_sdiff, sup_bot_eq]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem symm_map_nhdsWithin_image {x : H} {s : Set H} : map I.symm (𝓝[I '' s] I x) = 𝓝[s] x

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
x : H
s : Set H
⊢ map (↑I.symm) (𝓝[↑I '' s] ↑I x) = 𝓝[s] x

Tactic:
rw [← I.map_nhdsWithin_eq, map_map, I.symm_comp_self, map_id]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem add_int_iff : LiouvilleWith p (x + m) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
m : ℤ
⊢ LiouvilleWith p (x + ↑m) ↔ LiouvilleWith p x

Tactic:
rw [← Rat.cast_intCast m, add_rat_iff]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem of_rat_sub (h : Irrational (q - x)) : Irrational x :=
  of_neg (of_rat_add q (by simpa only [sub_eq_add_neg] using h))

Proof state:
q : ℚ
x : ℝ
h : Irrational (↑q - x)
⊢ Irrational (↑q + -x)

Tactic:
simpa only [sub_eq_add_neg] using h

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem span_eq_top_of_surjective {s : Set P₁} (hf : Function.Surjective f)
    (h : affineSpan k s = ⊤) : affineSpan k (f '' s) = ⊤

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
s : Set P₁
hf : Function.Surjective ⇑f
h : affineSpan k s = ⊤
⊢ affineSpan k (⇑f '' s) = ⊤

Tactic:
rw [← AffineSubspace.map_span, h, map_top_of_surjective f hf]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Category.lean
theorem hcomp_id_app {H : D ⥤ E} (α : F ⟶ G) (X : C) : (α ◫ 𝟙 H).app X = H.map (α.app X)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
H : D ⥤ E
α : F ⟶ G
X : C
⊢ (α ◫ 𝟙 H).app X = H.map (α.app X)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_rpow : logb b (b ^ x) = x

Proof state:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ logb b (b ^ x) = x

Tactic:
rw [logb, div_eq_iff, log_rpow b_pos]

Result:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ log b ≠ 0

Proof state:
b x : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ log b ≠ 0

Tactic:
exact log_b_ne_zero b_pos b_ne_one

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem neg_mulExpNegMulSq_neg (ε x : ℝ) : - mulExpNegMulSq ε (-x) = mulExpNegMulSq ε x

Proof state:
ε x : ℝ
⊢ -ε.mulExpNegMulSq (-x) = ε.mulExpNegMulSq x

Tactic:
simp [mulExpNegMulSq]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_diff_add_encard_inter (s t : Set α) :
    (s \ t).encard + (s ∩ t).encard = s.encard

Proof state:
α : Type u_1
s t : Set α
⊢ (s \ t).encard + (s ∩ t).encard = s.encard

Tactic:
rw [← encard_union_eq (disjoint_of_subset_right inter_subset_right disjoint_sdiff_left),
  diff_union_inter]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma isGreatest_norm_quasispectrum (a : A) (ha : p a

Proof state:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : autoParam (p a) _auto✝
⊢ IsGreatest ((fun x => ‖x‖) '' σₙ 𝕜 a) ‖a‖

Tactic:
simpa only [cfcₙ_id 𝕜 a] using IsGreatest.norm_cfcₙ (id : 𝕜 → 𝕜) a

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem monic_X_pow_sub_C {R : Type u} [Ring R] (a : R) {n : ℕ} (h : n ≠ 0) :
    (X ^ n - C a).Monic

Proof state:
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : n ≠ 0
⊢ (X ^ n - C a).Monic

Tactic:
simpa only [map_neg, ← sub_eq_add_neg] using monic_X_pow_add_C (-a) h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem head?_iota (n : Nat) : (iota n).head? = if n = 0 then none else some n

Proof state:
n : Nat
⊢ (iota n).head? = if n = 0 then none else some n

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean
lemma congr_d {d d' : M.Derivation φ} (h : d = d') {X : Dᵒᵖ} (b : R.obj X) :
    d.d b = d'.d b

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
R : Dᵒᵖ ⥤ CommRingCat
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
d d' : M.Derivation φ
h : d = d'
X : Dᵒᵖ
b : ↑(R.obj X)
⊢ d.d b = d'.d b

Tactic:
rw [h]

Result:
no goals
-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem thin_diagram_of_surjective (Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), (F.map f).Surjective) {i j}
    (f g : i ⟶ j) : F.map f = F.map g :=
  let ⟨k, φ, hφ⟩ := IsCofilteredOrEmpty.cone_maps f g
  (Fsur φ).injective_comp_right <| by simp_rw [← types_comp, ← F.map_comp, hφ]

Proof state:
J : Type u
inst✝¹ : Category.{u_1, u} J
F : J ⥤ Type v
inst✝ : IsCofilteredOrEmpty J
Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)
i j : J
f g : i ⟶ j
k : J
φ : k ⟶ i
hφ : φ ≫ f = φ ≫ g
⊢ (fun g => g ∘ F.map φ) (F.map f) = (fun g => g ∘ F.map φ) (F.map g)

Tactic:
simp_rw [← types_comp, ← F.map_comp, hφ]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem Function.LeftInverse.eq_rec_eq {γ : β → Sort v} {f : α → β} {g : β → α}
    (h : Function.LeftInverse g f) (C : ∀ a : α, γ (f a)) (a : α) :
    -- TODO: mathlib3 uses `(congr_arg f (h a)).rec (C (g (f a)))` for LHS
    @Eq.rec β (f (g (f a))) (fun x _ ↦ γ x) (C (g (f a))) (f a) (congr_arg f (h a)) = C a :=
  eq_of_heq <| (eqRec_heq _ _).trans <| by rw [h]

Proof state:
α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ HEq (C (g (f a))) (C a)

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem image_ennreal_ofReal (h : s.OrdConnected) : (ENNReal.ofReal '' s).OrdConnected

Proof state:
s : Set ℝ
h : s.OrdConnected
⊢ (ENNReal.ofReal '' s).OrdConnected

Tactic:
simpa only [image_image] using h.image_real_toNNReal.image_coe_nnreal_ennreal

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Lemmas.lean
theorem recDiagAux_zero_left {motive : Nat → Nat → Sort _}
    (zero_left : ∀ n, motive 0 n) (zero_right : ∀ m, motive m 0)
    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) (n) :
    Nat.recDiagAux zero_left zero_right succ_succ 0 n = zero_left n

Proof state:
motive : Nat → Nat → Sort u_1
zero_left : (n : Nat) → motive 0 n
zero_right : (m : Nat) → motive m 0
succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)
n : Nat
⊢ Nat.recDiagAux zero_left zero_right succ_succ 0 n = zero_left n

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem map_prod_map_mk_nhds (x : X) (y : Y) :
    map (Prod.map mk mk) (𝓝 (x, y)) = 𝓝 (mk x, mk y)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
⊢ Filter.map (Prod.map mk mk) (𝓝 (x, y)) = 𝓝 (mk x, mk y)

Tactic:
rw [nhds_prod_eq, ← prod_map_map_eq', map_mk_nhds, map_mk_nhds, nhds_prod_eq]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem val_eq (h : v₁.IsEquiv v₂) {r s : R} : v₁ r = v₁ s ↔ v₂ r = v₂ s

Proof state:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r s : R
⊢ v₁ r = v₁ s ↔ v₂ r = v₂ s

Tactic:
simpa only [le_antisymm_iff] using and_congr (h r s) (h s r)

Result:
no goals
-- Mathlib/Condensed/Discrete/Colimit.lean
@[simp]
lemma lanPresheafNatIso_hom_app
    (hF : ∀ S : LightProfinite, IsColimit <| F.mapCocone (coconeRightOpOfCone S.asLimitCone))
    (S : LightProfiniteᵒᵖ) : (lanPresheafNatIso hF).hom.app S =
      colimit.desc _ (LightProfinite.Extend.cocone _ _)

Proof state:
F : LightProfiniteᵒᵖ ⥤ Type u
hF : (S : LightProfinite) → IsColimit (F.mapCocone (coconeRightOpOfCone S.asLimitCone))
S : LightProfiniteᵒᵖ
⊢ (lanPresheafNatIso hF).hom.app S =
    colimit.desc (CostructuredArrow.proj toLightProfinite.op (Opposite.op (Opposite.unop S)) ⋙ toLightProfinite.op ⋙ F)
      (LightProfinite.Extend.cocone F (Opposite.unop S))

Tactic:
simp [lanPresheafNatIso]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem ofNat_max_zero (n : Nat) : (max (n : Int) 0) = n

Proof state:
n : Nat
⊢ max (↑n) 0 = ↑n

Tactic:
rw [Int.max_eq_left (ofNat_zero_le n)]

Result:
no goals