harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Composition/Prod.lean
theorem prod_apply' (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η]
    (a : α) {s : Set (β × γ)} (hs : MeasurableSet s) :
    (κ ×ₖ η) a s = ∫⁻ b : β, (η a) {c : γ | (b, c) ∈ s} ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ×ₖ η) a) s = ∫⁻ (b : β), (η a) {c | (b, c) ∈ s} ∂κ a

Tactic:
simp_rw [prod, compProd_apply hs, swapLeft_apply _ _, prodMkLeft_apply, Prod.swap_prod_mk]

Result:
no goals
-- Mathlib/Data/Multiset/Functor.lean
theorem comp_traverse {G H : Type _ → Type _} [Applicative G] [Applicative H] [CommApplicative G]
    [CommApplicative H] {α β γ : Type _} (g : α → G β) (h : β → H γ) (x : Multiset α) :
    traverse (Comp.mk ∘ Functor.map h ∘ g) x =
    Comp.mk (Functor.map (traverse h) (traverse g x))

Proof state:
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
⊢ ∀ (a : List α), traverse (Comp.mk ∘ Functor.map h ∘ g) ⟦a⟧ = Comp.mk (traverse h <$> traverse g ⟦a⟧)

Tactic:
intro

Result:
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
a✝ : List α
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) ⟦a✝⟧ = Comp.mk (traverse h <$> traverse g ⟦a✝⟧)

Proof state:
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
a✝ : List α
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) ⟦a✝⟧ = Comp.mk (traverse h <$> traverse g ⟦a✝⟧)

Tactic:
simp only [traverse, quot_mk_to_coe, lift_coe, Function.comp_apply, Functor.map_map, functor_norm]

Result:
no goals

Proof state:
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
⊢ traverse (Comp.mk ∘ Functor.map h ∘ g) x = Comp.mk (traverse h <$> traverse g x)

Tactic:
refine Quotient.inductionOn x ?_

Result:
G H : Type u_1 → Type u_1
inst✝³ : Applicative G
inst✝² : Applicative H
inst✝¹ : CommApplicative G
inst✝ : CommApplicative H
α β γ : Type u_1
g : α → G β
h : β → H γ
x : Multiset α
⊢ ∀ (a : List α), traverse (Comp.mk ∘ Functor.map h ∘ g) ⟦a⟧ = Comp.mk (traverse h <$> traverse g ⟦a⟧)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem exists_of_eraseP {l : Array α} {a} (hm : a ∈ l) (hp : p a) :
    ∃ a l₁ l₂, (∀ b ∈ l₁, ¬p b) ∧ p a ∧ l = l₁.push a ++ l₂ ∧ l.eraseP p = l₁ ++ l₂

