harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Ioc_iff_integrableOn_Ioo :
    IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioo a b) μ :=
  integrableOn_Ioc_iff_integrableOn_Ioo' (by rw [measure_singleton]; exact ENNReal.zero_ne_top)

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ μ {b} ≠ ⊤

Tactic:
rw [measure_singleton]

Result:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤

Tactic:
exact ENNReal.zero_ne_top

Result:
no goals
-- Mathlib/Order/Directed.lean
theorem directedOn_pair' (h : Reflexive r) {a b : α} (hab : a ≼ b) :
    DirectedOn r ({b, a} : Set α)

Proof state:
α : Type u
r : α → α → Prop
h : Reflexive r
a b : α
hab : r a b
⊢ DirectedOn r {b, a}

Tactic:
rw [Set.pair_comm]

Result:
α : Type u
r : α → α → Prop
h : Reflexive r
a b : α
hab : r a b
⊢ DirectedOn r {a, b}

Proof state:
α : Type u
r : α → α → Prop
h : Reflexive r
a b : α
hab : r a b
⊢ DirectedOn r {a, b}

Tactic:
apply directedOn_pair h hab

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_pos_of_lt_neg_one (hx : x < -1) : 0 < log x

Proof state:
x : ℝ
hx : x < -1
⊢ 0 < log (-x)

Tactic:
have : 1 < -x := by linarith

Result:
x : ℝ
hx : x < -1
this : 1 < -x
⊢ 0 < log (-x)

Proof state:
x : ℝ
hx : x < -1
this : 1 < -x
⊢ 0 < log (-x)

Tactic:
exact log_pos this

Result:
no goals

Proof state:
x : ℝ
hx : x < -1
⊢ 0 < log x

Tactic:
rw [← neg_neg x, log_neg_eq_log]

Result:
x : ℝ
hx : x < -1
⊢ 0 < log (-x)

Proof state:
x : ℝ
hx : x < -1
⊢ 1 < -x

Tactic:
linarith

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_eq_getD [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} {h} :
    m.get a h = m.getD a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h✝ : m.WF
a : α
fallback : β a
h : a ∈ m
⊢ m.get a h = m.getD a fallback

Tactic:
simp_to_raw using Raw₀.get_eq_getD

Result:
no goals
-- Mathlib/Data/Real/ENatENNReal.lean
@[simp, norm_cast] lemma toENNReal_eq_top : (n : ℝ≥0∞) = ∞ ↔ n = ⊤

Proof state:
n : ℕ∞
⊢ ↑n = ⊤ ↔ n = ⊤

Tactic:
simp [← toENNReal_inj]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem eq_spanSingleton_mul {x : P} {I J : FractionalIdeal S P} :
    I = spanSingleton _ x * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
I J : FractionalIdeal S P
⊢ I = spanSingleton S x * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I

Tactic:
simp only [le_antisymm_iff, le_spanSingleton_mul_iff, spanSingleton_mul_le_iff]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem right_ne_of_oangle_sign_eq_one {p₁ p₂ p₃ : P} (h : (∡ p₁ p₂ p₃).sign = 1) : p₃ ≠ p₂ :=
  right_ne_of_oangle_sign_ne_zero (h.symm ▸ by decide : (∡ p₁ p₂ p₃).sign ≠ 0)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : (∡ p₁ p₂ p₃).sign = 1
⊢ 1 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem mem_map {x : L} (hx : x ∈ I) : f x ∈ map f I

Proof state:
case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
hx : x ∈ I
⊢ f x ∈ ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)

Tactic:
use x

Result:
case h
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
hx : x ∈ I
⊢ x ∈ ↑(toLieSubalgebra R L I).toSubmodule ∧ ↑f x = f x

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
hx : x ∈ I
⊢ f x ∈ map f I

Tactic:
apply LieSubmodule.subset_lieSpan

Result:
case a
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
hx : x ∈ I
⊢ f x ∈ ↑(Submodule.map (↑f) (toLieSubalgebra R L I).toSubmodule)

Proof state:
case h
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
x : L
hx : x ∈ I
⊢ x ∈ ↑(toLieSubalgebra R L I).toSubmodule ∧ ↑f x = f x

Tactic:
exact ⟨hx, rfl⟩

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma RepresentableBy.homEquiv_eq {F : Cᵒᵖ ⥤ Type v} {Y : C} (e : F.RepresentableBy Y)
    {X : C} (f : X ⟶ Y) :
    e.homEquiv f = F.map f.op (e.homEquiv (𝟙 Y))

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e : F.RepresentableBy Y
X : C
f : X ⟶ Y
⊢ e.homEquiv f = F.map f.op (e.homEquiv (𝟙 Y))

