harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem truncate_mk' (f : ℕ → R) :
    truncate n (@mk' p _ f) = TruncatedWittVector.mk _ fun k => f k

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
f : ℕ → R
⊢ (truncate n) { coeff := f } = TruncatedWittVector.mk p fun k => f ↑k

Tactic:
ext i

Result:
case h
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
f : ℕ → R
i : Fin n
⊢ TruncatedWittVector.coeff i ((truncate n) { coeff := f }) =
    TruncatedWittVector.coeff i (TruncatedWittVector.mk p fun k => f ↑k)

Proof state:
case h
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
f : ℕ → R
i : Fin n
⊢ TruncatedWittVector.coeff i ((truncate n) { coeff := f }) =
    TruncatedWittVector.coeff i (TruncatedWittVector.mk p fun k => f ↑k)

Tactic:
simp only [coeff_truncate, TruncatedWittVector.coeff_mk]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Slope.lean
theorem hasDerivWithinAt_iff_tendsto_slope :
    HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s \ {x}] x) (𝓝 f')

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
⊢ HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s \ {x}] x) (𝓝 f')

Tactic:
simp only [HasDerivWithinAt, nhdsWithin, diff_eq, ← inf_assoc, inf_principal.symm]

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
⊢ HasDerivAtFilter f f' x (𝓝 x ⊓ 𝓟 s) ↔ Tendsto (slope f x) (𝓝 x ⊓ 𝓟 s ⊓ 𝓟 {x}ᶜ) (𝓝 f')

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
⊢ HasDerivAtFilter f f' x (𝓝 x ⊓ 𝓟 s) ↔ Tendsto (slope f x) (𝓝 x ⊓ 𝓟 s ⊓ 𝓟 {x}ᶜ) (𝓝 f')

Tactic:
exact hasDerivAtFilter_iff_tendsto_slope

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem ite_eq_of_subset_right (t : Set α) {s₁ s₂ : Set α} (h : s₂ ⊆ s₁) :
    t.ite s₁ s₂ = (s₁ ∩ t) ∪ s₂

Proof state:
case h
α : Type u
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
x : α
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂

Tactic:
by_cases hx : x ∈ t <;> simp [*, Set.ite, or_iff_left_of_imp (@h x)]

Result:
no goals

Proof state:
α : Type u
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
⊢ t.ite s₁ s₂ = s₁ ∩ t ∪ s₂

Tactic:
ext x

Result:
case h
α : Type u
t s₁ s₂ : Set α
h : s₂ ⊆ s₁
x : α
⊢ x ∈ t.ite s₁ s₂ ↔ x ∈ s₁ ∩ t ∪ s₂
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem add_right_cancel {a b : Ordinal} (n : ℕ) : a + n = b + n ↔ a = b

Proof state:
a b : Ordinal.{u_4}
n : ℕ
⊢ a + ↑n = b + ↑n ↔ a = b

Tactic:
simp only [le_antisymm_iff, add_le_add_iff_right]

Result:
no goals
-- Mathlib/Data/ENat/Basic.lean
theorem toNat_sub {n : ℕ∞} (hn : n ≠ ⊤) (m : ℕ∞) : toNat (m - n) = toNat m - toNat n

Proof state:
case intro.coe
n a✝ : ℕ
⊢ (↑a✝ - ↑n).toNat = (↑a✝).toNat - (↑n).toNat

Tactic:
rw [← coe_sub, toNat_coe, toNat_coe, toNat_coe]

Result:
no goals

Proof state:
case intro.top
n : ℕ
⊢ (⊤ - ↑n).toNat = ⊤.toNat - (↑n).toNat

Tactic:
rw [top_sub_coe, toNat_top, zero_tsub]

Result:
no goals

Proof state:
case intro
m : ℕ∞
n : ℕ
⊢ (m - ↑n).toNat = m.toNat - (↑n).toNat

Tactic:
induction m

Result:
case intro.top
n : ℕ
⊢ (⊤ - ↑n).toNat = ⊤.toNat - (↑n).toNat

case intro.coe
n a✝ : ℕ
⊢ (↑a✝ - ↑n).toNat = (↑a✝).toNat - (↑n).toNat