Proof state:
α : Type u_1
p : α → Bool
l : Array α
a : α
hm : a ∈ l
hp : p a = true
⊢ ∃ a l₁ l₂, (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧ p a = true ∧ l = l₁.push a ++ l₂ ∧ l.eraseP p = l₁ ++ l₂

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
a : α
hp : p a = true
l : List α
hm : a ∈ { toList := l }
⊢ ∃ a l₁ l₂,
    (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧
      p a = true ∧ { toList := l } = l₁.push a ++ l₂ ∧ { toList := l }.eraseP p = l₁ ++ l₂

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
hp : p a = true
l : List α
hm : a ∈ { toList := l }
⊢ ∃ a l₁ l₂,
    (∀ (b : α), b ∈ l₁ → ¬p b = true) ∧
      p a = true ∧ { toList := l } = l₁.push a ++ l₂ ∧ { toList := l }.eraseP p = l₁ ++ l₂

Tactic:
obtain ⟨a, l₁, l₂, h₁, h₂, rfl, h₃⟩ := List.exists_of_eraseP (by simpa using hm) (hp)

Result:
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a✝ : α
hp : p a✝ = true
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
hm : a✝ ∈ { toList := l₁ ++ a :: l₂ }
h₃ : List.eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
⊢ ∃ a_1 l₁_1 l₂_1,
    (∀ (b : α), b ∈ l₁_1 → ¬p b = true) ∧
      p a_1 = true ∧
        { toList := l₁ ++ a :: l₂ } = l₁_1.push a_1 ++ l₂_1 ∧ { toList := l₁ ++ a :: l₂ }.eraseP p = l₁_1 ++ l₂_1

Proof state:
α : Type u_1
p : α → Bool
a✝ : α
hp : p a✝ = true
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
hm : a✝ ∈ { toList := l₁ ++ a :: l₂ }
h₃ : List.eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
⊢ { toList := l₁ ++ a :: l₂ } = { toList := l₁ }.push a ++ { toList := l₂ }

Tactic:
simp

Result:
no goals

Proof state:
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
p : α → Bool
a✝ : α
hp : p a✝ = true
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
hm : a✝ ∈ { toList := l₁ ++ a :: l₂ }
h₃ : List.eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
⊢ ∃ a_1 l₁_1 l₂_1,
    (∀ (b : α), b ∈ l₁_1 → ¬p b = true) ∧
      p a_1 = true ∧
        { toList := l₁ ++ a :: l₂ } = l₁_1.push a_1 ++ l₂_1 ∧ { toList := l₁ ++ a :: l₂ }.eraseP p = l₁_1 ++ l₂_1

Tactic:
refine ⟨a, ⟨l₁⟩, ⟨l₂⟩, by simpa using h₁, h₂, by simp, by simpa using h₃⟩

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
hp : p a = true
l : List α
hm : a ∈ { toList := l }
⊢ a ∈ ?m.4129

Tactic:
simpa using hm

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a✝ : α
hp : p a✝ = true
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
hm : a✝ ∈ { toList := l₁ ++ a :: l₂ }
h₃ : List.eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
⊢ ∀ (b : α), b ∈ { toList := l₁ } → ¬p b = true

Tactic:
simpa using h₁

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a✝ : α
hp : p a✝ = true
a : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬p b = true
h₂ : p a = true
hm : a✝ ∈ { toList := l₁ ++ a :: l₂ }
h₃ : List.eraseP p (l₁ ++ a :: l₂) = l₁ ++ l₂
⊢ { toList := l₁ ++ a :: l₂ }.eraseP p = { toList := l₁ } ++ { toList := l₂ }

Tactic:
simpa using h₃

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- Outside the usual range of `binEntropy`, it is negative. This is due to `log p = log |p|` -/
lemma binEntropy_neg_of_one_lt (hp : 1 < p) : binEntropy p < 0

Proof state:
p : ℝ
hp : 1 < p
⊢ binEntropy p < 0

Tactic:
rw [← binEntropy_one_sub]

Result:
p : ℝ
hp : 1 < p
⊢ binEntropy (1 - p) < 0

Proof state:
p : ℝ
hp : 1 < p
⊢ binEntropy (1 - p) < 0

Tactic:
exact binEntropy_neg_of_neg (sub_neg.2 hp)

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem tendsto_prod_iff {f : α × β → γ} {x : Filter α} {y : Filter β} {z : Filter γ} :
    Tendsto f (x ×ˢ y) z ↔ ∀ W ∈ z, ∃ U ∈ x, ∃ V ∈ y, ∀ x y, x ∈ U → y ∈ V → f (x, y) ∈ W

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
x : Filter α
y : Filter β
z : Filter γ
⊢ Tendsto f (x ×ˢ y) z ↔ ∀ W ∈ z, ∃ U ∈ x, ∃ V ∈ y, ∀ (x : α) (y : β), x ∈ U → y ∈ V → f (x, y) ∈ W

Tactic:
simp only [tendsto_def, mem_prod_iff, prod_sub_preimage_iff, exists_prop]

Result:
no goals
-- Mathlib/Data/String/Basic.lean
theorem toList_nonempty : ∀ {s : String}, s ≠ "" → s.toList = s.head :: (s.drop 1).toList
  | ⟨s⟩, h => by
    cases s with
    | nil => simp at h
    | cons c cs =>
      simp only [toList, data_drop, List.drop_succ_cons, List.drop_zero, List.cons.injEq, and_true]
      rfl

Proof state:
case cons
c : Char
cs : List Char
h : { data := c :: cs } ≠ ""
⊢ { data := c :: cs }.toList = { data := c :: cs }.head :: ({ data := c :: cs }.drop 1).toList

Tactic:
simp only [toList, data_drop, List.drop_succ_cons, List.drop_zero, List.cons.injEq, and_true]

Result:
case cons
c : Char
cs : List Char
h : { data := c :: cs } ≠ ""
⊢ c = { data := c :: cs }.head

Proof state:
s : List Char
h : { data := s } ≠ ""
⊢ { data := s }.toList = { data := s }.head :: ({ data := s }.drop 1).toList

Tactic:
cases s with
| nil => simp at h
| cons c cs =>
  simp only [toList, data_drop, List.drop_succ_cons, List.drop_zero, List.cons.injEq, and_true]
  rfl

Result:
no goals

Proof state:
case cons
c : Char
cs : List Char
h : { data := c :: cs } ≠ ""
⊢ c = { data := c :: cs }.head

Tactic:
rfl

Result:
no goals

Proof state:
case nil
h : { data := [] } ≠ ""
⊢ { data := [] }.toList = { data := [] }.head :: ({ data := [] }.drop 1).toList

Tactic:
simp at h

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean
theorem int_prod_range_pos {m : ℤ} {n : ℕ} (hn : Even n) (hm : m ∉ Ico (0 : ℤ) n) :
    0 < ∏ k ∈ Finset.range n, (m - k)

Proof state:
case intro.intro
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 ↑n
a : ℕ
ha : a ∈ Finset.range n
h : m - ↑a = 0
⊢ m ∈ Ico 0 ↑n

Tactic:
rw [sub_eq_zero.1 h]

Result:
case intro.intro
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 ↑n
a : ℕ
ha : a ∈ Finset.range n
h : m - ↑a = 0
⊢ ↑a ∈ Ico 0 ↑n

Proof state:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 ↑n
⊢ 0 < ∏ k ∈ Finset.range n, (m - ↑k)

Tactic:
refine (int_prod_range_nonneg m n hn).lt_of_ne fun h => hm ?_

Result:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 ↑n
h : 0 = ∏ k ∈ Finset.range n, (m - ↑k)
⊢ m ∈ Ico 0 ↑n

Proof state:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 ↑n
h : ∃ a ∈ Finset.range n, m - ↑a = 0
⊢ m ∈ Ico 0 ↑n

Tactic:
obtain ⟨a, ha, h⟩ := h

Result:
case intro.intro
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 ↑n
a : ℕ
ha : a ∈ Finset.range n
h : m - ↑a = 0
⊢ m ∈ Ico 0 ↑n

Proof state:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 ↑n
h : 0 = ∏ k ∈ Finset.range n, (m - ↑k)
⊢ m ∈ Ico 0 ↑n

Tactic:
rw [eq_comm, Finset.prod_eq_zero_iff] at h

Result:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 ↑n
h : ∃ a ∈ Finset.range n, m - ↑a = 0
⊢ m ∈ Ico 0 ↑n

Proof state:
case intro.intro
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 ↑n
a : ℕ
ha : a ∈ Finset.range n
h : m - ↑a = 0
⊢ ↑a ∈ Ico 0 ↑n

Tactic:
exact ⟨Int.ofNat_zero_le _, Int.ofNat_lt.2 <| Finset.mem_range.1 ha⟩

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem mul_induction_on {I J : FractionalIdeal S P} {C : P → Prop} {r : P}
    (hr : r ∈ I * J) (hm : ∀ i ∈ I, ∀ j ∈ J, C (i * j)) (ha : ∀ x y, C x → C y → C (x + y)) :
    C r

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
C : P → Prop
r : P
hm : ∀ i ∈ I, ∀ j ∈ J, C (i * j)
ha : ∀ (x y : P), C x → C y → C (x + y)
hr : r ∈ ⟨↑I * ↑J, ⋯⟩
⊢ C r

Tactic:
exact Submodule.mul_induction_on hr hm ha

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
C : P → Prop
r : P
hr : r ∈ I * J
hm : ∀ i ∈ I, ∀ j ∈ J, C (i * j)
ha : ∀ (x y : P), C x → C y → C (x + y)
⊢ C r

Tactic:
simp only [mul_def] at hr

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
C : P → Prop
r : P
hm : ∀ i ∈ I, ∀ j ∈ J, C (i * j)
ha : ∀ (x y : P), C x → C y → C (x + y)
hr : r ∈ ⟨↑I * ↑J, ⋯⟩
⊢ C r
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_subtype : range p.subtype = p

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ range p.subtype = p

Tactic:
simpa using map_comap_subtype p ⊤

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem le_one_div_of_neg (ha : a < 0) (hb : b < 0) : a ≤ 1 / b ↔ b ≤ 1 / a

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

Tactic:
simpa using le_inv_of_neg ha hb

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem edist_toLp_zero (f : α → E) (hf : MemLp f p μ) : edist (hf.toLp f) 0 = eLpNorm f p μ

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
⊢ edist (MemLp.toLp f hf) 0 = eLpNorm f p μ

Tactic:
simpa using edist_toLp_toLp f 0 hf MemLp.zero

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive (attr := simp) isAddFreimanHom_one_iff]
lemma isMulFreimanHom_one_iff : IsMulFreimanHom 1 A B f ↔ MapsTo f A B :=
  ⟨fun h => h.mapsTo, fun h => ⟨h, by aesop (add simp card_eq_one)⟩⟩

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
h : MapsTo f A B
⊢ ∀ ⦃s t : Multiset α⦄,
    (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
      (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → s.card = 1 → t.card = 1 → s.prod = t.prod → (map f s).prod = (map f t).prod

Tactic:
aesop (add simp card_eq_one)

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
theorem map_subtype_embedding_Icc (hp : ∀ ⦃a b x⦄, a ≤ x → x ≤ b → p a → p b → p x):
    (Icc a b).map (Embedding.subtype p) = (Icc a b : Finset α)

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Icc ↑a ↑b)) = Icc ↑a ↑b

Tactic:
refine Finset.subtype_map_of_mem fun x hx => ?_

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Icc ↑a ↑b
⊢ p x

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Icc a b) = Icc ↑a ↑b

