harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem formPerm_subsingleton (s : Cycle α) (h : Subsingleton s) : formPerm s h.nodup = 1

Proof state:
case h.nil
α : Type u_1
inst✝ : DecidableEq α
h : [].length ≤ 1
⊢ [].formPerm = 1

Tactic:
simp

Result:
no goals

Proof state:
case h.cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
h : (hd :: tl).length ≤ 1
⊢ (hd :: tl).formPerm = 1

Tactic:
simp only [length_eq_zero, add_le_iff_nonpos_left, List.length, nonpos_iff_eq_zero] at h

Result:
case h.cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
h : tl = []
⊢ (hd :: tl).formPerm = 1

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ formPerm (Quot.mk (⇑(IsRotated.setoid α)) s) ⋯ = 1

Tactic:
simp only [formPerm_coe, mk_eq_coe]

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ s.formPerm = 1

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ s.formPerm = 1

Tactic:
simp only [length_subsingleton_iff, length_coe, mk_eq_coe] at h

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : List α
h : s.length ≤ 1
⊢ s.formPerm = 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
h : s.Subsingleton
⊢ s.formPerm ⋯ = 1

Tactic:
induction' s using Quot.inductionOn with s

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) s)
⊢ formPerm (Quot.mk (⇑(IsRotated.setoid α)) s) ⋯ = 1

Proof state:
case h.cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
h : tl = []
⊢ (hd :: tl).formPerm = 1

Tactic:
simp [h]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : List α
h : s.length ≤ 1
⊢ s.formPerm = 1

Tactic:
obtain - | ⟨hd, tl⟩ := s

Result:
case h.nil
α : Type u_1
inst✝ : DecidableEq α
h : [].length ≤ 1
⊢ [].formPerm = 1

case h.cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
h : (hd :: tl).length ≤ 1
⊢ (hd :: tl).formPerm = 1
-- Mathlib/Algebra/CharZero/Defs.lean
theorem cast_eq_one {n : ℕ} : (n : R) = 1 ↔ n = 1

Proof state:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
n : ℕ
⊢ ↑n = 1 ↔ n = 1

Tactic:
rw [← cast_one, cast_inj]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
theorem contMDiffWithinAt_of_not_mem_mulTSupport {f : M → M'} [One M'] {x : M}
    (hx : x ∉ mulTSupport f) (n : WithTop ℕ∞) (s : Set M) : ContMDiffWithinAt I I' n f s x

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H M
inst✝¹ : ChartedSpace H' M'
f : M → M'
inst✝ : One M'
x : M
hx : x ∉ mulTSupport f
n : WithTop ℕ∞
s : Set M
⊢ ContMDiffWithinAt I I' n f s x

Tactic:
apply contMDiffWithinAt_const.congr_of_eventuallyEq
  (eventually_nhdsWithin_of_eventually_nhds <| not_mem_mulTSupport_iff_eventuallyEq.mp hx)
  (image_eq_one_of_nmem_mulTSupport hx)

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem isHomogeneous_X (i : σ) : IsHomogeneous (X i : MvPolynomial σ R) 1

Proof state:
case hn
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (single i 1).degree = 1

Tactic:
rw [Finsupp.degree, Finsupp.support_single_ne_zero _ one_ne_zero, Finset.sum_singleton]

Result:
case hn
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (single i 1) i = 1

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (X i).IsHomogeneous 1

Tactic:
apply isHomogeneous_monomial

Result:
case hn
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (single i 1).degree = 1

Proof state:
case hn
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (single i 1) i = 1

Tactic:
exact Finsupp.single_eq_same

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem add_right_cancel (h₁ : c ≡ d [MOD n]) (h₂ : a + c ≡ b + d [MOD n]) :
    a ≡ b [MOD n]

Proof state:
n a b c d : ℕ
h₁ : c ≡ d [MOD n]
h₂ : c + a ≡ d + b [MOD n]
⊢ a ≡ b [MOD n]

Tactic:
exact h₁.add_left_cancel h₂

Result:
no goals

Proof state:
n a b c d : ℕ
h₁ : c ≡ d [MOD n]
h₂ : a + c ≡ b + d [MOD n]
⊢ a ≡ b [MOD n]

Tactic:
rw [add_comm a, add_comm b] at h₂