Proof state:
n : ℕ∞
hn : n ≠ ⊤
m : ℕ∞
⊢ (m - n).toNat = m.toNat - n.toNat

Tactic:
lift n to ℕ using hn

Result:
case intro
m : ℕ∞
n : ℕ
⊢ (m - ↑n).toNat = m.toNat - (↑n).toNat
-- Mathlib/Data/Fintype/Fin.lean
theorem card_filter_univ_succ' (p : Fin (n + 1) → Prop) [DecidablePred p] :
    #{x | p x} = ite (p 0) 1 0 + #{x | p (.succ x)}

Proof state:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ #(filter (fun x => p x) univ) = (if p 0 then 1 else 0) + #(filter (fun x => p x.succ) univ)

Tactic:
rw [card_filter_univ_succ]

Result:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ (if p 0 then #(filter (fun x => p x.succ) univ) + 1 else #(filter (fun x => p x.succ) univ)) =
    (if p 0 then 1 else 0) + #(filter (fun x => p x.succ) univ)

Proof state:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ (if p 0 then #(filter (fun x => p x.succ) univ) + 1 else #(filter (fun x => p x.succ) univ)) =
    (if p 0 then 1 else 0) + #(filter (fun x => p x.succ) univ)

Tactic:
split_ifs <;> simp [add_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Action.lean
theorem smul_mem_ae (c : G) {s : Set α} : c • s ∈ ae μ ↔ s ∈ ae μ

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s : Set α
⊢ c • s ∈ ae μ ↔ s ∈ ae μ

Tactic:
simp only [mem_ae_iff, ← smul_set_compl, measure_smul_eq_zero_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem shiftLeft_bitwise_distrib {a b : Nat} (of_false_false : f false false = false

Proof state:
f : Bool → Bool → Bool
i a b : Nat
of_false_false : autoParam (f false false = false) _auto✝
⊢ bitwise f a b <<< i = bitwise f (a <<< i) (b <<< i)

Tactic:
simp [shiftLeft_eq, bitwise_mul_two_pow of_false_false]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem not_all_eq_any_not (l : List α) (p : α → Bool) : (!l.all p) = l.any fun a => !p a

Proof state:
case cons
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
ih : (!tail✝.all p) = tail✝.any fun a => !p a
⊢ (!p head✝ || !tail✝.all p) = (!p head✝ || tail✝.any fun a => !p a)

Tactic:
rw [ih]

Result:
no goals

Proof state:
α : Type u_1
l : List α
p : α → Bool
⊢ (!l.all p) = l.any fun a => !p a

Tactic:
induction l with simp | cons _ _ ih => rw [ih]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem unzip_mk (a : Array (α × β)) (h : a.size = n) :
    (Vector.mk a h).unzip = (Vector.mk a.unzip.1 (by simp_all), Vector.mk a.unzip.2 (by simp_all)) := rfl

Proof state:
α : Type ?u.18534
β : Type ?u.18533
n : Nat
a : Array (α × β)
h : a.size = n
⊢ a.unzip.snd.size = n

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type ?u.18534
β : Type ?u.18533
n : Nat
a : Array (α × β)
h : a.size = n
⊢ a.unzip.fst.size = n

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma Nontrivial.mul_right : s.Nontrivial → t.Nonempty → (s * t).Nontrivial

Proof state:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ (s * t).Nontrivial

Tactic:
exact ⟨a * c, mul_mem_mul ha hc, b * c, mul_mem_mul hb hc, by simpa⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ a * c ≠ b * c

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s t : Finset α
⊢ s.Nontrivial → t.Nonempty → (s * t).Nontrivial

Tactic:
rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ (s * t).Nontrivial
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem ne_none_iff_isSome : o ≠ none ↔ o.isSome

Proof state:
α✝ : Type u_1
o : Option α✝
⊢ o ≠ none ↔ o.isSome = true

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma cpow_ofReal_re (x : ℂ) (y : ℝ) : (x ^ (y : ℂ)).re = ‖x‖ ^ y * Real.cos (arg x * y)

Proof state:
x : ℂ
y z : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos z) + ↑(Real.sin z) * I)).re = ‖x‖ ^ y * Real.cos z

Tactic:
simp [Real.cos]

Result:
no goals

Proof state:
x : ℂ
y : ℝ
⊢ (x ^ ↑y).re = ‖x‖ ^ y * Real.cos (x.arg * y)

Tactic:
rw [cpow_ofReal]

Result:
x : ℂ
y : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)).re = ‖x‖ ^ y * Real.cos (x.arg * y)