Tactic:
rw [subtype_Icc_eq]

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Icc ↑a ↑b)) = Icc ↑a ↑b

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Icc ↑a ↑b
⊢ p x

Tactic:
rw [mem_Icc] at hx

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a ≤ x ∧ x ≤ ↑b
⊢ p x

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a ≤ x ∧ x ≤ ↑b
⊢ p x

Tactic:
exact hp hx.1 hx.2 a.prop b.prop

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem deriv.scomp_of_eq
    (hg : DifferentiableAt 𝕜' g₁ y) (hh : DifferentiableAt 𝕜 h x) (hy : y = h x) :
    deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableAt 𝕜' g₁ (h x)
hh : DifferentiableAt 𝕜 h x
hy : y = h x
⊢ deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)

Tactic:
exact deriv.scomp x hg hh

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableAt 𝕜' g₁ y
hh : DifferentiableAt 𝕜 h x
hy : y = h x
⊢ deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)

Tactic:
rw [hy] at hg

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
y : 𝕜'
hg : DifferentiableAt 𝕜' g₁ (h x)
hh : DifferentiableAt 𝕜 h x
hy : y = h x
⊢ deriv (g₁ ∘ h) x = deriv h x • deriv g₁ (h x)
-- Mathlib/Topology/Category/Compactum.lean
theorem cl_eq_closure {X : Compactum} (A : Set X) : cl A = closure A

