harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem canonicalEquiv_flip (I) : canonicalEquiv S P P' (canonicalEquiv S P' P I) = I

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P'
⊢ (canonicalEquiv S P P') ((canonicalEquiv S P' P) I) = I

Tactic:
rw [← canonicalEquiv_symm, RingEquiv.symm_apply_apply]

Result:
no goals
-- Mathlib/Algebra/Homology/ComplexShapeSigns.lean
@[simp]
lemma ε_zero : c.ε 0 = 1

Proof state:
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
⊢ c.ε 0 = 1

Tactic:
apply MonoidHom.map_one

Result:
no goals
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem Monovary.sum_comp_perm_smul_lt_sum_smul_iff (hfg : Monovary f g) :
    ∑ i, f (σ i) • g i < ∑ i, f i • g i ↔ ¬Monovary (f ∘ σ) g

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedSemiring α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i : ι, f (σ i) • g i < ∑ i : ι, f i • g i ↔ ¬Monovary (f ∘ ⇑σ) g

Tactic:
simp [(hfg.monovaryOn _).sum_comp_perm_smul_lt_sum_smul_iff fun _ _ ↦ mem_univ _]

Result:
no goals
-- Mathlib/LinearAlgebra/SModEq.lean
theorem eval {R : Type*} [CommRing R] {I : Ideal R} {x y : R} (h : x ≡ y [SMOD I]) (f : R[X]) :
    f.eval x ≡ f.eval y [SMOD I]

Proof state:
R : Type u_5
inst✝ : CommRing R
I : Ideal R
x y : R
f : R[X]
h : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
⊢ (Ideal.Quotient.mk I) (Polynomial.eval x f) = (Ideal.Quotient.mk I) (Polynomial.eval y f)

Tactic:
rw [← Polynomial.eval₂_at_apply, ← Polynomial.eval₂_at_apply, h]

Result:
no goals

Proof state:
R : Type u_5
inst✝ : CommRing R
I : Ideal R
x y : R
h : Submodule.Quotient.mk x = Submodule.Quotient.mk y
f : R[X]
⊢ (Ideal.Quotient.mk I) (Polynomial.eval x f) = (Ideal.Quotient.mk I) (Polynomial.eval y f)

Tactic:
replace h : Ideal.Quotient.mk I x = Ideal.Quotient.mk I y := h

Result:
R : Type u_5
inst✝ : CommRing R
I : Ideal R
x y : R
f : R[X]
h : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
⊢ (Ideal.Quotient.mk I) (Polynomial.eval x f) = (Ideal.Quotient.mk I) (Polynomial.eval y f)

Proof state:
R : Type u_5
inst✝ : CommRing R
I : Ideal R
x y : R
h : Submodule.Quotient.mk x = Submodule.Quotient.mk y
f : R[X]
⊢ Submodule.Quotient.mk (Polynomial.eval x f) = Submodule.Quotient.mk (Polynomial.eval y f)

Tactic:
show Ideal.Quotient.mk I (f.eval x) = Ideal.Quotient.mk I (f.eval y)

Result:
R : Type u_5
inst✝ : CommRing R
I : Ideal R
x y : R
h : Submodule.Quotient.mk x = Submodule.Quotient.mk y
f : R[X]
⊢ (Ideal.Quotient.mk I) (Polynomial.eval x f) = (Ideal.Quotient.mk I) (Polynomial.eval y f)

Proof state:
R : Type u_5
inst✝ : CommRing R
I : Ideal R
x y : R
h : x ≡ y [SMOD I]
f : R[X]
⊢ Polynomial.eval x f ≡ Polynomial.eval y f [SMOD I]

Tactic:
rw [SModEq.def] at h ⊢