Proof state:
x : ℂ
y : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * I)).re = ‖x‖ ^ y * Real.cos (x.arg * y)

Tactic:
generalize arg x * y = z

Result:
x : ℂ
y z : ℝ
⊢ (↑(‖x‖ ^ y) * (↑(Real.cos z) + ↑(Real.sin z) * I)).re = ‖x‖ ^ y * Real.cos z
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_fintype_iUnion {ι : Type*} [Fintype ι] {s : ι → Set X}
    (hs : ∀ i, MeasurableSet (s i)) (h's : Pairwise (Disjoint on s))
    (hf : ∀ i, IntegrableOn f (s i) μ) : ∫ x in ⋃ i, s i, f x ∂μ = ∑ i, ∫ x in s i, f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i) μ
⊢ ∫ (x : X) in ⋃ i, s i, f x ∂μ = ∑ i : ι, ∫ (x : X) in s i, f x ∂μ

Tactic:
convert integral_finset_biUnion Finset.univ (fun i _ => hs i) _ fun i _ => hf i

Result:
case h.e'_2.h.e'_6.h.e'_4.h.e'_3.h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i) μ
x✝ : ι
⊢ s x✝ = ⋃ (_ : x✝ ∈ Finset.univ), s x✝

X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i) μ
⊢ (↑Finset.univ).Pairwise (Disjoint on s)

Proof state:
case h.e'_2.h.e'_6.h.e'_4.h.e'_3.h
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i) μ
x✝ : ι
⊢ s x✝ = ⋃ (_ : x✝ ∈ Finset.univ), s x✝

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i) μ
⊢ (↑Finset.univ).Pairwise (Disjoint on s)

Tactic:
simp [pairwise_univ, h's]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Lattice.lean
theorem inf_arrow_factors_right {B : C} (X Y : Subobject B) : Y.Factors (X ⊓ Y).arrow :=
  (factors_iff _ _).mpr ⟨ofLE (X ⊓ Y) Y (inf_le_right X Y), by simp⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
B : C
X Y : Subobject B
⊢ (X ⊓ Y).ofLE Y ⋯ ≫ (representative.obj Y).arrow = (X ⊓ Y).arrow

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
lemma essInf_eq_iInf (hμ : ∀ a, μ {a} ≠ 0) (f : α → β) : essInf f μ = ⨅ i, f i

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
hμ : ∀ (a : α), μ {a} ≠ 0
f : α → β
⊢ essInf f μ = ⨅ i, f i

Tactic:
rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_iInf]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem measure_union_add_inter₀' (hs : NullMeasurableSet s μ) (t : Set α) :
    μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
⊢ μ (s ∪ t) + μ (s ∩ t) = μ s + μ t

Tactic:
rw [union_comm, inter_comm, measure_union_add_inter₀ t hs, add_comm]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem eq_bot_of_subsingleton [Subsingleton S] : S = ⊥

Proof state:
M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
y : M
hy : y ∈ S
⊢ y = 1

Tactic:
simpa using congr_arg ((↑) : S → M) <| Subsingleton.elim (⟨y, hy⟩ : S) 1

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
⊢ ∀ x ∈ S, x = 1

Tactic:
intro y hy

Result:
M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
y : M
hy : y ∈ S
⊢ y = 1

Proof state:
M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
⊢ S = ⊥

Tactic:
rw [eq_bot_iff_forall]

Result:
M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
⊢ ∀ x ∈ S, x = 1
-- Mathlib/Data/Finset/Prod.lean
theorem product_sdiff_diag : s ×ˢ s \ s.diag = s.offDiag

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s ×ˢ s \ s.diag = s.offDiag

Tactic:
rw [← diag_union_offDiag, union_comm, union_sdiff_self,
  sdiff_eq_self_of_disjoint (disjoint_diag_offDiag _).symm]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem closure_singleton_one : closure ({1} : Set M) = ⊥