Result:
n a b c d : ℕ
h₁ : c ≡ d [MOD n]
h₂ : c + a ≡ d + b [MOD n]
⊢ a ≡ b [MOD n]
-- Mathlib/Data/Matrix/Block.lean
theorem toBlock_mul_eq_mul {m n k : Type*} [Fintype n] (p : m → Prop) (q : k → Prop)
    (A : Matrix m n R) (B : Matrix n k R) :
    (A * B).toBlock p q = A.toBlock p ⊤ * B.toBlock ⊤ q

Proof state:
R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k → Prop
A : Matrix m n R
B : Matrix n k R
⊢ (A * B).toBlock p q = A.toBlock p ⊤ * B.toBlock ⊤ q

Tactic:
ext i k

Result:
case a
R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ (A * B).toBlock p q i k = (A.toBlock p ⊤ * B.toBlock ⊤ q) i k

Proof state:
case a
R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∑ j : n, A (↑i) j * B j ↑k = ∑ x : { a // ⊤ a }, A ↑i ↑x * B ↑x ↑k

Tactic:
rw [Finset.sum_subtype]

Result:
case a.h
R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∀ (x : n), x ∈ Finset.univ ↔ ⊤ x

Proof state:
case a
R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ (A * B).toBlock p q i k = (A.toBlock p ⊤ * B.toBlock ⊤ q) i k

Tactic:
simp only [toBlock_apply, mul_apply]

Result:
case a
R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∑ j : n, A (↑i) j * B j ↑k = ∑ x : { a // ⊤ a }, A ↑i ↑x * B ↑x ↑k

Proof state:
case a.h
R : Type u_10
inst✝¹ : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝ : Fintype n
p : m → Prop
q : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // q a }
⊢ ∀ (x : n), x ∈ Finset.univ ↔ ⊤ x

Tactic:
simp [Pi.top_apply, Prop.top_eq_true]

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem smul_of [DistribSMul S R] [IsScalarTower S R R] (a : S) (x : R) :
    a • of f x = of f (a • x)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
f : R[X]
inst✝¹ : DistribSMul S R
inst✝ : IsScalarTower S R R
a : S
x : R
⊢ a • (of f) x = (of f) (a • x)

Tactic:
rw [of, RingHom.comp_apply, RingHom.comp_apply, smul_mk, smul_C]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem bot_orthogonal_eq_top : (⊥ : Submodule 𝕜 E)ᗮ = ⊤

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ⊥ᗮ = ⊤

Tactic:
rw [← top_orthogonal_eq_bot, eq_top_iff]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ⊤ ≤ ⊤ᗮᗮ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ ⊤ ≤ ⊤ᗮᗮ

Tactic:
exact le_orthogonal_orthogonal ⊤

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem getElem_enumFrom (l : List α) (n) (i : Nat) (h : i < (l.enumFrom n).length) :
    (l.enumFrom n)[i] = (n + i, l[i]'(by simpa [enumFrom_length] using h))

Proof state:
α : Type ?u.29913
l : List α
n i : Nat
h : i < (enumFrom n l).length
⊢ i < l.length

Tactic:
simpa [enumFrom_length] using h

Result:
no goals

Proof state:
α : Type u_1
l : List α
n i : Nat
h✝ : i < (enumFrom n l).length
h : i < l.length
⊢ (enumFrom n l)[i] = (n + i, l[i])

Tactic:
rw [getElem_eq_getElem?_get]

Result:
α : Type u_1
l : List α
n i : Nat
h✝ : i < (enumFrom n l).length
h : i < l.length
⊢ (enumFrom n l)[i]?.get ⋯ = (n + i, l[i])

Proof state:
α : Type u_1
l : List α
n i : Nat
h✝ : i < (enumFrom n l).length
h : i < l.length
⊢ (enumFrom n l)[i]?.get ⋯ = (n + i, l[i])

Tactic:
simp only [getElem?_enumFrom, getElem?_eq_getElem h]

Result:
α : Type u_1
l : List α
n i : Nat
h✝ : i < (enumFrom n l).length
h : i < l.length
⊢ (Option.map (fun a => (n + i, a)) (some l[i])).get ⋯ = (n + i, l[i])

Proof state:
α : Type u_1
l : List α
n i : Nat
h : i < (enumFrom n l).length
⊢ (enumFrom n l)[i] = (n + i, l[i])

Tactic:
simp only [enumFrom_length] at h

Result:
α : Type u_1
l : List α
n i : Nat
h✝ : i < (enumFrom n l).length
h : i < l.length
⊢ (enumFrom n l)[i] = (n + i, l[i])

Proof state:
α : Type u_1
l : List α
n i : Nat
h✝ : i < (enumFrom n l).length
h : i < l.length
⊢ (Option.map (fun a => (n + i, a)) (some l[i])).get ⋯ = (n + i, l[i])

Tactic:
simp

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
lemma iSup_coe_eq_top : ⨆ x, (f x : WithTop α) = ⊤ ↔ ¬BddAbove (range f)

Proof state:
case refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ b < ⊤, ∃ i, b < ↑(f i)
r : α
⊢ ∃ y ∈ range f, r < y

Tactic:
rcases hf r (WithTop.coe_lt_top r) with ⟨i, hi⟩

Result:
case refine_1.intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ b < ⊤, ∃ i, b < ↑(f i)
r : α
i : ι
hi : ↑r < ↑(f i)
⊢ ∃ y ∈ range f, r < y

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
i : ι
hi : a.untop ⋯ < f i
⊢ a < ↑(f i)

Tactic:
simpa only [WithTop.coe_untop _ ha.ne] using WithTop.coe_lt_coe.mpr hi

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ⨆ x, ↑(f x) = ⊤ ↔ ¬BddAbove (range f)

Tactic:
rw [iSup_eq_top, not_bddAbove_iff]

Result:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ (∀ b < ⊤, ∃ i, b < ↑(f i)) ↔ ∀ (x : α), ∃ y ∈ range f, x < y

Proof state:
case refine_1.intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ b < ⊤, ∃ i, b < ↑(f i)
r : α
i : ι
hi : ↑r < ↑(f i)
⊢ ∃ y ∈ range f, r < y

Tactic:
exact ⟨f i, ⟨i, rfl⟩, WithTop.coe_lt_coe.mp hi⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
⊢ ∃ i, a < ↑(f i)

Tactic:
rcases hf (a.untop ha.ne) with ⟨-, ⟨i, rfl⟩, hi⟩

Result:
case refine_2.intro.intro.intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
i : ι
hi : a.untop ⋯ < f i
⊢ ∃ i, a < ↑(f i)

Proof state:
case refine_2.intro.intro.intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
i : ι
hi : a.untop ⋯ < f i
⊢ ∃ i, a < ↑(f i)

Tactic:
exact ⟨i, by simpa only [WithTop.coe_untop _ ha.ne] using WithTop.coe_lt_coe.mpr hi⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ (∀ b < ⊤, ∃ i, b < ↑(f i)) ↔ ∀ (x : α), ∃ y ∈ range f, x < y

Tactic:
refine ⟨fun hf r => ?_, fun hf a ha => ?_⟩

Result:
case refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ b < ⊤, ∃ i, b < ↑(f i)
r : α
⊢ ∃ y ∈ range f, r < y

case refine_2
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
hf : ∀ (x : α), ∃ y ∈ range f, x < y
a : WithTop α
ha : a < ⊤
⊢ ∃ i, a < ↑(f i)
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem deriv_comp_of_eq (hh₂ : DifferentiableAt 𝕜' h₂ y) (hh : DifferentiableAt 𝕜 h x)
    (hy : h x = y) :
    deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
y : 𝕜'
hh₂ : DifferentiableAt 𝕜' h₂ y
hh : DifferentiableAt 𝕜 h x
hy : h x = y
⊢ deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x

Tactic:
subst hy

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh : DifferentiableAt 𝕜 h x
hh₂ : DifferentiableAt 𝕜' h₂ (h x)
⊢ deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
hh : DifferentiableAt 𝕜 h x
hh₂ : DifferentiableAt 𝕜' h₂ (h x)
⊢ deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x

Tactic:
exact deriv_comp x hh₂ hh

Result:
no goals
-- Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean
lemma smul_eq_zero_iff_left (hx : x ≠ 0) : c • x = 0 ↔ c = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
x : M
hx : x ≠ 0
⊢ c • x = 0 ↔ c = 0

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_prod {α : Type*} (s : Finset α) (f : α → ℝ) (hf : ∀ x ∈ s, f x ≠ 0) :
    log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i)

Proof state:
case h₁
α : Type u_1
f : α → ℝ
hf : ∀ x ∈ ∅, f x ≠ 0
⊢ log (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, log (f i)

Tactic:
simp

Result:
no goals

Proof state:
case h₂
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
ih : (∀ x ∈ s, f x ≠ 0) → log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i)
hf : f a ≠ 0 ∧ ∀ x ∈ s, f x ≠ 0
⊢ log (∏ i ∈ Finset.cons a s ha, f i) = ∑ i ∈ Finset.cons a s ha, log (f i)

Tactic:
simp [ih hf.2, log_mul hf.1 (Finset.prod_ne_zero_iff.2 hf.2)]

Result:
no goals

Proof state:
case h₂
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
ih : (∀ x ∈ s, f x ≠ 0) → log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i)
hf : ∀ x ∈ Finset.cons a s ha, f x ≠ 0
⊢ log (∏ i ∈ Finset.cons a s ha, f i) = ∑ i ∈ Finset.cons a s ha, log (f i)

Tactic:
rw [Finset.forall_mem_cons] at hf

Result:
case h₂
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
ih : (∀ x ∈ s, f x ≠ 0) → log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i)
hf : f a ≠ 0 ∧ ∀ x ∈ s, f x ≠ 0
⊢ log (∏ i ∈ Finset.cons a s ha, f i) = ∑ i ∈ Finset.cons a s ha, log (f i)

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i)

