harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
    (h : m.WF) (h₁ : k ∉ m) (h₂ : (f (m.get? k)).isNone)  :
    (m.alter k f).size = m.size

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ m.contains k = false → (f (m.get? k)).isNone = true → (m.alter k f).size = m.size

Tactic:
simp_to_raw using Raw₀.size_alter_eq_self_of_not_mem

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ ¬k ∈ m → (f (m.get? k)).isNone = true → (m.alter k f).size = m.size

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ m.contains k = false → (f (m.get? k)).isNone = true → (m.alter k f).size = m.size

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
h₁ : ¬k ∈ m
h₂ : (f (m.get? k)).isNone = true
⊢ (m.alter k f).size = m.size

Tactic:
revert h₁ h₂

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ ¬k ∈ m → (f (m.get? k)).isNone = true → (m.alter k f).size = m.size
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_set {l : List α} {i j} {a} (h) :
    (set l i a)[j]'h = if i = j then a else l[j]'(length_set .. ▸ h)

Proof state:
α : Type u_1
l : List α
i j : Nat
a : α
h✝ : j < (l.set i a).length
h : ¬i = j
⊢ (l.set i a)[j] = if i = j then a else l[j]

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
l : List α
i j : Nat
a : α
h : j < (l.set i a).length
⊢ (l.set i a)[j] = if i = j then a else l[j]

Tactic:
if h : i = j then
  subst h; simp only [getElem_set_self, ↓reduceIte]
else
  simp [h]

Result:
no goals

Proof state:
α : Type u_1
l : List α
i j : Nat
a : α
h✝ : j < (l.set i a).length
h : i = j
⊢ (l.set i a)[j] = if i = j then a else l[j]

Tactic:
subst h

Result:
α : Type u_1
l : List α
i : Nat
a : α
h : i < (l.set i a).length
⊢ (l.set i a)[i] = if i = i then a else l[i]

Proof state:
α : Type u_1
l : List α
i : Nat
a : α
h : i < (l.set i a).length
⊢ (l.set i a)[i] = if i = i then a else l[i]

Tactic:
simp only [getElem_set_self, ↓reduceIte]

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra/Cardinality.lean
theorem cardinalMk_le_max : #(FreeAlgebra R X) ≤ #R ⊔ #X ⊔ ℵ₀

Proof state:
R : Type u
inst✝ : CommSemiring R
X : Type u
⊢ #(FreeAlgebra R X) ≤ #R ⊔ #X ⊔ ℵ₀

Tactic:
simpa using cardinalMk_le_max_lift R X

Result:
no goals
-- Mathlib/Topology/SeparatedMap.lean
theorem eq_of_comp_eq
    [PreconnectedSpace A] (h₁ : Continuous g₁) (h₂ : Continuous g₂)
    (he : p ∘ g₁ = p ∘ g₂) (a : A) (ha : g₁ a = g₂ a) : g₁ = g₂ := funext fun a' ↦ by
  apply (IsClopen.eq_univ ⟨sep.isClosed_eqLocus h₁ h₂ he, inj.isOpen_eqLocus h₁ h₂ he⟩ ⟨a, ha⟩).symm
    ▸ Set.mem_univ a'

Proof state:
X : Type u_1
E : Type u_2
A : Type u_3
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace A
p : E → X
g₁ g₂ : A → E
sep : IsSeparatedMap p
inj : IsLocallyInjective p
inst✝ : PreconnectedSpace A
h₁ : Continuous g₁
h₂ : Continuous g₂
he : p ∘ g₁ = p ∘ g₂
a : A
ha : g₁ a = g₂ a
a' : A
⊢ g₁ a' = g₂ a'

Tactic:
apply (IsClopen.eq_univ ⟨sep.isClosed_eqLocus h₁ h₂ he, inj.isOpen_eqLocus h₁ h₂ he⟩ ⟨a, ha⟩).symm
  ▸ Set.mem_univ a'

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Basic.lean
theorem transitionMap_comp_eval {m n : ℕ} (hmn : m ≤ n) :
    transitionMap I M hmn ∘ₗ eval I M n = eval I M m

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
hmn : m ≤ n
⊢ transitionMap I M hmn ∘ₗ eval I M n = eval I M m

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
hmn : m ≤ n
x : AdicCompletion I M
⊢ (transitionMap I M hmn ∘ₗ eval I M n) x = (eval I M m) x

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m n : ℕ
hmn : m ≤ n
x : AdicCompletion I M
⊢ (transitionMap I M hmn ∘ₗ eval I M n) x = (eval I M m) x

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem leftMoves_neg_cases {x : PGame} (k) {P : (-x).LeftMoves → Prop}
    (h : ∀ i, P <| toLeftMovesNeg i) :
    P k