Proof state:
M : Type u_1
inst✝ : Monoid M
⊢ closure {1} = ⊥

Tactic:
simp [eq_bot_iff_forall, mem_closure_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) :
    (mkArray n v)[i] = v

Proof state:
α : Type u_1
i n : Nat
v : α
h : i < (mkArray n v).size
⊢ (mkArray n v)[i] = v

Tactic:
simp [← getElem_toList]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem IsRegularOfDegree.compl [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj]
    {k : ℕ} (h : G.IsRegularOfDegree k) : Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k)

Proof state:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
k : ℕ
h : G.IsRegularOfDegree k
v : V
⊢ Gᶜ.degree v = Fintype.card V - 1 - k

Tactic:
rw [degree_compl, h v]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
k : ℕ
h : G.IsRegularOfDegree k
⊢ Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k)

Tactic:
intro v

Result:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
k : ℕ
h : G.IsRegularOfDegree k
v : V
⊢ Gᶜ.degree v = Fintype.card V - 1 - k
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_congr {R S : Type*} [Semiring R] [Semiring S] {f g : R →+* S} {s t : S}
    {φ ψ : R[X]} : f = g → s = t → φ = ψ → eval₂ f s φ = eval₂ g t ψ

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f g : R →+* S
s t : S
φ ψ : R[X]
⊢ f = g → s = t → φ = ψ → eval₂ f s φ = eval₂ g t ψ

Tactic:
rintro rfl rfl rfl

Result:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
s : S
φ : R[X]
⊢ eval₂ f s φ = eval₂ f s φ

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
s : S
φ : R[X]
⊢ eval₂ f s φ = eval₂ f s φ

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem pairwise_pair : Set.Pairwise {a, b} r ↔ a ≠ b → r a b ∧ r b a

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
⊢ {a, b}.Pairwise r ↔ a ≠ b → r a b ∧ r b a

Tactic:
simp [pairwise_insert]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem map_comp (g : β → γ) : (p.map f).map g = p.map (g ∘ f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : PMF α
g : β → γ
⊢ map g (map f p) = map (g ∘ f) p

Tactic:
simp [map, Function.comp_def]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem AffineEquiv.wbtw_map_iff {x y z : P} (f : P ≃ᵃ[R] P') :
    Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P ≃ᵃ[R] P'
⊢ Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z

Tactic:
have : Function.Injective f.toAffineMap := f.injective

Result:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P ≃ᵃ[R] P'
this : Function.Injective ⇑↑f
⊢ Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P ≃ᵃ[R] P'
this : Function.Injective ⇑↑f
⊢ Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z

Tactic:
apply this.wbtw_map_iff

Result:
no goals
-- Mathlib/Probability/Moments/ComplexMGF.lean
lemma complexMGF_congr_identDistrib {Ω' : Type*} {mΩ' : MeasurableSpace Ω'} {μ' : Measure Ω'}
    {Y : Ω' → ℝ}  (h : IdentDistrib X Y μ μ') :
    complexMGF X μ = complexMGF Y μ'

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
⊢ complexMGF X μ = complexMGF Y μ'

Tactic:
rw [← complexMGF_id_map h.aemeasurable_fst, ← complexMGF_id_map h.aemeasurable_snd, h.map_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean
/-- The kernel of a zero map is preserved by any functor which preserves zero morphisms. -/
lemma preservesKernel_zero' (f : X ⟶ Y) (hf : f = 0) :
    PreservesLimit (parallelPair f 0) 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
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
f : X ⟶ Y
hf : f = 0
⊢ PreservesLimit (parallelPair f 0) G

Tactic:
rw [hf]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
f : X ⟶ Y
hf : f = 0
⊢ PreservesLimit (parallelPair 0 0) 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
X Y : C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
f : X ⟶ Y
hf : f = 0
⊢ PreservesLimit (parallelPair 0 0) G

Tactic:
infer_instance

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
@[simp]
lemma cochainsMap_zero : cochainsMap (A := A) (B := B) f 0 = 0

Proof state:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
⊢ cochainsMap f 0 = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem quotient_mk_comp_C_isIntegral_of_isJacobsonRing {R : Type*} [CommRing R] [IsJacobsonRing R]
    (P : Ideal (MvPolynomial (Fin n) R)) [hP : P.IsMaximal] :
    RingHom.IsIntegral (RingHom.comp (Ideal.Quotient.mk P) (MvPolynomial.C))

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin n) R)
hP : P.IsMaximal
⊢ (algebraMap R (MvPolynomial (Fin n) R ⧸ P)).IsIntegral

Tactic:
apply quotient_mk_comp_C_isIntegral_of_isJacobsonRing'

Result:
case hP
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin n) R)
hP : P.IsMaximal
⊢ P.IsMaximal

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin n) R)
hP : P.IsMaximal
⊢ ((Ideal.Quotient.mk P).comp C).IsIntegral