Tactic:
conv_lhs => rw [← Category.comp_id f, e.homEquiv_comp]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem jacobson_mono {I J : Ideal R} : I ≤ J → I.jacobson ≤ J.jacobson

Proof state:
R : Type u
inst✝ : Ring R
I J : Ideal R
⊢ I ≤ J → I.jacobson ≤ J.jacobson

Tactic:
intro h x hx

Result:
R : Type u
inst✝ : Ring R
I J : Ideal R
h : I ≤ J
x : R
hx : x ∈ I.jacobson
⊢ x ∈ J.jacobson

Proof state:
R : Type u
inst✝ : Ring R
I J : Ideal R
h : I ≤ J
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1
⊢ ∀ ⦃I : Ideal R⦄, I ∈ {J_1 | J ≤ J_1 ∧ J_1.IsMaximal} → x ∈ I

Tactic:
exact fun K ⟨hK, hK_max⟩ => hx ⟨Trans.trans h hK, hK_max⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
I J : Ideal R
h : I ≤ J
x : R
hx : x ∈ I.jacobson
⊢ x ∈ J.jacobson

Tactic:
erw [mem_sInf] at hx ⊢

Result:
R : Type u
inst✝ : Ring R
I J : Ideal R
h : I ≤ J
x : R
hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1
⊢ ∀ ⦃I : Ideal R⦄, I ∈ {J_1 | J ≤ J_1 ∧ J_1.IsMaximal} → x ∈ I
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[simp] lemma ofZeros_f' (hf : S.f = 0) (hg : S.g = 0) :
    (ofZeros S hf hg).f' = 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).f' = 0