Proof state:
case h.mpr.intro.intro
X : Compactum
A : Set X.A
x✝ : X.A
F : Ultrafilter X.A
h1 : A ∈ F
h2 : ↑F ≤ 𝓝 x✝
⊢ x✝ ∈ Compactum.cl A

Tactic:
exact ⟨F, h1, str_eq_of_le_nhds _ _ h2⟩

Result:
no goals

Proof state:
case h.mp
X : Compactum
A : Set X.A
x✝ : X.A
⊢ x✝ ∈ Compactum.cl A → ∃ u, A ∈ u ∧ ↑u ≤ 𝓝 x✝

Tactic:
rintro ⟨F, h1, h2⟩

Result:
case h.mp.intro.intro
X : Compactum
A : Set X.A
x✝ : X.A
F : Ultrafilter X.A
h1 : F ∈ Compactum.basic A
h2 : X.str F = x✝
⊢ ∃ u, A ∈ u ∧ ↑u ≤ 𝓝 x✝

Proof state:
case h
X : Compactum
A : Set X.A
x✝ : X.A
⊢ x✝ ∈ Compactum.cl A ↔ ∃ u, A ∈ u ∧ ↑u ≤ 𝓝 x✝

Tactic:
constructor

Result:
case h.mp
X : Compactum
A : Set X.A
x✝ : X.A
⊢ x✝ ∈ Compactum.cl A → ∃ u, A ∈ u ∧ ↑u ≤ 𝓝 x✝