Result:
R : Type u_5
inst✝ : CommRing R
I : Ideal R
x y : R
h : Submodule.Quotient.mk x = Submodule.Quotient.mk y
f : R[X]
⊢ Submodule.Quotient.mk (Polynomial.eval x f) = Submodule.Quotient.mk (Polynomial.eval y f)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addX_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) : W.addX P Q =
      ((P y * Q z - Q y * P z) ^ 2 * P z * Q z
        + W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z)
        - W.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 - P x * Q z * (P x * Q z - Q x * P z) ^ 2
        - Q x * P z * (P x * Q z - Q x * P z) ^ 2) * (P x * Q z - Q x * P z) / (P z * Q z) ^ 2

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.addX P Q =
    ((P y * Q z - Q y * P z) ^ 2 * P z * Q z + W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
              W.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
            P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
          Q x * P z * (P x * Q z - Q x * P z) ^ 2) *
        (P x * Q z - Q x * P z) /
      (P z * Q z) ^ 2

Tactic:
rw [← addX_eq' hP hQ, mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_mod (a b n : Nat) : a * b % n = (a % n) * (b % n) % n

Proof state:
a b n : Nat
⊢ a * b % n = a % n * (b % n) % n

Tactic:
rw (occs := [1]) [← mod_add_div a n]

Result:
a b n : Nat
⊢ (a % n + n * (a / n)) * b % n = a % n * (b % n) % n

Proof state:
a b n : Nat
⊢ (a % n + n * (a / n)) * (b % n + n * (b / n)) % n = a % n * (b % n) % n

Tactic:
rw [Nat.add_mul, Nat.mul_add, Nat.mul_add,
  Nat.mul_assoc, Nat.mul_assoc, ← Nat.mul_add n, add_mul_mod_self_left,
  Nat.mul_comm _ (n * (b / n)), Nat.mul_assoc, add_mul_mod_self_left]

Result:
no goals

Proof state:
a b n : Nat
⊢ (a % n + n * (a / n)) * b % n = a % n * (b % n) % n

Tactic:
rw (occs := [1]) [← mod_add_div b n]

Result:
a b n : Nat
⊢ (a % n + n * (a / n)) * (b % n + n * (b / n)) % n = a % n * (b % n) % n
-- Mathlib/CategoryTheory/Category/Cat.lean
lemma rightUnitor_hom_app {B C : Cat} (F : B ⟶ C) (X : B) : (ρ_ F).hom.app X = eqToHom (by simp) :=
  rfl

Proof state:
B C : Cat
F : B ⟶ C
X : ↑B
⊢ (F ≫ 𝟙 C).obj X = F.obj X

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Distributions/Gamma.lean
lemma gammaPDF_of_nonneg {a r x : ℝ} (hx : 0 ≤ x) :
    gammaPDF a r x = ENNReal.ofReal (r ^ a / (Gamma a) * x ^ (a-1) * exp (-(r * x)))

Proof state:
a r x : ℝ
hx : 0 ≤ x
⊢ gammaPDF a r x = ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))

Tactic:
simp only [gammaPDF_eq, if_pos hx]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem rootSet_C_mul_X_pow [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} (hn : n ≠ 0) {a : R}
    (ha : a ≠ 0) : rootSet (C a * X ^ n) S = {0}

Proof state:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
a : R
ha : a ≠ 0
⊢ (C a * X ^ n).rootSet S = {0}

Tactic:
rw [C_mul_X_pow_eq_monomial, rootSet_monomial hn ha]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem HasMFDerivWithinAt.mfderivWithin (h : HasMFDerivWithinAt I I' f s x f')
    (hxs : UniqueMDiffWithinAt I s x) : mfderivWithin I I' f s x = f'