Tactic:
rw [← cancel_mono ((ofZeros S hf hg).i), zero_comp, f'_i, hf]

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem countable_setOf_covBy_left [OrderTopology α] [SecondCountableTopology α] :
    Set.Countable { x : α | ∃ y, y ⋖ x }

Proof state:
case h.e'_2.h.h.e'_2.h.h.h.e'_2.h.h.a
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
e_1✝ : α = αᵒᵈ
x✝¹ x✝ : α
⊢ x✝ ⋖ x✝¹ ↔ x✝¹ ⋖ x✝

Tactic:
exact toDual_covBy_toDual_iff.symm

Result:
no goals

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ {x | ∃ y, y ⋖ x}.Countable

Tactic:
convert countable_setOf_covBy_right (α := αᵒᵈ) using 5

Result:
case h.e'_2.h.h.e'_2.h.h.h.e'_2.h.h.a
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
e_1✝ : α = αᵒᵈ
x✝¹ x✝ : α
⊢ x✝ ⋖ x✝¹ ↔ x✝¹ ⋖ x✝
-- Mathlib/Data/Fintype/List.lean
theorem mem_lists_iff (s : Multiset α) (l : List α) : l ∈ lists s ↔ s = ⟦l⟧

Proof state:
α : Type u_1
s : Multiset α
l : List α
⊢ l ∈ s.lists ↔ s = ⟦l⟧

Tactic:
induction s using Quotient.inductionOn

Result:
case h
α : Type u_1
l a✝ : List α
⊢ l ∈ lists ⟦a✝⟧ ↔ ⟦a✝⟧ = ⟦l⟧

Proof state:
case h
α : Type u_1
l a✝ : List α
⊢ l ∈ lists ⟦a✝⟧ ↔ ⟦a✝⟧ = ⟦l⟧

Tactic:
simpa using perm_comm

Result:
no goals
-- Mathlib/Data/Nat/Multiplicity.lean
theorem dvd_choose_pow (hp : Prime p) (hk : k ≠ 0) (hkp : k ≠ p ^ n) : p ∣ (p ^ n).choose k

Proof state:
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : emultiplicity p ((p ^ n).choose k) = 0
H : p ^ n ∣ k ∧ ¬p ^ (n + 1) ∣ k
⊢ p ^ n ∣ k

Tactic:
exact H.1

Result:
no goals

Proof state:
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : emultiplicity p ((p ^ n).choose k) = 0
H : emultiplicity p ((p ^ n).choose k) + emultiplicity p k = ↑n
⊢ p ^ n ∣ k

Tactic:
rw [h, zero_add, emultiplicity_eq_coe] at H

Result:
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : emultiplicity p ((p ^ n).choose k) = 0
H : p ^ n ∣ k ∧ ¬p ^ (n + 1) ∣ k
⊢ p ^ n ∣ k

Proof state:
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
⊢ p ∣ (p ^ n).choose k

Tactic:
refine emultiplicity_ne_zero.1 fun h => hkp.not_le <| Nat.le_of_dvd hk.bot_lt ?_

Result:
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : emultiplicity p ((p ^ n).choose k) = 0
⊢ p ^ n ∣ k

Proof state:
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : emultiplicity p ((p ^ n).choose k) = 0
⊢ p ^ n ∣ k

Tactic:
have H := hp.emultiplicity_choose_prime_pow_add_emultiplicity hkp.le hk

Result:
case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
h : emultiplicity p ((p ^ n).choose k) = 0
H : emultiplicity p ((p ^ n).choose k) + emultiplicity p k = ↑n
⊢ p ^ n ∣ k

Proof state:
case inl
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : p ^ n < k
⊢ p ∣ (p ^ n).choose k

Tactic:
simp [choose_eq_zero_of_lt hkp]

Result:
no goals

Proof state:
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp : k ≠ p ^ n
⊢ p ∣ (p ^ n).choose k

Tactic:
obtain hkp | hkp := hkp.symm.lt_or_lt

Result:
case inl
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : p ^ n < k
⊢ p ∣ (p ^ n).choose k

case inr
p n k : ℕ
hp : Prime p
hk : k ≠ 0
hkp✝ : k ≠ p ^ n
hkp : k < p ^ n
⊢ p ∣ (p ^ n).choose k
-- Mathlib/Topology/Constructions.lean
theorem IsClosed.trans (ht : IsClosed t) (hs : IsClosed s) : IsClosed (t : Set X)

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
s' : Set X
hs' : IsClosed s'
ht : IsClosed (s ↓∩ s')
⊢ IsClosed (s ∩ s')

Tactic:
exact hs.inter hs'

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
ht : IsClosed t
hs : IsClosed s
⊢ IsClosed (Subtype.val '' t)

Tactic:
rcases isClosed_induced_iff.mp ht with ⟨s', hs', rfl⟩

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
s' : Set X
hs' : IsClosed s'
ht : IsClosed (s ↓∩ s')
⊢ IsClosed (Subtype.val '' s ↓∩ s')

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
s' : Set X
hs' : IsClosed s'
ht : IsClosed (s ↓∩ s')
⊢ IsClosed (Subtype.val '' s ↓∩ s')

Tactic:
rw [Subtype.image_preimage_coe]

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
s' : Set X
hs' : IsClosed s'
ht : IsClosed (s ↓∩ s')
⊢ IsClosed (s ∩ s')
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂Hom_congr {f₁ f₂ : R →+* S₁} {g₁ g₂ : σ → S₁} {p₁ p₂ : MvPolynomial σ R} :
    f₁ = f₂ → g₁ = g₂ → p₁ = p₂ → eval₂Hom f₁ g₁ p₁ = eval₂Hom f₂ g₂ p₂

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f₁ : R →+* S₁
g₁ : σ → S₁
p₁ : MvPolynomial σ R
⊢ (eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₁ g₁) p₁

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f₁ f₂ : R →+* S₁
g₁ g₂ : σ → S₁
p₁ p₂ : MvPolynomial σ R
⊢ f₁ = f₂ → g₁ = g₂ → p₁ = p₂ → (eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₂ g₂) p₂

Tactic:
rintro rfl rfl rfl

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f₁ : R →+* S₁
g₁ : σ → S₁
p₁ : MvPolynomial σ R
⊢ (eval₂Hom f₁ g₁) p₁ = (eval₂Hom f₁ g₁) p₁
-- Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
theorem OrderIso.mulRight₀'_symm {a : α} (ha : a ≠ 0) :
    (OrderIso.mulRight₀' ha).symm = OrderIso.mulRight₀' (inv_ne_zero ha)

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
⊢ (mulRight₀' ha).symm = mulRight₀' ⋯

Tactic:
ext

Result:
case h.h
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
x✝ : α
⊢ (mulRight₀' ha).symm x✝ = (mulRight₀' ⋯) x✝

Proof state:
case h.h
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
x✝ : α
⊢ (mulRight₀' ha).symm x✝ = (mulRight₀' ⋯) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem card_insert {a : α} (s : Set α) [Fintype s] (h : a ∉ s)
    {d : Fintype (insert a s : Set α)} : @Fintype.card _ d = Fintype.card s + 1

Proof state:
α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑(insert a s)

Tactic:
congr!

Result:
no goals

Proof state:
α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑s + 1

Tactic:
rw [← card_fintypeInsertOfNotMem s h]

Result:
α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑(insert a s)
-- Mathlib/Algebra/Order/Interval/Set/Instances.lean
theorem one_sub_mem {t : β} (ht : t ∈ Ioo (0 : β) 1) : 1 - t ∈ Ioo (0 : β) 1

Proof state:
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : 0 < t ∧ t < 1
⊢ 0 < 1 - t ∧ 1 - t < 1

Tactic:
refine ⟨sub_pos.2 ht.2, ?_⟩

Result:
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : 0 < t ∧ t < 1
⊢ 1 - t < 1

Proof state:
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : 0 < t ∧ t < 1
⊢ 1 - t < 1

Tactic:
exact lt_of_le_of_ne ((sub_le_self_iff 1).2 ht.1.le) (mt sub_eq_self.mp ht.1.ne')

Result:
no goals

Proof state:
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : t ∈ Ioo 0 1
⊢ 1 - t ∈ Ioo 0 1

Tactic:
rw [mem_Ioo] at *

Result:
β : Type u_2
inst✝ : OrderedRing β
t : β
ht : 0 < t ∧ t < 1
⊢ 0 < 1 - t ∧ 1 - t < 1
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
lemma add_eq_of_lt {q r : ℚ} (hqr : q + r ≠ 0)
    (hq : q ≠ 0) (hr : r ≠ 0) (hval : padicValRat p q < padicValRat p r) :
    padicValRat p (q + r) = padicValRat p q

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hval : padicValRat p q < padicValRat p r
⊢ padicValRat p (q + r) = padicValRat p q

Tactic:
rw [add_eq_min hqr hq hr (ne_of_lt hval), min_eq_left (le_of_lt hval)]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem isUpperSet_iff_Ici_subset : IsUpperSet s ↔ ∀ ⦃a⦄, a ∈ s → Ici a ⊆ s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Ici a ⊆ s

Tactic:
simp [IsUpperSet, subset_def, @forall_swap (_ ∈ s)]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem measurableSet_preimage (e : α ≃ᵐ β) {s : Set β} :
    MeasurableSet (e ⁻¹' s) ↔ MeasurableSet s :=
  ⟨fun h => by simpa only [symm_preimage_preimage] using e.symm.measurable h, fun h =>
    e.measurable h⟩

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

Tactic:
simpa only [symm_preimage_preimage] using e.symm.measurable h

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[gcongr, bound]
lemma div_lt_div_of_pos_left (ha : 0 < a) (hc : 0 < c) (h : c < b) : a / b < a / c

Proof state:
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : ZeroLEOneClass G₀
inst✝² : PosMulReflectLT G₀
a b c : G₀
inst✝¹ : MulPosStrictMono G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
hc : 0 < c
h : c < b
⊢ a / b < a / c

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]

Result:
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : ZeroLEOneClass G₀
inst✝² : PosMulReflectLT G₀
a b c : G₀
inst✝¹ : MulPosStrictMono G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
hc : 0 < c
h : c < b
⊢ a * b⁻¹ < a * c⁻¹

Proof state:
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : ZeroLEOneClass G₀
inst✝² : PosMulReflectLT G₀
a b c : G₀
inst✝¹ : MulPosStrictMono G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
hc : 0 < c
h : c < b
⊢ a * b⁻¹ < a * c⁻¹

Tactic:
exact mul_lt_mul_of_pos_left ((inv_lt_inv₀ (hc.trans h) hc).2 h) ha

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Even.lean
lemma two_not_dvd_two_mul_add_one (n : ℕ) : ¬2 ∣ 2 * n + 1

Proof state:
n : ℕ
⊢ ¬2 ∣ 2 * n + 1

Tactic:
simp [add_mod]

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
theorem reprW_hom_app (F : Cᵒᵖ ⥤ Type v₁) [F.IsRepresentable]
    (X : Cᵒᵖ) (f : unop X ⟶ F.reprX) :
    F.reprW.hom.app X f = F.map f.op F.reprx

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : F.IsRepresentable
X : Cᵒᵖ
f : unop X ⟶ F.reprX
⊢ F.reprW.hom.app X f = F.map f.op F.reprx

Tactic:
apply RepresentableBy.homEquiv_eq

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem mapOfCompatibleSMul_surjective : Function.Surjective (mapOfCompatibleSMul R A M N) :=
  fun x ↦ x.induction_on (⟨0, map_zero _⟩) (fun m n ↦ ⟨_, mapOfCompatibleSMul_tmul ..⟩)
    fun _ _ ⟨x, hx⟩ ⟨y, hy⟩ ↦ ⟨x + y, by simpa using congr($hx + $hy)⟩

Proof state:
R : Type u_1
inst✝⁹ : CommSemiring R
A : Type u_4
M : Type u_5
N : Type u_6
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring A
inst✝³ : Module A M
inst✝² : Module A N
inst✝¹ : SMulCommClass R A M
inst✝ : CompatibleSMul R A M N
x✝⁴ x✝³ x✝² : M ⊗[R] N
x✝¹ : ∃ a, (mapOfCompatibleSMul R A M N) a = x✝³
x✝ : ∃ a, (mapOfCompatibleSMul R A M N) a = x✝²
x : M ⊗[A] N
hx : (mapOfCompatibleSMul R A M N) x = x✝³
y : M ⊗[A] N
hy : (mapOfCompatibleSMul R A M N) y = x✝²
⊢ (mapOfCompatibleSMul R A M N) (x + y) = x✝³ + x✝²

Tactic:
simpa using congr($hx + $hy)

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem HasFDerivWithinAt.hasFDerivAt (h : HasFDerivWithinAt f f' s x) (hs : s ∈ 𝓝 x) :
    HasFDerivAt f f' x

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
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hs : s ∈ 𝓝 x
⊢ HasFDerivAt f f' x

Tactic:
rwa [← univ_inter s, hasFDerivWithinAt_inter hs, hasFDerivWithinAt_univ] at h

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Submodule.lean
theorem Module.subsingleton_of_localization_maximal
    (h : ∀ (P : Ideal R) [P.IsMaximal], Subsingleton (Mₚ P)) :
    Subsingleton M

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
h : ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (Mₚ P)
⊢ Subsingleton M

Tactic:
rw [subsingleton_iff_forall_eq 0]

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
h : ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (Mₚ P)
⊢ ∀ (y : M), y = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
h : ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (Mₚ P)
x : M
⊢ x = 0

Tactic:
exact Module.eq_of_localization_maximal Mₚ f x 0 fun _ _ ↦ Subsingleton.elim _ _

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
h : ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (Mₚ P)
⊢ ∀ (y : M), y = 0

Tactic:
intro x

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [inst : P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
h : ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (Mₚ P)
x : M
⊢ x = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_isSome {xs : Array α} {p : α → Bool} :
    (xs.findIdx? p).isSome = xs.any p

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
⊢ (findIdx? p xs).isSome = xs.any p

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ (findIdx? p { toList := xs }).isSome = { toList := xs }.any p

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : List α
⊢ (findIdx? p { toList := xs }).isSome = { toList := xs }.any p

Tactic:
simp [List.findIdx?_isSome]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Ultra.lean
theorem IsUltrametricDist.of_normedAlgebra [NormedDivisionRing L] [NormedAlgebra K L]
    [h : IsUltrametricDist K] : IsUltrametricDist L

Proof state:
K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedDivisionRing L
inst✝ : NormedAlgebra K L
h : IsUltrametricDist K
⊢ IsUltrametricDist L

Tactic:
rw [isUltrametricDist_iff_forall_norm_natCast_le_one] at h ⊢

Result:
K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedDivisionRing L
inst✝ : NormedAlgebra K L
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
⊢ ∀ (n : ℕ), ‖↑n‖ ≤ 1

Proof state:
K : Type u_1
L : Type u_2
inst✝² : NormedField K
inst✝¹ : NormedDivisionRing L
inst✝ : NormedAlgebra K L
h : ∀ (n : ℕ), ‖↑n‖ ≤ 1
⊢ ∀ (n : ℕ), ‖↑n‖ ≤ 1

Tactic:
exact fun n => (algebraMap.coe_natCast (R := K) (A := L) n) ▸ norm_algebraMap' L (n : K) ▸ h n

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem not_rankPos_iff : ¬RankPos M ↔ M = loopyOn M.E

Proof state:
α : Type u_1
M : Matroid α
⊢ ¬M.RankPos ↔ M = loopyOn M.E

Tactic:
rw [rankPos_iff, not_iff_comm, empty_isBase_iff]

Result:
no goals
-- Mathlib/Data/Pi/Interval.lean
theorem card_Ico : #(Ico a b) = ∏ i, #(Icc (a i) (b i)) - 1

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Ico a b) = ∏ i : ι, #(Icc (a i) (b i)) - 1

Tactic:
rw [card_Ico_eq_card_Icc_sub_one, card_Icc]

Result:
no goals