case h.mpr
X : Compactum
A : Set X.A
x✝ : X.A
⊢ (∃ u, A ∈ u ∧ ↑u ≤ 𝓝 x✝) → x✝ ∈ Compactum.cl A

Proof state:
case h.mp.intro.intro
X : Compactum
A : Set X.A
x✝ : X.A
F : Ultrafilter X.A
h1 : F ∈ Compactum.basic A
h2 : X.str F = x✝
⊢ ∃ u, A ∈ u ∧ ↑u ≤ 𝓝 x✝

Tactic:
exact ⟨F, h1, le_nhds_of_str_eq _ _ h2⟩

Result:
no goals

Proof state:
case h.mpr
X : Compactum
A : Set X.A
x✝ : X.A
⊢ (∃ u, A ∈ u ∧ ↑u ≤ 𝓝 x✝) → x✝ ∈ Compactum.cl A

Tactic:
rintro ⟨F, h1, h2⟩

Result:
case h.mpr.intro.intro
X : Compactum
A : Set X.A
x✝ : X.A
F : Ultrafilter X.A
h1 : A ∈ F
h2 : ↑F ≤ 𝓝 x✝
⊢ x✝ ∈ Compactum.cl A

Proof state:
X : Compactum
A : Set X.A
⊢ Compactum.cl A = closure A

Tactic:
ext

Result:
case h
X : Compactum
A : Set X.A
x✝ : X.A
⊢ x✝ ∈ Compactum.cl A ↔ x✝ ∈ closure A

Proof state:
case h
X : Compactum
A : Set X.A
x✝ : X.A
⊢ x✝ ∈ Compactum.cl A ↔ x✝ ∈ closure A

Tactic:
rw [mem_closure_iff_ultrafilter]

Result:
case h
X : Compactum
A : Set X.A
x✝ : X.A
⊢ x✝ ∈ Compactum.cl A ↔ ∃ u, A ∈ u ∧ ↑u ≤ 𝓝 x✝
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem coe_tsum {f : α → ℝ≥0} : ↑(∑' a, f a) = ∑' a, (f a : ℝ)

Proof state:
α : Type u_1
f : α → ℝ≥0
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)

Tactic:
exact if hf : Summable f then Eq.symm <| (hasSum_coe.2 <| hf.hasSum).tsum_eq
else by simp [tsum_def, hf, mt summable_coe.1 hf]

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ≥0
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)

Tactic:
classical
exact if hf : Summable f then Eq.symm <| (hasSum_coe.2 <| hf.hasSum).tsum_eq
else by simp [tsum_def, hf, mt summable_coe.1 hf]

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ≥0
hf : ¬Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)

Tactic:
simp [tsum_def, hf, mt summable_coe.1 hf]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem coe_subtype : (SubgroupClass.subtype H : H → G) = ((↑) : H → G)

Proof state:
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
⊢ ⇑↑H = Subtype.val

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem dropWhile_replicate_eq_filter_not (p : α → Bool) :
    (replicate n a).dropWhile p = (replicate n a).filter (fun a => !p a)

Proof state:
case succ
α : Type u_1
a : α
p : α → Bool
n : Nat
ih : dropWhile p (replicate n a) = filter (fun a => !p a) (replicate n a)
⊢ dropWhile p (replicate (n + 1) a) = filter (fun a => !p a) (replicate (n + 1) a)

Tactic:
simp only [replicate_succ, dropWhile_cons]

Result:
case succ
α : Type u_1
a : α
p : α → Bool
n : Nat
ih : dropWhile p (replicate n a) = filter (fun a => !p a) (replicate n a)
⊢ (if p a = true then dropWhile p (replicate n a) else a :: replicate n a) = filter (fun a => !p a) (a :: replicate n a)