Tactic:
induction' s using Finset.cons_induction_on with a s ha ih

Result:
case h₁
α : Type u_1
f : α → ℝ
hf : ∀ x ∈ ∅, f x ≠ 0
⊢ log (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, log (f i)

case h₂
α : Type u_1
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
ih : (∀ x ∈ s, f x ≠ 0) → log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i)
hf : ∀ x ∈ Finset.cons a s ha, f x ≠ 0
⊢ log (∏ i ∈ Finset.cons a s ha, f i) = ∑ i ∈ Finset.cons a s ha, log (f i)
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem Parallel.symm {s₁ s₂ : AffineSubspace k P} (h : s₁ ∥ s₂) : s₂ ∥ s₁

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ : AffineSubspace k P
v : V
⊢ s₁ = map (↑(constVAdd k P (-v))) (map (↑(constVAdd k P v)) s₁)

Tactic:
rw [map_map, ← coe_trans_to_affineMap, ← constVAdd_add, neg_add_cancel, constVAdd_zero,
  coe_refl_to_affineMap, map_id]

Result:
no goals

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ : AffineSubspace k P
v : V
⊢ map (↑(constVAdd k P v)) s₁ ∥ s₁

Tactic:
refine ⟨-v, ?_⟩

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ : AffineSubspace k P
v : V
⊢ s₁ = map (↑(constVAdd k P (-v))) (map (↑(constVAdd k P v)) s₁)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ s₂ : AffineSubspace k P
h : s₁ ∥ s₂
⊢ s₂ ∥ s₁

