harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Preadditive/Basic.lean
lemma mono_of_isZero_kernel' {X Y : C} {f : X ⟶ Y} (c : KernelFork f) (hc : IsLimit c)
    (h : IsZero c.pt) : Mono f := mono_of_cancel_zero _ (fun g hg => by
  obtain ⟨a, ha⟩ := KernelFork.IsLimit.lift' hc _ hg
  rw [← ha, h.eq_of_tgt a 0, Limits.zero_comp])

Proof state:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
h : IsZero c.pt
P✝ : C
g : P✝ ⟶ X
hg : g ≫ f = 0
a : P✝ ⟶ c.pt
ha : a ≫ Fork.ι c = g
⊢ g = 0

Tactic:
rw [← ha, h.eq_of_tgt a 0, Limits.zero_comp]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
h : IsZero c.pt
P✝ : C
g : P✝ ⟶ X
hg : g ≫ f = 0
⊢ g = 0

Tactic:
obtain ⟨a, ha⟩ := KernelFork.IsLimit.lift' hc _ hg

Result:
case mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
h : IsZero c.pt
P✝ : C
g : P✝ ⟶ X
hg : g ≫ f = 0
a : P✝ ⟶ c.pt
ha : a ≫ Fork.ι c = g
⊢ g = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem take_nil : ([] : List α).take i = []

Proof state:
α : Type u
i : Nat
⊢ take i nil = nil