Proof state:
case zero
α : Type u_1
a : α
p : α → Bool
⊢ dropWhile p (replicate 0 a) = filter (fun a => !p a) (replicate 0 a)

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
a : α
p : α → Bool
n : Nat
ih : dropWhile p (replicate n a) = filter (fun a => !p a) (replicate n a)
⊢ (if p a = true then dropWhile p (replicate n a) else a :: replicate n a) = filter (fun a => !p a) (a :: replicate n a)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
p : α → Bool
⊢ dropWhile p (replicate n a) = filter (fun a => !p a) (replicate n a)

Tactic:
induction n with
| zero => simp
| succ n ih =>
  simp only [replicate_succ, dropWhile_cons]
  split <;> simp_all

Result:
no goals
-- Mathlib/Data/Complex/Order.lean
theorem not_le_iff {z w : ℂ} : ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im

Proof state:
z w : ℂ
⊢ ¬z ≤ w ↔ w.re < z.re ∨ z.im ≠ w.im

Tactic:
rw [le_def, not_and_or, not_le]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Over/Basic.lean
theorem OverMorphism.ext {X : T} {U V : Over X} {f g : U ⟶ V} (h : f.left = g.left) : f = g

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Over X
f g : U ⟶ V
h : f.left = g.left
⊢ f = g

Tactic:
let ⟨_,b,_⟩ := f

Result:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Over X
f g : U ⟶ V
left✝ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
h : { left := left✝, right := b, w := w✝ }.left = g.left
⊢ { left := left✝, right := b, w := w✝ } = g

Proof state:
case e_right
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Over X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e
h : { left := left✝¹, right := b, w := w✝¹ }.left = { left := left✝, right := e, w := w✝ }.left
⊢ b = e

Tactic:
simp only [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Over X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e
h : { left := left✝¹, right := b, w := w✝¹ }.left = { left := left✝, right := e, w := w✝ }.left
⊢ { left := left✝¹, right := b, w := w✝¹ } = { left := left✝, right := e, w := w✝ }

Tactic:
congr

Result:
case e_right
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Over X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e
h : { left := left✝¹, right := b, w := w✝¹ }.left = { left := left✝, right := e, w := w✝ }.left
⊢ b = e

Proof state:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Over X
f g : U ⟶ V
left✝ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
h : { left := left✝, right := b, w := w✝ }.left = g.left
⊢ { left := left✝, right := b, w := w✝ } = g

Tactic:
let ⟨_,e,_⟩ := g

Result:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Over X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e
h : { left := left✝¹, right := b, w := w✝¹ }.left = { left := left✝, right := e, w := w✝ }.left
⊢ { left := left✝¹, right := b, w := w✝¹ } = { left := left✝, right := e, w := w✝ }
-- Mathlib/Data/Fin/Basic.lean
theorem pred_one' [NeZero n] (h := (zero_ne_one' (n := n)).symm) :
    Fin.pred (1 : Fin (n + 1)) h = 0

Proof state:
n : ℕ
inst✝ : NeZero n
h : optParam (1 ≠ 0) ⋯
⊢ pred 1 h = 0

Tactic:
simp_rw [Fin.ext_iff, coe_pred, val_one', val_zero, Nat.sub_eq_zero_iff_le, Nat.mod_le]

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem exists_nonsquare (hF : ringChar F ≠ 2) : ∃ a : F, ¬IsSquare a

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
h : ¬Function.Injective fun x => x * x
⊢ ∃ a, ¬IsSquare a

Tactic:
simpa [Finite.injective_iff_surjective, Function.Surjective, IsSquare, eq_comm] using h

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
h : Function.Injective fun x => x * x
⊢ -1 * -1 = 1 * 1

Tactic:
simp

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
⊢ ∃ a, ¬IsSquare a

Tactic:
have h : ¬Function.Injective fun x : F ↦ x * x := fun h ↦
  h.ne (Ring.neg_one_ne_one_of_char_ne_two hF) <| by simp

Result:
F : Type u_3
inst✝¹ : Field F
inst✝ : Finite F
hF : ringChar F ≠ 2
h : ¬Function.Injective fun x => x * x
⊢ ∃ a, ¬IsSquare a