Tactic:
rcases h with ⟨v, rfl⟩

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s₁ : AffineSubspace k P
v : V
⊢ map (↑(constVAdd k P v)) s₁ ∥ s₁
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedTotalDegree_zero (w : σ → M) :
    weightedTotalDegree w (0 : MvPolynomial σ R) = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
⊢ weightedTotalDegree w 0 = ⊥

Tactic:
simp only [weightedTotalDegree, support_zero, Finset.sup_empty]

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
theorem MonotoneOn.convexOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
    (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D))
    (hf'_mono : MonotoneOn (deriv f) (interior D)) : ConvexOn ℝ D f :=
  convexOn_of_slope_mono_adjacent hD
    (by
      intro x y z hx hz hxy hyz
      -- First we prove some trivial inclusions
      have hxzD : Icc x z ⊆ D := hD.ordConnected.out hx hz
      have hxyD : Icc x y ⊆ D := (Icc_subset_Icc_right hyz.le).trans hxzD
      have hxyD' : Ioo x y ⊆ interior D :=
        subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hxyD⟩
      have hyzD : Icc y z ⊆ D := (Icc_subset_Icc_left hxy.le).trans hxzD
      have hyzD' : Ioo y z ⊆ interior D :=
        subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hyzD⟩
      -- Then we apply MVT to both `[x, y]` and `[y, z]`
      obtain ⟨a, ⟨hxa, hay⟩, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x) :=
        exists_deriv_eq_slope f hxy (hf.mono hxyD) (hf'.mono hxyD')
      obtain ⟨b, ⟨hyb, hbz⟩, hb⟩ : ∃ b ∈ Ioo y z, deriv f b = (f z - f y) / (z - y) :=
        exists_deriv_eq_slope f hyz (hf.mono hyzD) (hf'.mono hyzD')
      rw [← ha, ← hb]
      exact hf'_mono (hxyD' ⟨hxa, hay⟩) (hyzD' ⟨hyb, hbz⟩) (hay.trans hyb).le)

Proof state:
case intro.intro.intro
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
hyzD : Icc y z ⊆ D
hyzD' : Ioo y z ⊆ interior D
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)