Proof state:
case h
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivWithinAt I I' f s x f'
hxs : UniqueMDiffWithinAt I s x
x✝ : TangentSpace I x
⊢ (mfderivWithin I I' f s x) x✝ = f' x✝

Tactic:
rw [hxs.eq h h.mdifferentiableWithinAt.hasMFDerivWithinAt]

Result:
no goals

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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivWithinAt I I' f s x f'
hxs : UniqueMDiffWithinAt I s x
⊢ mfderivWithin I I' f s x = f'

Tactic:
ext

Result:
case h
𝕜 : 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : HasMFDerivWithinAt I I' f s x f'
hxs : UniqueMDiffWithinAt I s x
x✝ : TangentSpace I x
⊢ (mfderivWithin I I' f s x) x✝ = f' x✝
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_mul_const {𝕜 : Type*} [RCLike 𝕜] (r : 𝕜) (f : ℝ → 𝕜) :
    ∫ x in a..b, f x * r ∂μ = (∫ x in a..b, f x ∂μ) * r

Proof state:
a b : ℝ
μ : Measure ℝ
𝕜 : Type u_6
inst✝ : RCLike 𝕜
r : 𝕜
f : ℝ → 𝕜
⊢ ∫ (x : ℝ) in a..b, f x * r ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) * r

Tactic:
simpa only [mul_comm r] using integral_const_mul r f

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem sign_pos (ha : 0 < a) : sign a = 1

Proof state:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
a : α
ha : 0 < a
⊢ sign a = 1

Tactic:
rwa [sign_apply, if_pos]

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

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

Tactic:
cases a <;> simp_all

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem pair_diff_right (hne : a ≠ b) : ({a, b} : Set α) \ {b} = {a}

Proof state:
α : Type u
a b : α
hne : a ≠ b
⊢ {a, b} \ {b} = {a}

Tactic:
rw [pair_comm, pair_diff_left hne.symm]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
lemma exists_mem_image₂ {p : γ → Prop} :
    (∃ z ∈ image₂ f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
p : γ → Prop
⊢ (∃ z ∈ image₂ f s t, p z) ↔ ∃ x ∈ s, ∃ y ∈ t, p (f x y)

Tactic:
simp_rw [← mem_coe, coe_image₂, exists_mem_image2]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem dvd_of_dvd_mul_right_of_gcd_one {a b c : ℤ} (habc : a ∣ b * c) (hab : gcd a b = 1) :
    a ∣ c

Proof state:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd b = 1
⊢ a ∣ c

Tactic:
rw [mul_comm] at habc

Result:
a b c : ℤ
habc : a ∣ c * b
hab : a.gcd b = 1
⊢ a ∣ c

Proof state:
a b c : ℤ
habc : a ∣ c * b
hab : a.gcd b = 1
⊢ a ∣ c

Tactic:
exact dvd_of_dvd_mul_left_of_gcd_one habc hab

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem NormedAddCommGroup.tendsto_atTop' [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)]
    [NoMaxOrder α] {β : Type*} [SeminormedAddCommGroup β] {f : α → β} {b : β} :
    Tendsto f atTop (𝓝 b) ↔ ∀ ε, 0 < ε → ∃ N, ∀ n, N < n → ‖f n - b‖ < ε :=
  (atTop_basis_Ioi.tendsto_iff Metric.nhds_basis_ball).trans (by simp [dist_eq_norm])

Proof state:
α : Type u_2
inst✝⁴ : Nonempty α
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝¹ : NoMaxOrder α
β : Type u_5
inst✝ : SeminormedAddCommGroup β
f : α → β
b : β
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Set.Ioi ia, f x ∈ Metric.ball b ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N < n → ‖f n - b‖ < ε

Tactic:
simp [dist_eq_norm]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem HasProd.inv (h : HasProd f a) : HasProd (fun b ↦ (f b)⁻¹) a⁻¹

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a : α
h : HasProd f a
⊢ HasProd (fun b => (f b)⁻¹) a⁻¹

Tactic:
simpa only using h.map (MonoidHom.id α)⁻¹ continuous_inv

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivWithinAt.iterate {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivWithinAt f f' s x)
    (hx : f x = x) (hs : MapsTo f s s) (n : ℕ) : HasDerivWithinAt f^[n] (f' ^ n) s x

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
this : HasFDerivWithinAt f^[n] (smulRight 1 f' ^ n) s x
⊢ HasDerivWithinAt f^[n] (f' ^ n) s x

Tactic:
rwa [ContinuousLinearMap.smulRight_one_pow] at this

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
⊢ HasDerivWithinAt f^[n] (f' ^ n) s x

Tactic:
have := HasFDerivWithinAt.iterate hf hx hs n

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
f' : 𝕜
hf : HasDerivWithinAt f f' s x
hx : f x = x
hs : MapsTo f s s
n : ℕ
this : HasFDerivWithinAt f^[n] (smulRight 1 f' ^ n) s x
⊢ HasDerivWithinAt f^[n] (f' ^ n) s x
-- Mathlib/Algebra/MvPolynomial/Basic.lean
@[simp]
lemma X_mul_mem_coeffsIn : X s * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
p : MvPolynomial σ S
s : σ
⊢ X s * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Tactic:
simp [mul_comm]

Result:
no goals
-- Mathlib/Order/Monotone/MonovaryOrder.lean
lemma monovaryOn_iff_exists_antitoneOn :
    MonovaryOn f g s ↔ ∃ (_ : LinearOrder ι), AntitoneOn f s ∧ AntitoneOn g s

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s ↔ ∃ x, AntitoneOn f s ∧ AntitoneOn g s

Tactic:
simp_rw [← antivaryOn_toDual_left, antivaryOn_iff_exists_monotoneOn_antitoneOn,
  monotoneOn_toDual_comp_iff]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderivWithin_zero_of_nmem_closure (h : x ∉ closure s) : fderivWithin 𝕜 f s x = 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : x ∉ closure s
⊢ fderivWithin 𝕜 f s x = 0

Tactic:
rw [fderivWithin, if_pos (hasFDerivWithinAt_of_nmem_closure h)]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem smul_vec2 {R : Type*} [SMul R α] (x : R) (a₀ a₁ : α) :
    x • ![a₀, a₁] = ![x • a₀, x • a₁]

Proof state:
α : Type u
R : Type u_1
inst✝ : SMul R α
x : R
a₀ a₁ : α
⊢ x • ![a₀, a₁] = ![x • a₀, x • a₁]

Tactic:
rw [smul_cons, smul_cons, smul_empty]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem exists_conts_a_of_num {A : K} (nth_num_eq : g.nums n = A) :
    ∃ conts, g.conts n = conts ∧ conts.a = A

Proof state:
K : Type u_1
g : GenContFract K
n : ℕ
inst✝ : DivisionRing K
A : K
nth_num_eq : g.nums n = A
⊢ ∃ conts, g.conts n = conts ∧ conts.a = A

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean
@[to_additive]
lemma right_mul_prod_Ioo (h : a < b) : f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
a b : α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x

Tactic:
rw [Ioc_eq_cons_Ioo h, prod_cons]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem pairwise_disjoint_Ioc_zpow :
    Pairwise (Disjoint on fun n : ℤ => Ioc (b ^ n) (b ^ (n + 1)))

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
b : α
⊢ Pairwise (Disjoint on fun n => Ioc (b ^ n) (b ^ (n + 1)))

Tactic:
simpa only [one_mul] using pairwise_disjoint_Ioc_mul_zpow 1 b

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
@[simp]
lemma preimage_image (e : α ≃ᵐ β) (s : Set α) : e ⁻¹' (e '' s) = s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set α
⊢ ⇑e ⁻¹' (⇑e '' s) = s

Tactic:
rw [← coe_toEquiv, Equiv.preimage_image]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_add_zsmul' (a b : α) (m : ℤ) :
    toIcoMod hp (a + m • p) b = toIcoMod hp a b + m • p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp (a + m • p) b = toIcoMod hp a b + m • p

Tactic:
simp only [toIcoMod, toIcoDiv_add_zsmul', sub_smul, sub_add]

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map_map₂_right_anticomm {f : α → β' → γ} {g : β → β'} {f' : β → α → δ} {g' : δ → γ}
    (h_right_anticomm : ∀ a b, f a (g b) = g' (f' b a)) :
    map₂ f a (b.map g) = (map₂ f' b a).map g'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
β' : Type u_6
f : α → β' → γ
g : β → β'
f' : β → α → δ
g' : δ → γ
h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)
⊢ map₂ f a (Option.map g b) = Option.map g' (map₂ f' b a)

Tactic:
cases a <;> cases b <;> simp [h_right_anticomm]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem minimalPeriod_eq_zero_iff_nmem_periodicPts : minimalPeriod f x = 0 ↔ x ∉ periodicPts f

Proof state:
α : Type u_1
f : α → α
x : α
⊢ minimalPeriod f x = 0 ↔ x ∉ periodicPts f

Tactic:
rw [← minimalPeriod_pos_iff_mem_periodicPts, not_lt, nonpos_iff_eq_zero]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem _root_.LinearIsometry.angle_map {E F : Type*} [NormedAddCommGroup E] [NormedAddCommGroup F]
    [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] (f : E →ₗᵢ[ℝ] F) (u v : E) :
    angle (f u) (f v) = angle u v

Proof state:
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →ₗᵢ[ℝ] F
u v : E
⊢ angle (f u) (f v) = angle u v

Tactic:
rw [angle, angle, f.inner_map_map, f.norm_map, f.norm_map]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp] lemma cast_pos : (0 : K) < q ↔ 0 < q

Proof state:
q : ℚ
K : Type u_5
inst✝ : LinearOrderedField K
⊢ 0 < ↑q ↔ 0 < q

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_le_left (hy : 0 ≤ y) : √x ≤ y ↔ x ≤ y ^ 2

Proof state:
x y : ℝ
hy : 0 ≤ y
⊢ √x ≤ y ↔ x ≤ y ^ 2

Tactic:
rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff_le_sq, sq, ← Real.toNNReal_mul hy,
  Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[reassoc (attr := simp)]
lemma ιTotalOrZero_map (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) :
    K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂ ≫ (total.map φ c₁₂).f i₁₂ =
      (φ.f i₁).f i₂ ≫ L.ιTotalOrZero c₁₂ i₁ i₂ i₁₂

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
⊢ K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂ ≫ (total.map φ c₁₂).f i₁₂ = (φ.f i₁).f i₂ ≫ L.ιTotalOrZero c₁₂ i₁ i₂ i₁₂

Tactic:
simp [total.map, ιTotalOrZero]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_right' {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂}
    {h₂₂ : X₂₂ ⟶ X₂₃} {h₁₃ : X₁₁ ⟶ X₁₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃}
    (s : IsPullback h₁₃ v₁₁ v₁₃ (h₂₁ ≫ h₂₂)) (t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂) :
    IsPullback (t.lift h₁₃ (v₁₁ ≫ h₂₁) (by rw [s.w, Category.assoc])) v₁₁ v₁₂ h₂₁ :=
  of_right ((t.lift_fst _ _ _) ▸ s) (t.lift_snd _ _ _) t

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₂ : X₂₂ ⟶ X₂₃
h₁₃ : X₁₁ ⟶ X₁₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPullback h₁₃ v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂
⊢ h₁₃ ≫ v₁₃ = (v₁₁ ≫ h₂₁) ≫ h₂₂

Tactic:
rw [s.w, Category.assoc]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma lintegral_stieltjesOfMeasurableRat [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν)
    (a : α) (x : ℝ) :
    ∫⁻ b, ENNReal.ofReal (stieltjesOfMeasurableRat f hf.measurable (a, b) x) ∂(ν a)
      = κ a (univ ×ˢ Iic x)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
⊢ ∫⁻ (b : β), ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) ∂ν a = (κ a) (univ ×ˢ Iic x)

Tactic:
rw [← setLIntegral_univ, setLIntegral_stieltjesOfMeasurableRat hf _ _ MeasurableSet.univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_gcd_self_left_left (m n : Nat) : gcd (gcd m n) m = gcd m n

Proof state:
m n : Nat
⊢ (m.gcd n).gcd m = m.gcd n

Tactic:
rw [gcd_comm m n, gcd_gcd_self_left_right]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_addY (P Q : Fin 3 → R) :
    (W'.map f).toJacobian.addY (f ∘ P) (f ∘ Q) = f (W'.addY P Q)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P Q : Fin 3 → R
⊢ (map W' f).toJacobian.addY (⇑f ∘ P) (⇑f ∘ Q) = f (W'.addY P Q)

Tactic:
simp only [addY, negY_eq, map_negAddY, map_addX, map_addZ]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P Q : Fin 3 → R
⊢ -f (W'.negAddY P Q) - (map W' f).toJacobian.a₁ * f (W'.addX P Q) * f (addZ P Q) -
      (map W' f).toJacobian.a₃ * f (addZ P Q) ^ 3 =
    f (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * addZ P Q ^ 3)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P Q : Fin 3 → R
⊢ -f (W'.negAddY P Q) - (map W' f).toJacobian.a₁ * f (W'.addX P Q) * f (addZ P Q) -
      (map W' f).toJacobian.a₃ * f (addZ P Q) ^ 3 =
    f (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * addZ P Q ^ 3)

Tactic:
map_simp

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
@[simp]
lemma denom_S (z : ℍ) : denom S z = z

Proof state:
z : ℍ
⊢ denom (↑S) z = ↑z

Tactic:
simp only [S, denom_apply, of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one,
  cons_val_one, head_fin_const, Int.cast_one, one_mul, head_cons, Int.cast_zero, add_zero]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
lemma sum_pow' (s : Finset ι') (f : ι' → α) (n : ℕ) :
    (∑ a ∈ s, f a) ^ n = ∑ p ∈ piFinset fun _i : Fin n ↦ s, ∏ i, f (p i)

Proof state:
case h.e'_2
ι' : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι'
f : ι' → α
n : ℕ
⊢ (∑ a ∈ s, f a) ^ n = ∏ i : Fin n, ∑ j ∈ s, f j

Tactic:
simp

Result:
no goals

Proof state:
ι' : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι'
f : ι' → α
n : ℕ
⊢ (∑ a ∈ s, f a) ^ n = ∑ p ∈ piFinset fun _i => s, ∏ i : Fin n, f (p i)

Tactic:
convert @prod_univ_sum (Fin n) _ _ _ _ _ (fun _i ↦ s) fun _i d ↦ f d

Result:
case h.e'_2
ι' : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι'
f : ι' → α
n : ℕ
⊢ (∑ a ∈ s, f a) ^ n = ∏ i : Fin n, ∑ j ∈ s, f j
-- Mathlib/Data/PNat/Prime.lean
theorem gcd_eq_right_iff_dvd {m n : ℕ+} : m ∣ n ↔ n.gcd m = m

Proof state:
m n : ℕ+
⊢ m ∣ n ↔ m.gcd n = m

Tactic:
apply gcd_eq_left_iff_dvd

Result:
no goals

Proof state:
m n : ℕ+
⊢ m ∣ n ↔ n.gcd m = m

Tactic:
rw [gcd_comm]

Result:
m n : ℕ+
⊢ m ∣ n ↔ m.gcd n = m
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem frontier_setOf_lt_im (a : ℝ) : frontier { z : ℂ | a < z.im } = { z | z.im = a }

Proof state:
a : ℝ
⊢ frontier {z | a < z.im} = {z | z.im = a}

Tactic:
simpa only [frontier_Ioi] using frontier_preimage_im (Ioi a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem add_eq_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : (a + b = c + d) = (a + (b - d) = c)

Proof state:
a c b d : Nat
h : b ≥ d
⊢ (a + b = c + d) = (a + (b - d) = c)

Tactic:
rw [@Eq.comm _ (a + b) _, add_eq_add_le c a h, @Eq.comm _ _ c]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_of_isEmpty [IsEmpty α] (s : Finset α) : ∏ i ∈ s, f i = 1

Proof state:
α : Type u_3
β : Type u_4
f : α → β
inst✝¹ : CommMonoid β
inst✝ : IsEmpty α
s : Finset α
⊢ ∏ i ∈ s, f i = 1

Tactic:
rw [eq_empty_of_isEmpty s, prod_empty]

Result:
no goals