Proof state:
x : PGame
k : (-x).LeftMoves
P : (-x).LeftMoves → Prop
h : ∀ (i : x.RightMoves), P (toLeftMovesNeg i)
⊢ P (toLeftMovesNeg (toLeftMovesNeg.symm k))

Tactic:
exact h _

Result:
no goals

Proof state:
x : PGame
k : (-x).LeftMoves
P : (-x).LeftMoves → Prop
h : ∀ (i : x.RightMoves), P (toLeftMovesNeg i)
⊢ P k

Tactic:
rw [← toLeftMovesNeg.apply_symm_apply k]

Result:
x : PGame
k : (-x).LeftMoves
P : (-x).LeftMoves → Prop
h : ∀ (i : x.RightMoves), P (toLeftMovesNeg i)
⊢ P (toLeftMovesNeg (toLeftMovesNeg.symm k))
-- Mathlib/Data/Finsupp/Indicator.lean
theorem support_indicator_subset : ((indicator s f).support : Set ι) ⊆ s

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : i ∈ ↑(indicator s f).support
⊢ i ∈ ↑s

Tactic:
rw [mem_coe, mem_support_iff] at hi

Result:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : (indicator s f) i ≠ 0
⊢ i ∈ ↑s

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
⊢ ↑(indicator s f).support ⊆ ↑s

Tactic:
intro i hi

Result:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : i ∈ ↑(indicator s f).support
⊢ i ∈ ↑s

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : (indicator s f) i ≠ 0
h : i ∉ ↑s
⊢ False

Tactic:
exact hi (indicator_of_not_mem h _)

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : (indicator s f) i ≠ 0
⊢ i ∈ ↑s

Tactic:
by_contra h

Result:
ι : Type u_1
α : Type u_2
inst✝ : Zero α
s : Finset ι
f : (i : ι) → i ∈ s → α
i : ι
hi : (indicator s f) i ≠ 0
h : i ∉ ↑s
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean
theorem hasStrictDerivAt_arctan (x : ℝ) : HasStrictDerivAt arctan (1 / (1 + x ^ 2)) x

Proof state:
x : ℝ
A : cos (arctan x) ≠ 0
⊢ 1 / cos (↑tanPartialHomeomorph.symm x) ^ 2 ≠ 0

Tactic:
simpa

Result:
no goals

Proof state:
x : ℝ
A : cos (arctan x) ≠ 0
⊢ HasStrictDerivAt arctan (1 / (1 + x ^ 2)) x

Tactic:
simpa [cos_sq_arctan] using
  tanPartialHomeomorph.hasStrictDerivAt_symm trivial (by simpa) (hasStrictDerivAt_tan A)

Result:
no goals

Proof state:
x : ℝ
⊢ HasStrictDerivAt arctan (1 / (1 + x ^ 2)) x

Tactic:
have A : cos (arctan x) ≠ 0 := (cos_arctan_pos x).ne'

Result:
x : ℝ
A : cos (arctan x) ≠ 0
⊢ HasStrictDerivAt arctan (1 / (1 + x ^ 2)) x
-- Mathlib/Data/Complex/Norm.lean
theorem lim_re (f : CauSeq ℂ (‖·‖)) : lim (cauSeqRe f) = (lim f).re

Proof state:
f : CauSeq ℂ fun x => ‖x‖
⊢ (cauSeqRe f).lim = (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I).re

Tactic:
simp [ofReal]

Result:
no goals

Proof state:
f : CauSeq ℂ fun x => ‖x‖
⊢ (cauSeqRe f).lim = f.lim.re

Tactic:
rw [lim_eq_lim_im_add_lim_re]

Result:
f : CauSeq ℂ fun x => ‖x‖
⊢ (cauSeqRe f).lim = (↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I).re
-- Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
theorem eval_zero : eval f a 0 = 0

Proof state:
K : Type u
inst✝¹ : Field K
L : Type u
inst✝ : Field L
f : K →+* L
a : L
⊢ eval f a 0 = 0

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem mem_support_derivative [NoZeroSMulDivisors ℕ R] (p : R[X]) (n : ℕ) :
    n ∈ (derivative p).support ↔ n + 1 ∈ p.support

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
⊢ ¬(n + 1 = 0 ∨ p.coeff (n + 1) = 0) ↔ p.coeff (n + 1) ≠ 0