Tactic:
change RingHom.IsIntegral (algebraMap R (MvPolynomial (Fin n) R ⧸ P))

Result:
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin n) R)
hP : P.IsMaximal
⊢ (algebraMap R (MvPolynomial (Fin n) R ⧸ P)).IsIntegral

Proof state:
case hP
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsJacobsonRing R
P : Ideal (MvPolynomial (Fin n) R)
hP : P.IsMaximal
⊢ P.IsMaximal

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem MonovaryOn.sum_comp_perm_smul_le_sum_smul (hfg : MonovaryOn f g s)
    (hσ : {x | σ x ≠ x} ⊆ s) : ∑ i ∈ s, f (σ i) • g i ≤ ∑ i ∈ s, f i • g i

Proof state:
case h.e'_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g (σ⁻¹ i)

Tactic:
exact σ.sum_comp' s (fun i j ↦ f i • g j) hσ

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f (σ i) • g i ≤ ∑ i ∈ s, f i • g i

Tactic:
convert hfg.sum_smul_comp_perm_le_sum_smul
  (show { x | σ⁻¹ x ≠ x } ⊆ s by simp only [set_support_inv_eq, hσ]) using 1

Result:
case h.e'_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f (σ i) • g i = ∑ i ∈ s, f i • g (σ⁻¹ i)

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ {x | σ⁻¹ x ≠ x} ⊆ ↑s

Tactic:
simp only [set_support_inv_eq, hσ]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_le_one_of_ge (h : b ≤ a) (hb : b ≤ 0) : a / b ≤ 1

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
h : b ≤ a
hb : b ≤ 0
⊢ a / b ≤ 1

Tactic:
simpa only [neg_div_neg_eq] using div_le_one_of_le₀ (neg_le_neg h) (neg_nonneg_of_nonpos hb)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sqrtTwoAddSeries_monotone_left {x y : ℝ} (h : x ≤ y) :
    ∀ n : ℕ, sqrtTwoAddSeries x n ≤ sqrtTwoAddSeries y n
  | 0 => h
  | n + 1 => by
    rw [sqrtTwoAddSeries, sqrtTwoAddSeries]
    exact sqrt_le_sqrt (add_le_add_left (sqrtTwoAddSeries_monotone_left h _) _)

Proof state:
x y : ℝ
h : x ≤ y
n : ℕ
⊢ x.sqrtTwoAddSeries (n + 1) ≤ y.sqrtTwoAddSeries (n + 1)

Tactic:
rw [sqrtTwoAddSeries, sqrtTwoAddSeries]

Result:
x y : ℝ
h : x ≤ y
n : ℕ
⊢ √(2 + x.sqrtTwoAddSeries n) ≤ √(2 + y.sqrtTwoAddSeries n)

Proof state:
x y : ℝ
h : x ≤ y
n : ℕ
⊢ √(2 + x.sqrtTwoAddSeries n) ≤ √(2 + y.sqrtTwoAddSeries n)

Tactic:
exact sqrt_le_sqrt (add_le_add_left (sqrtTwoAddSeries_monotone_left h _) _)

Result:
no goals
-- Mathlib/Logic/Small/Defs.lean
theorem Shrink.ext {α : Type v} [Small.{w} α] {x y : Shrink α}
    (w : (equivShrink _).symm x = (equivShrink _).symm y) : x = y

Proof state:
α : Type v
inst✝ : Small.{w, v} α
x y : Shrink.{w, v} α
w : (equivShrink α).symm x = (equivShrink α).symm y
⊢ x = y

Tactic:
simpa using w

Result:
no goals