Tactic:
cases i <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attachWith_map_coe {p : α → Prop} (f : α → β) (l : Array α) (H : ∀ a ∈ l, p a) :
    ((l.attachWith p H).map fun (i : { i // p i}) => f i) = l.map f

Proof state:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : α → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ map (fun i => f i.val) ({ toList := toList✝ }.attachWith p H) = map f { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : α → β
l : Array α
H : ∀ (a : α), a ∈ l → p a
⊢ map (fun i => f i.val) (l.attachWith p H) = map f l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
p : α → Prop
f : α → β
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ map (fun i => f i.val) ({ toList := toList✝ }.attachWith p H) = map f { toList := toList✝ }
-- Mathlib/Data/Matrix/Mul.lean
theorem vecMul_one (v : m → α) : v ᵥ* 1 = v

Proof state:
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
⊢ v ᵥ* 1 = v

Tactic:
ext

Result:
case h
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
x✝ : m
⊢ (v ᵥ* 1) x✝ = v x✝

Proof state:
case h
m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
v : m → α
x✝ : m
⊢ (v ᵥ* 1) x✝ = v x✝

Tactic:
rw [← diagonal_one, vecMul_diagonal, mul_one]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_list_count [DecidableEq α] [CommMonoid α] (s : List α) :
    s.prod = ∏ m ∈ s.toFinset, m ^ s.count m

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s : List α
⊢ s.prod = ∏ m ∈ s.toFinset, m ^ count m s

Tactic:
simpa using prod_list_map_count s id

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
theorem iterate_comp_eval₂ (k : ℕ) (t : S) :
    eval₂ f t (p.comp^[k] q) = (fun x => eval₂ f x p)^[k] (eval₂ f t q)

Proof state:
case succ
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
t : S
k : ℕ
IH : eval₂ f t (p.comp^[k] q) = (fun x => eval₂ f x p)^[k] (eval₂ f t q)
⊢ eval₂ f t (p.comp^[k + 1] q) = (fun x => eval₂ f x p)^[k + 1] (eval₂ f t q)

Tactic:
rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
k : ℕ
t : S
⊢ eval₂ f t (p.comp^[k] q) = (fun x => eval₂ f x p)^[k] (eval₂ f t q)

Tactic:
induction k with
| zero => simp
| succ k IH => rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]

Result:
no goals

Proof state:
case zero
R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : CommSemiring S
f : R →+* S
t : S
⊢ eval₂ f t (p.comp^[0] q) = (fun x => eval₂ f x p)^[0] (eval₂ f t q)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Kleene.lean
theorem add_le_iff : a + b ≤ c ↔ a ≤ c ∧ b ≤ c

Proof state:
α : Type u_1
inst✝ : IdemSemiring α
a b c : α
⊢ a + b ≤ c ↔ a ≤ c ∧ b ≤ c

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_star_id : cfcₙ (star · : R → R) a = star a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
ha : autoParam (p a) _auto✝
⊢ cfcₙ (fun x => star x) a = star a

Tactic:
rw [cfcₙ_star _ a, cfcₙ_id' R a]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem contains_alter_of_beq_eq_false [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)}
    (h : (k == k') = false) : (m.alter k f).contains k' = m.contains k'

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : (k == k') = false
⊢ (m.alter k f).contains k' = m.contains k'

Tactic:
simp only [contains_alter, h, Bool.false_eq_true, reduceIte]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Monoid.lean
theorem Tendsto.atTop_of_isBoundedUnder_le_mul (hf : IsBoundedUnder (· ≤ ·) l f)
    (hfg : Tendsto (fun x => f x * g x) l atTop) : Tendsto g l atTop

Proof state:
case intro
α : Type u_1
M : Type u_2
inst✝ : OrderedCancelCommMonoid M
l : Filter α
f g : α → M
hfg : Tendsto (fun x => f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun x1 x2 => x1 ≤ x2) x C
⊢ Tendsto g l atTop

Tactic:
refine .atTop_of_const_mul C <| tendsto_atTop_mono' l ?_ hfg

Result:
case intro
α : Type u_1
M : Type u_2
inst✝ : OrderedCancelCommMonoid M
l : Filter α
f g : α → M
hfg : Tendsto (fun x => f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun x1 x2 => x1 ≤ x2) x C
⊢ (fun x => f x * g x) ≤ᶠ[l] fun x => C * g x

Proof state:
α : Type u_1
M : Type u_2
inst✝ : OrderedCancelCommMonoid M
l : Filter α
f g : α → M
hf : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l f
hfg : Tendsto (fun x => f x * g x) l atTop
⊢ Tendsto g l atTop

Tactic:
obtain ⟨C, hC⟩ := hf

Result:
case intro
α : Type u_1
M : Type u_2
inst✝ : OrderedCancelCommMonoid M
l : Filter α
f g : α → M
hfg : Tendsto (fun x => f x * g x) l atTop
C : M
hC : ∀ᶠ (x : M) in map f l, (fun x1 x2 => x1 ≤ x2) x C
⊢ Tendsto g l atTop
-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem isOpen_analyticAt : IsOpen { x | AnalyticAt 𝕜 f x }

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
⊢ IsOpen {x | AnalyticAt 𝕜 f x}

Tactic:
rw [isOpen_iff_mem_nhds]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
⊢ ∀ x ∈ {x | AnalyticAt 𝕜 f x}, {x | AnalyticAt 𝕜 f x} ∈ 𝓝 x

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
⊢ {x | AnalyticAt 𝕜 f x} ∈ 𝓝 x

Tactic:
exact mem_of_superset (EMetric.ball_mem_nhds _ hr.r_pos) fun y hy => hr.analyticAt_of_mem hy

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
⊢ ∀ x ∈ {x | AnalyticAt 𝕜 f x}, {x | AnalyticAt 𝕜 f x} ∈ 𝓝 x

Tactic:
rintro x ⟨p, r, hr⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
⊢ {x | AnalyticAt 𝕜 f x} ∈ 𝓝 x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_modifyKey_self [BEq α] [LawfulBEq α] [Inhabited α] {k fallback : α} {f : β k → β k}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
    getKeyD k (modifyKey k f l) fallback = if containsKey k l then k else fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k fallback : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ getKeyD k (modifyKey k f l) fallback = if containsKey k l = true then k else fallback

Tactic:
simp [getKeyD_modifyKey, hl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseIdx_mkArray {n : Nat} {a : α} {k : Nat} {h} :
    (mkArray n a).eraseIdx k = mkArray (n - 1) a

Proof state:
α : Type u_1
n : Nat
a : α
k : Nat
h : k < (mkArray n a).size
⊢ (mkArray n a).eraseIdx k h = mkArray (n - 1) a

Tactic:
simp at h

Result:
α : Type u_1
n : Nat
a : α
k : Nat
h✝ : k < (mkArray n a).size
h : k < n
⊢ (mkArray n a).eraseIdx k h✝ = mkArray (n - 1) a

Proof state:
α : Type u_1
n : Nat
a : α
k : Nat
h✝ : k < (mkArray n a).size
h : k < n
⊢ ((List.replicate n a).eraseIdx k).toArray = (List.replicate (n - 1) a).toArray

Tactic:
simp [List.eraseIdx_replicate, h]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
k : Nat
h✝ : k < (mkArray n a).size
h : k < n
⊢ (mkArray n a).eraseIdx k h✝ = mkArray (n - 1) a

Tactic:
simp only [← List.toArray_replicate, List.eraseIdx_toArray]

Result:
α : Type u_1
n : Nat
a : α
k : Nat
h✝ : k < (mkArray n a).size
h : k < n
⊢ ((List.replicate n a).eraseIdx k).toArray = (List.replicate (n - 1) a).toArray
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_and_distrib_right {f : Filter α} {p : α → Prop} {q : Prop} :
    (∃ᶠ x in f, p x ∧ q) ↔ (∃ᶠ x in f, p x) ∧ q

Proof state:
α : Type u
f : Filter α
p : α → Prop
q : Prop
⊢ (∃ᶠ (x : α) in f, p x ∧ q) ↔ (∃ᶠ (x : α) in f, p x) ∧ q

Tactic:
simp only [@and_comm _ q, frequently_and_distrib_left]

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rdropWhile_eq_self_iff : rdropWhile p l = l ↔ ∀ hl : l ≠ [], ¬p (l.getLast hl)

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l = l ↔ ∀ (hl : l ≠ []), ¬p (l.getLast hl) = true

Tactic:
simp [rdropWhile, reverse_eq_iff, getLast_eq_getElem, Nat.pos_iff_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_iff_append {a : α} {l : Vector α n} :
    a ∈ l ↔ ∃ (m k : Nat) (w : m + 1 + k = n) (s : Vector α m) (t : Vector α k),
      l = (s.push a ++ t).cast w :=
  ⟨append_of_mem, by rintro ⟨m, k, rfl, s, t, rfl⟩; simp⟩

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
a : α
m k : Nat
s : Vector α m
t : Vector α k
⊢ a ∈ Vector.cast ⋯ (s.push a ++ t)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
l : Vector α n
⊢ (∃ m k w s t, l = Vector.cast w (s.push a ++ t)) → a ∈ l

Tactic:
rintro ⟨m, k, rfl, s, t, rfl⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
a : α
m k : Nat
s : Vector α m
t : Vector α k
⊢ a ∈ Vector.cast ⋯ (s.push a ++ t)
-- Mathlib/Order/LiminfLimsup.lean
lemma HasBasis.blimsup_eq_iInf_iSup {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α}
    (hf : f.HasBasis p s) {q : β → Prop} :
    blimsup u f q = ⨅ (i) (_ : p i), ⨆ a ∈ s i, ⨆ (_ : q a), u a

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : CompleteLattice α
p : ι → Prop
s : ι → Set β
f : Filter β
u : β → α
hf : f.HasBasis p s
q : β → Prop
⊢ blimsup u f q = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, ⨆ (_ : q a), u a

Tactic:
simp only [blimsup_eq_limsup, (hf.inf_principal _).limsup_eq_iInf_iSup, mem_inter_iff, iSup_and,
  mem_setOf_eq]

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
/-- If `s ≤ t` in colex, and all elements in `t` are small, then all elements in `s` are small. -/
lemma forall_lt_mono (hst : toColex s ≤ toColex t) (ht : ∀ b ∈ t, b < a) : ∀ b ∈ s, b < a

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
⊢ b < a

Tactic:
by_cases b ∈ t

Result:
case pos
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∈ t
⊢ b < a

case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b < a

Proof state:
case neg.intro.intro.intro
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∉ t
c : α
hct : c ∈ { ofColex := t }.ofColex
hbc : b ≤ c
⊢ b < a

Tactic:
exact hbc.trans_lt <| ht _ hct

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∈ t
⊢ b < a

Tactic:
exact ht _ ‹_›

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∉ t
⊢ b < a

Tactic:
obtain ⟨c, hct, -, hbc⟩ := hst hb ‹_›

Result:
case neg.intro.intro.intro
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
h✝ : b ∉ t
c : α
hct : c ∈ { ofColex := t }.ofColex
hbc : b ≤ c
⊢ b < a

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b < a
⊢ ∀ b ∈ s, b < a

Tactic:
rintro b hb

Result:
α : Type u_1
inst✝ : PartialOrder α
s t : Finset α
a : α
hst : { ofColex := s } ≤ { ofColex := t }
ht : ∀ b ∈ t, b < a
b : α
hb : b ∈ s
⊢ b < a
-- Mathlib/Data/Matrix/Hadamard.lean
theorem dotProduct_vecMul_hadamard [DecidableEq m] [DecidableEq n] (v : m → α) (w : n → α) :
    dotProduct (v ᵥ* (A ⊙ B)) w = trace (diagonal v * A * (B * diagonal w)ᵀ)

Proof state:
α : Type u_1
m : Type u_2
n : Type u_3
A B : Matrix m n α
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
v : m → α
w : n → α
⊢ v ᵥ* A ⊙ B ⬝ᵥ w = (diagonal v * A * (B * diagonal w)ᵀ).trace

Tactic:
rw [← sum_hadamard_eq, Finset.sum_comm]

Result:
α : Type u_1
m : Type u_2
n : Type u_3
A B : Matrix m n α
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
v : m → α
w : n → α
⊢ v ᵥ* A ⊙ B ⬝ᵥ w = ∑ y : n, ∑ x : m, ((diagonal v * A) ⊙ (B * diagonal w)) x y

Proof state:
α : Type u_1
m : Type u_2
n : Type u_3
A B : Matrix m n α
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring α
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
v : m → α
w : n → α
⊢ v ᵥ* A ⊙ B ⬝ᵥ w = ∑ y : n, ∑ x : m, ((diagonal v * A) ⊙ (B * diagonal w)) x y

Tactic:
simp [dotProduct, vecMul, Finset.sum_mul, mul_assoc]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Prod.lean
theorem deterministic_prod_apply' {f : α → β} (mf : Measurable f) (κ : Kernel α γ)
    [IsSFiniteKernel κ] (a : α) {s : Set (β × γ)} (hs : MeasurableSet s) :
    ((Kernel.deterministic f mf) ×ₖ κ) a s = κ a (Prod.mk (f a) ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
mf : Measurable f
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ (κ a) {c | (f a, c) ∈ s} = (κ a) (Prod.mk (f a) ⁻¹' s)

Tactic:
rfl

Result:
no goals

Proof state:
case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
mf : Measurable f
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Measurable fun b => (κ a) {c | (b, c) ∈ s}

Tactic:
exact measurable_measure_prod_mk_left hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
mf : Measurable f
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((deterministic f mf ×ₖ κ) a) s = (κ a) (Prod.mk (f a) ⁻¹' s)

Tactic:
rw [prod_apply' _ _ _ hs, lintegral_deterministic']

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
mf : Measurable f
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ (κ a) {c | (f a, c) ∈ s} = (κ a) (Prod.mk (f a) ⁻¹' s)

case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
mf : Measurable f
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ Measurable fun b => (κ a) {c | (b, c) ∈ s}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_map {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β) (l H) :
    pmap g (map f l) H = pmap (fun a h => g (f a) h) l fun _ h => H _ (mem_map_of_mem _ h)

Proof state:
β : Type u_1
γ : Type u_2
α : Type u_3
p : β → Prop
g : (b : β) → p b → γ
f : α → β
l : Array α
H : ∀ (a : β), a ∈ map f l → p a
⊢ pmap g (map f l) H = pmap (fun a h => g (f a) h) l ⋯

Tactic:
cases l

Result:
case mk
β : Type u_1
γ : Type u_2
α : Type u_3
p : β → Prop
g : (b : β) → p b → γ
f : α → β
toList✝ : List α
H : ∀ (a : β), a ∈ map f { toList := toList✝ } → p a
⊢ pmap g (map f { toList := toList✝ }) H = pmap (fun a h => g (f a) h) { toList := toList✝ } ⋯

Proof state:
case mk
β : Type u_1
γ : Type u_2
α : Type u_3
p : β → Prop
g : (b : β) → p b → γ
f : α → β
toList✝ : List α
H : ∀ (a : β), a ∈ map f { toList := toList✝ } → p a
⊢ pmap g (map f { toList := toList✝ }) H = pmap (fun a h => g (f a) h) { toList := toList✝ } ⋯

Tactic:
simp [List.pmap_map]

Result:
no goals
-- Mathlib/Data/Finset/Dedup.lean
theorem toFinset.ext_iff {a b : List α} : a.toFinset = b.toFinset ↔ ∀ x, x ∈ a ↔ x ∈ b

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : List α
⊢ a.toFinset = b.toFinset ↔ ∀ (x : α), x ∈ a ↔ x ∈ b

Tactic:
simp only [Finset.ext_iff, mem_toFinset]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem erase_insert_of_ne {a b : α} {s : Finset α} (h : a ≠ b) :
    erase (insert a s) b = insert a (erase s b) :=
  ext fun x => by
    have : x ≠ b ∧ x = a ↔ x = a := and_iff_right_of_imp fun hx => hx.symm ▸ h
    simp only [mem_erase, mem_insert, and_or_left, this]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Finset α
h : a ≠ b
x : α
⊢ x ∈ (insert a s).erase b ↔ x ∈ insert a (s.erase b)

Tactic:
have : x ≠ b ∧ x = a ↔ x = a := and_iff_right_of_imp fun hx => hx.symm ▸ h

Result:
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Finset α
h : a ≠ b
x : α
this : x ≠ b ∧ x = a ↔ x = a
⊢ x ∈ (insert a s).erase b ↔ x ∈ insert a (s.erase b)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Finset α
h : a ≠ b
x : α
this : x ≠ b ∧ x = a ↔ x = a
⊢ x ∈ (insert a s).erase b ↔ x ∈ insert a (s.erase b)

Tactic:
simp only [mem_erase, mem_insert, and_or_left, this]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma leftUnshift_smul {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') (x : R) :
    (x • γ).leftUnshift n hn = x • γ.leftUnshift n hn

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
x : R
⊢ (leftShiftLinearEquiv R K L n a n' hn).symm (x • γ) = x • γ.leftUnshift n hn

Tactic:
apply map_smul

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
x : R
⊢ (x • γ).leftUnshift n hn = x • γ.leftUnshift n hn

Tactic:
change (leftShiftLinearEquiv  R K L n a n' hn).symm (x • γ) = _

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
x : R
⊢ (leftShiftLinearEquiv R K L n a n' hn).symm (x • γ) = x • γ.leftUnshift n hn
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem tensorRightTensor_inv_app (X Y Z : C) :
    (tensorRightTensor X Y).inv.app Z = (associator Z X Y).hom

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
⊢ (tensorRightTensor X Y).inv.app Z = (α_ Z X Y).hom

Tactic:
simp [tensorRightTensor]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exponential.lean
theorem Real.exp_eq_exp_ℝ : Real.exp = NormedSpace.exp ℝ

Proof state:
⊢ rexp = NormedSpace.exp ℝ

Tactic:
ext x

Result:
case h
x : ℝ
⊢ rexp x = NormedSpace.exp ℝ x

Proof state:
case h
x : ℝ
⊢ rexp x = NormedSpace.exp ℝ x

Tactic:
exact mod_cast congr_fun Complex.exp_eq_exp_ℂ x

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem iterateFrobeniusEquiv_one_apply (x : R) : iterateFrobeniusEquiv R p 1 x = x ^ p

Proof state:
R : Type u_1
p : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ (iterateFrobeniusEquiv R p 1) x = x ^ p

Tactic:
rw [iterateFrobeniusEquiv_def, pow_one]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem one_le {P : Submodule R A} : (1 : Submodule R A) ≤ P ↔ (1 : A) ∈ P

Proof state:
R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
P : Submodule R A
⊢ 1 ≤ P ↔ 1 ∈ P

Tactic:
simp [one_eq_span]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Basic.lean
theorem coe_decompose_mul_add_of_left_mem [AddLeftCancelMonoid ι] [GradedRing 𝒜] {a b : A}
    (a_mem : a ∈ 𝒜 i) : (decompose 𝒜 (a * b) (i + j) : A) = a * decompose 𝒜 b j

Proof state:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddLeftCancelMonoid ι
inst✝ : GradedRing 𝒜
b : A
a : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (↑a * b)) (i + j)) = ↑a * ↑(((decompose 𝒜) b) j)

Tactic:
rw [decompose_mul, decompose_coe, coe_of_mul_apply_add]

Result:
no goals

Proof state:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddLeftCancelMonoid ι
inst✝ : GradedRing 𝒜
a b : A
a_mem : a ∈ 𝒜 i
⊢ ↑(((decompose 𝒜) (a * b)) (i + j)) = a * ↑(((decompose 𝒜) b) j)

Tactic:
lift a to 𝒜 i using a_mem

Result:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
i j : ι
inst✝¹ : AddLeftCancelMonoid ι
inst✝ : GradedRing 𝒜
b : A
a : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (↑a * b)) (i + j)) = ↑a * ↑(((decompose 𝒜) b) j)