Tactic:
simp only [Nat.succ_ne_zero, false_or]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
⊢ ¬p.coeff (n + 1) * ↑(n + 1) = 0 ↔ p.coeff (n + 1) ≠ 0

Tactic:
rw [← nsmul_eq_mul', smul_eq_zero]

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
⊢ ¬(n + 1 = 0 ∨ p.coeff (n + 1) = 0) ↔ p.coeff (n + 1) ≠ 0

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
⊢ n ∈ (derivative p).support ↔ n + 1 ∈ p.support

Tactic:
suffices ¬p.coeff (n + 1) * (n + 1 : ℕ) = 0 ↔ coeff p (n + 1) ≠ 0 by
  simpa only [mem_support_iff, coeff_derivative, Ne, Nat.cast_succ]

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
⊢ ¬p.coeff (n + 1) * ↑(n + 1) = 0 ↔ p.coeff (n + 1) ≠ 0

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroSMulDivisors ℕ R
p : R[X]
n : ℕ
this : ¬p.coeff (n + 1) * ↑(n + 1) = 0 ↔ p.coeff (n + 1) ≠ 0
⊢ n ∈ (derivative p).support ↔ n + 1 ∈ p.support

Tactic:
simpa only [mem_support_iff, coeff_derivative, Ne, Nat.cast_succ]

Result:
no goals
-- Mathlib/Topology/Germ.lean
theorem restrictGermPredicate_congr {P : ∀ x : X, Germ (𝓝 x) Y → Prop}
    (hf : RestrictGermPredicate P A x f) (h : ∀ᶠ z in 𝓝ˢ A, g z = f z) :
    RestrictGermPredicate P A x g

Proof state:
case intro
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
hx : x ∈ A
y : X
hy : P y ↑f
h'y : ∀ᶠ (x : X) in 𝓝 y, g x = f x
⊢ P y ↑g

Tactic:
rwa [Germ.coe_eq.mpr h'y]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
⊢ RestrictGermPredicate P A x ↑g

Tactic:
intro hx

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
hx : x ∈ A
⊢ ∀ᶠ (y : X) in 𝓝 x, P y ↑g

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
hx : x ∈ A
⊢ ∀ᶠ (y : X) in 𝓝 x, P y ↑g

Tactic:
apply ((hf hx).and <| (eventually_nhdsSet_iff_forall.mp h x hx).eventually_nhds).mono

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
hx : x ∈ A
⊢ ∀ (x : X), (P x ↑f ∧ ∀ᶠ (x : X) in 𝓝 x, g x = f x) → P x ↑g

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
hx : x ∈ A
⊢ ∀ (x : X), (P x ↑f ∧ ∀ᶠ (x : X) in 𝓝 x, g x = f x) → P x ↑g

Tactic:
rintro y ⟨hy, h'y⟩

Result:
case intro
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
hx : x ∈ A
y : X
hy : P y ↑f
h'y : ∀ᶠ (x : X) in 𝓝 y, g x = f x
⊢ P y ↑g
-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
@[simp]
lemma comp_id {ι₂ M₂ N₂ : Type*}
    [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
    (P : RootPairing ι R M N) (Q : RootPairing ι₂ R M₂ N₂) (f : Hom P Q) :
    comp (id Q) f = f

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
f : P.Hom Q
⊢ (id Q).comp f = f

Tactic:
ext x <;> simp

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
lemma image2_curry (f : α × β → γ) (s : Set α) (t : Set β) :
    image2 (fun a b ↦ f (a, b)) s t = f '' s ×ˢ t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α × β → γ
s : Set α
t : Set β
⊢ image2 (fun a b => f (a, b)) s t = f '' s ×ˢ t

Tactic:
simp [← image_uncurry_prod, uncurry]

Result:
no goals
-- Mathlib/Topology/Instances/Matrix.lean
theorem Matrix.transpose_tsum [T2Space R] {f : X → Matrix m n R} : (∑' x, f x)ᵀ = ∑' x, (f x)ᵀ

Proof state:
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst✝² : AddCommMonoid R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : X → Matrix m n R
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ

Tactic:
by_cases hf : Summable f

Result:
case pos
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst✝² : AddCommMonoid R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : X → Matrix m n R
hf : Summable f
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ

case neg
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst✝² : AddCommMonoid R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ

Proof state:
case neg
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst✝² : AddCommMonoid R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => (f x)ᵀ
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ

Tactic:
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft, transpose_zero]

Result:
no goals

Proof state:
case neg
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst✝² : AddCommMonoid R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ

Tactic:
have hft := summable_matrix_transpose.not.mpr hf

Result:
case neg
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst✝² : AddCommMonoid R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => (f x)ᵀ
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ

Proof state:
case pos
X : Type u_1
m : Type u_4
n : Type u_5
R : Type u_8
inst✝² : AddCommMonoid R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : X → Matrix m n R
hf : Summable f
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ

Tactic:
exact hf.hasSum.matrix_transpose.tsum_eq.symm

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem iSup_restrict_spanningSets_of_measurableSet [SigmaFinite μ] (hs : MeasurableSet s) :
    ⨆ i, μ.restrict (spanningSets μ i) s = μ s :=
  calc
    ⨆ i, μ.restrict (spanningSets μ i) s = μ.restrict (⋃ i, spanningSets μ i) s :=
      (restrict_iUnion_apply_eq_iSup (monotone_spanningSets μ).directed_le hs).symm
    _ = μ s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : SigmaFinite μ
hs : MeasurableSet s
⊢ (μ.restrict (⋃ i, spanningSets μ i)) s = μ s

Tactic:
rw [iUnion_spanningSets, restrict_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem mem_ite_none_right {x : α} [Decidable p] {l : Option α} :
    (x ∈ if p then l else none) ↔ p ∧ x ∈ l

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : Option α
⊢ (x ∈ if p then l else none) ↔ p ∧ x ∈ l

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/WittPolynomial.lean
theorem wittPolynomial_zero : wittPolynomial p R 0 = X 0

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
⊢ W_ R 0 = X 0

Tactic:
simp only [wittPolynomial, X, sum_singleton, range_one, pow_zero, zero_add, tsub_self]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem span_mul_span' (S T : Set R) : span S * span T = span (S * T)

Proof state:
R : Type u
inst✝ : CommSemiring R
S T : Set R
⊢ span S * span T = span (S * T)

Tactic:
unfold span

Result:
R : Type u
inst✝ : CommSemiring R
S T : Set R
⊢ Submodule.span R S * Submodule.span R T = Submodule.span R (S * T)

Proof state:
R : Type u
inst✝ : CommSemiring R
S T : Set R
⊢ Submodule.span R S * Submodule.span R T = Submodule.span R (S * T)

Tactic:
rw [Submodule.span_mul_span]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem exp_one_rpow (x : ℝ) : exp 1 ^ x = exp x

Proof state:
x : ℝ
⊢ rexp 1 ^ x = rexp x

Tactic:
rw [← exp_mul, one_mul]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem finrank_eq_rank :
    finrank ℝ ({w : InfinitePlace K // w ≠ w₀} → ℝ) = Units.rank K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℝ ({ w // w ≠ w₀ } → ℝ) = rank K

Tactic:
simp only [finrank_fintype_fun_eq_card, Fintype.card_subtype_compl,
  Fintype.card_ofSubsingleton, rank]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℝ ({ w // w ≠ w₀ } → ℝ) = rank K

Tactic:
classical
simp only [finrank_fintype_fun_eq_card, Fintype.card_subtype_compl,
  Fintype.card_ofSubsingleton, rank]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean
lemma exp_llr_of_ac' (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] (hμν : ν ≪ μ) :
    (fun x ↦ exp (llr μ ν x)) =ᵐ[ν] fun x ↦ (μ.rnDeriv ν x).toReal

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
⊢ rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal

Tactic:
rwa [if_neg hx_pos.ne'] at hx

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : ν ≪ μ
⊢ (fun x => rexp (llr μ ν x)) =ᶠ[ae ν] fun x => (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [exp_llr μ ν, Measure.rnDeriv_pos' hμν] with x hx hx_pos

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
⊢ rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal
-- Mathlib/FieldTheory/Extension.lean
theorem carrier_union : (union c hc).carrier = ⨆ i : c, i.1.carrier :=
  le_antisymm (iSup_le <| by rintro ⟨i, rfl|hi⟩; exacts [bot_le, le_iSup_of_le ⟨i, hi⟩ le_rfl]) <|
    iSup_le fun i ↦ le_iSup_of_le ⟨i, .inr i.2⟩ le_rfl

Proof state:
case mk.inl
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
⊢ (↑⟨⊥, ⋯⟩).carrier ≤ ⨆ i, (↑i).carrier

case mk.inr
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
i : Lifts F E K
hi : i ∈ c
⊢ (↑⟨i, ⋯⟩).carrier ≤ ⨆ i, (↑i).carrier

Tactic:
exacts [bot_le, le_iSup_of_le ⟨i, hi⟩ le_rfl]

Result:
no goals

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
⊢ ∀ (i : ↑(insert ⊥ c)), (↑i).carrier ≤ ⨆ i, (↑i).carrier

Tactic:
rintro ⟨i, rfl|hi⟩

Result:
case mk.inl
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
⊢ (↑⟨⊥, ⋯⟩).carrier ≤ ⨆ i, (↑i).carrier

case mk.inr
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
c : Set (Lifts F E K)
hc : IsChain (fun x1 x2 => x1 ≤ x2) c
i : Lifts F E K
hi : i ∈ c
⊢ (↑⟨i, ⋯⟩).carrier ≤ ⨆ i, (↑i).carrier
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem iInf_Ioi_eq (f : StieltjesFunction) (x : ℝ) : ⨅ r : Ioi x, f r = f x

Proof state:
f : StieltjesFunction
x : ℝ
⊢ 𝓝[>] x ≠ ⊥

Tactic:
rw [← neBot_iff]

Result:
f : StieltjesFunction
x : ℝ
⊢ (𝓝[>] x).NeBot

Proof state:
f : StieltjesFunction
x : ℝ
⊢ (𝓝[>] x).NeBot

Tactic:
infer_instance

Result:
no goals

Proof state:
f : StieltjesFunction
x : ℝ
this : rightLim (↑f) x = ⨅ r, ↑f ↑r
⊢ ⨅ r, ↑f ↑r = ↑f x

Tactic:
rw [← this, f.rightLim_eq]

Result:
no goals

Proof state:
f : StieltjesFunction
x : ℝ
⊢ ⨅ r, ↑f ↑r = ↑f x

Tactic:
suffices Function.rightLim f x = ⨅ r : Ioi x, f r by rw [← this, f.rightLim_eq]

Result:
f : StieltjesFunction
x : ℝ
⊢ rightLim (↑f) x = ⨅ r, ↑f ↑r

Proof state:
f : StieltjesFunction
x : ℝ
⊢ rightLim (↑f) x = ⨅ r, ↑f ↑r

Tactic:
rw [f.mono.rightLim_eq_sInf, sInf_image']

Result:
f : StieltjesFunction
x : ℝ
⊢ 𝓝[>] x ≠ ⊥
-- Mathlib/Analysis/Normed/Order/UpperLower.lean
lemma dist_mono_left_pi : MonotoneOn (dist · y) (Ici y)

Proof state:
ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Ici y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Ici y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ (y₁ i - y i).toNNReal ≤ (y₂ i - y i).toNNReal

Tactic:
exact Real.toNNReal_mono (sub_le_sub_right (hy _) _)

Result:
no goals

Proof state:
ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Ici y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Ici y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ nndist (y₁ i) (y i) ≤ nndist (y₂ i) (y i)

Tactic:
rw [Real.nndist_eq, Real.nnabs_of_nonneg (sub_nonneg_of_le (‹y ≤ _› i : y i ≤ y₁ i)),
  Real.nndist_eq, Real.nnabs_of_nonneg (sub_nonneg_of_le (‹y ≤ _› i : y i ≤ y₂ i))]

Result:
ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Ici y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Ici y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ (y₁ i - y i).toNNReal ≤ (y₂ i - y i).toNNReal

Proof state:
ι : Type u_2
inst✝ : Fintype ι
y : ι → ℝ
⊢ MonotoneOn (fun x => dist x y) (Ici y)

Tactic:
refine fun y₁ hy₁ y₂ hy₂ hy ↦ NNReal.coe_le_coe.2 (Finset.sup_mono_fun fun i _ ↦ ?_)

Result:
ι : Type u_2
inst✝ : Fintype ι
y y₁ : ι → ℝ
hy₁ : y₁ ∈ Ici y
y₂ : ι → ℝ
hy₂ : y₂ ∈ Ici y
hy : y₁ ≤ y₂
i : ι
x✝ : i ∈ Finset.univ
⊢ nndist (y₁ i) (y i) ≤ nndist (y₂ i) (y i)
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean
theorem PreservesCokernel.iso_inv : (PreservesCokernel.iso G f).inv = cokernelComparison f G

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ cokernel.π (G.map f) ≫ (iso G f).inv = cokernel.π (G.map f) ≫ cokernelComparison f G

Tactic:
simp [PreservesCokernel.iso]

Result:
no goals

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ (iso G f).inv = cokernelComparison f G

Tactic:
rw [← cancel_epi (cokernel.π _)]

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ cokernel.π (G.map f) ≫ (iso G f).inv = cokernel.π (G.map f) ≫ cokernelComparison f G