Tactic:
obtain ⟨b, ⟨hyb, hbz⟩, hb⟩ : ∃ b ∈ Ioo y z, deriv f b = (f z - f y) / (z - y) :=
  exists_deriv_eq_slope f hyz (hf.mono hyzD) (hf'.mono hyzD')

Result:
case intro.intro.intro.intro.intro.intro
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
hyzD : Icc y z ⊆ D
hyzD' : Ioo y z ⊆ interior D
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hb : deriv f b = (f z - f y) / (z - y)
hyb : y < b
hbz : b < z
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (deriv f) (interior D)
⊢ ∀ {x y z : ℝ}, x ∈ D → z ∈ D → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)

Tactic:
intro x y z hx hz hxy hyz

Result:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
-- Mathlib/RingTheory/Spectrum/Prime/Module.lean
lemma Module.stableUnderSpecialization_support :
    StableUnderSpecialization (Module.support R M)

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ StableUnderSpecialization (support R M)

Tactic:
intros x y e H

Result:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : PrimeSpectrum R
e : x ⤳ y
H : x ∈ support R M
⊢ y ∈ support R M

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : PrimeSpectrum R
e : x ⤳ y
H : x ∈ support R M
⊢ y ∈ support R M

Tactic:
rw [mem_support_iff_exists_annihilator] at H ⊢

Result:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : PrimeSpectrum R
e : x ⤳ y
H : ∃ m, (Submodule.span R {m}).annihilator ≤ x.asIdeal
⊢ ∃ m, (Submodule.span R {m}).annihilator ≤ y.asIdeal

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : PrimeSpectrum R
e : x ⤳ y
H : ∃ m, (Submodule.span R {m}).annihilator ≤ x.asIdeal
⊢ ∃ m, (Submodule.span R {m}).annihilator ≤ y.asIdeal

Tactic:
obtain ⟨m, hm⟩ := H

Result:
case intro
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : PrimeSpectrum R
e : x ⤳ y
m : M
hm : (Submodule.span R {m}).annihilator ≤ x.asIdeal
⊢ ∃ m, (Submodule.span R {m}).annihilator ≤ y.asIdeal

Proof state:
case intro
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : PrimeSpectrum R
e : x ⤳ y
m : M
hm : (Submodule.span R {m}).annihilator ≤ x.asIdeal
⊢ ∃ m, (Submodule.span R {m}).annihilator ≤ y.asIdeal

Tactic:
exact ⟨m, hm.trans ((PrimeSpectrum.le_iff_specializes _ _).mpr e)⟩

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem supIndep_attach : (s.attach.SupIndep fun a => f a) ↔ s.SupIndep f

Proof state:
α : Type u_1
ι : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
⊢ (s.attach.SupIndep fun a => f ↑a) ↔ s.SupIndep f

Tactic:
simpa [Finset.attach_map_val] using (supIndep_map (s := s.attach) (g := .subtype _)).symm

Result:
no goals
-- Mathlib/NumberTheory/VonMangoldt.lean
theorem vonMangoldt_apply_prime {p : ℕ} (hp : p.Prime) : Λ p = Real.log p

Proof state:
p : ℕ
hp : Nat.Prime p
⊢ Λ p = Real.log ↑p

Tactic:
rw [vonMangoldt_apply, Prime.minFac_eq hp, if_pos hp.prime.isPrimePow]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma isDiameter_iff_right_mem_and_pointReflection_center_right :
    s.IsDiameter p₁ p₂ ↔ p₂ ∈ s ∧ Equiv.pointReflection s.center p₂ = p₁

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
⊢ s.IsDiameter p₁ p₂ ↔ p₂ ∈ s ∧ (Equiv.pointReflection s.center) p₂ = p₁

Tactic:
rw [isDiameter_comm, isDiameter_iff_left_mem_and_pointReflection_center_left]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem eqToHom_f {C₁ C₂ : HomologicalComplex V c} (h : C₁ = C₂) (n : ι) :
    HomologicalComplex.Hom.f (eqToHom h) n =
      eqToHom (congr_fun (congr_arg HomologicalComplex.X h) n)

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ : HomologicalComplex V c
n : ι
⊢ (eqToHom ⋯).f n = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
h : C₁ = C₂
n : ι
⊢ (eqToHom h).f n = eqToHom ⋯

Tactic:
subst h

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ : HomologicalComplex V c
n : ι
⊢ (eqToHom ⋯).f n = eqToHom ⋯