harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FirstDerivativeTest.lean
/-- The First-Derivative Test from calculus, maxima version.
Suppose `a < b < c`, `f : ℝ → ℝ` is continuous at `b`,
the derivative `f'` is nonnegative on `(a,b)`, and
the derivative `f'` is nonpositive on `(b,c)`. Then `f` has a local maximum at `a`. -/
lemma isLocalMax_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a < b) (g₁ : b < c)
    (h : ContinuousAt f b)
    (hd₀ : DifferentiableOn ℝ f (Ioo a b))
    (hd₁ : DifferentiableOn ℝ f (Ioo b c))
    (h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x)
    (h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) : IsLocalMax f b :=
  have hIoc : ContinuousOn f (Ioc a b) :=
    Ioo_union_right g₀ ▸ hd₀.continuousOn.union_continuousAt (isOpen_Ioo (a := a) (b := b))
      (by simp_all)
  have hIco : ContinuousOn f (Ico b c) :=
    Ioo_union_left g₁ ▸ hd₁.continuousOn.union_continuousAt (isOpen_Ioo (a := b) (b := c))
      (by simp_all)
  isLocalMax_of_mono_anti g₀ g₁
    (monotoneOn_of_deriv_nonneg (convex_Ioc a b) hIoc (by simp_all) (by simp_all))
    (antitoneOn_of_deriv_nonpos (convex_Ico b c) hIco (by simp_all) (by simp_all))

Proof state:
f : ℝ → ℝ
a b c : ℝ
g₀ : a < b
g₁ : b < c
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
hIoc : ContinuousOn f (Ioc a b)
hIco : ContinuousOn f (Ico b c)
⊢ DifferentiableOn ℝ f (interior (Ico b c))

Tactic:
simp_all

Result:
no goals

Proof state:
f : ℝ → ℝ
a b c : ℝ
g₀ : a < b
g₁ : b < c
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
hIoc : ContinuousOn f (Ioc a b)
hIco : ContinuousOn f (Ico b c)
⊢ ∀ x ∈ interior (Ioc a b), 0 ≤ deriv f x

Tactic:
simp_all

Result:
no goals

Proof state:
f : ℝ → ℝ
a b c : ℝ
g₀ : a < b
g₁ : b < c
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
hIoc : ContinuousOn f (Ioc a b)
hIco : ContinuousOn f (Ico b c)
⊢ ∀ x ∈ interior (Ico b c), deriv f x ≤ 0

Tactic:
simp_all

Result:
no goals

Proof state:
f : ℝ → ℝ
a b c : ℝ
g₀ : a < b
g₁ : b < c
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ {b}, ContinuousAt f x

Tactic:
simp_all

Result:
no goals

Proof state:
f : ℝ → ℝ
a b c : ℝ
g₀ : a < b
g₁ : b < c
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
hIoc : ContinuousOn f (Ioc a b)
⊢ ∀ x ∈ {b}, ContinuousAt f x

Tactic:
simp_all

Result:
no goals

Proof state:
f : ℝ → ℝ
a b c : ℝ
g₀ : a < b
g₁ : b < c
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
hIoc : ContinuousOn f (Ioc a b)
hIco : ContinuousOn f (Ico b c)
⊢ DifferentiableOn ℝ f (interior (Ioc a b))

Tactic:
simp_all

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

Proof state:
α : Type u_1
p q : α → Bool
l : List α
⊢ dropWhile q (filter p l) = filter p (dropWhile (fun a => !p a || q a) l)

Tactic:
simp [← filterMap_eq_filter, dropWhile_filterMap]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
lemma sdiff_sup_lowerClosure (hts : t ⊆ s) (hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t) :
    s.sdiff t ⊔ lowerClosure t = s

Proof state:
case inl
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t
a : α
ha : a ∈ ↑s
hat : a ∈ t
⊢ a ∈ ↑(s.sdiff t ⊔ lowerClosure t)

Tactic:
exact subset_union_right (subset_lowerClosure hat)

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t
a : α
ha : a ∈ ↑s
hat : a ∉ t
⊢ a ∈ ↑(s.sdiff t ⊔ lowerClosure t)

Tactic:
refine subset_union_left ⟨ha, ?_⟩

Result:
case inr
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t
a : α
ha : a ∈ ↑s
hat : a ∉ t
⊢ a ∉ ↑(upperClosure t)

Proof state:
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t
a : α
ha : a ∈ ↑s
⊢ a ∈ ↑(s.sdiff t ⊔ lowerClosure t)

Tactic:
obtain hat | hat := em (a ∈ t)

Result:
case inl
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t
a : α
ha : a ∈ ↑s
hat : a ∈ t
⊢ a ∈ ↑(s.sdiff t ⊔ lowerClosure t)

case inr
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t
a : α
ha : a ∈ ↑s
hat : a ∉ t
⊢ a ∈ ↑(s.sdiff t ⊔ lowerClosure t)

Proof state:
case inr.intro.intro
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t
a : α
ha : a ∈ ↑s
hat : a ∉ t
b : α
hb : b ∈ t
hba : b ≤ a
⊢ False

Tactic:
exact hat <| hst _ ha _ hb hba

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t
⊢ s.sdiff t ⊔ lowerClosure t = s

Tactic:
refine le_antisymm (sup_le sdiff_le_left <| lowerClosure_le.2 hts) fun a ha ↦ ?_

Result:
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t
a : α
ha : a ∈ ↑s
⊢ a ∈ ↑(s.sdiff t ⊔ lowerClosure t)

Proof state:
case inr
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t
a : α
ha : a ∈ ↑s
hat : a ∉ t
⊢ a ∉ ↑(upperClosure t)

Tactic:
rintro ⟨b, hb, hba⟩

Result:
case inr.intro.intro
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t
a : α
ha : a ∈ ↑s
hat : a ∉ t
b : α
hb : b ∈ t
hba : b ≤ a
⊢ False
-- Mathlib/Data/Set/Function.lean
theorem MapsTo.restrict_inj (h : MapsTo f s t) : Injective (h.restrict f s t) ↔ InjOn f s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ Injective (restrict f s t h) ↔ InjOn f s

Tactic:
rw [h.restrict_eq_codRestrict, injective_codRestrict, injOn_iff_injective]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem _root_.aemeasurable_add_measure_iff :
    AEMeasurable f (μ + ν) ↔ AEMeasurable f μ ∧ AEMeasurable f ν

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ ν : Measure α
⊢ AEMeasurable f (bif true then μ else ν) ∧ AEMeasurable f (bif false then μ else ν) ↔
    AEMeasurable f μ ∧ AEMeasurable f ν

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ ν : Measure α
⊢ AEMeasurable f (μ + ν) ↔ AEMeasurable f μ ∧ AEMeasurable f ν

Tactic:
rw [← sum_cond, aemeasurable_sum_measure_iff, Bool.forall_bool, and_comm]

Result:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ ν : Measure α
⊢ AEMeasurable f (bif true then μ else ν) ∧ AEMeasurable f (bif false then μ else ν) ↔
    AEMeasurable f μ ∧ AEMeasurable f ν
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem Measurable.piecewise {_ : DecidablePred (· ∈ s)} (hs : MeasurableSet s)
    (hf : Measurable f) (hg : Measurable g) : Measurable (piecewise s f g)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
⊢ Measurable (s.piecewise f g)

Tactic:
intro t ht

Result:
α : Type u_1
β : Type u_2
s : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (s.piecewise f g ⁻¹' t)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (s.piecewise f g ⁻¹' t)

Tactic:
rw [piecewise_preimage]

Result:
α : Type u_1
β : Type u_2
s : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (s.ite (f ⁻¹' t) (g ⁻¹' t))

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f g : α → β
m : MeasurableSpace α
mβ : MeasurableSpace β
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : Measurable f
hg : Measurable g
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (s.ite (f ⁻¹' t) (g ⁻¹' t))

Tactic:
exact hs.ite (hf ht) (hg ht)

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem mem_chain_of_mem_ωSup {c : Chain (Part α)} {a : α} (h : a ∈ Part.ωSup c) : some a ∈ c

Proof state:
case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : a ∈ some (Classical.choose h_1)
⊢ some a ∈ c

Tactic:
have h' := Classical.choose_spec h_1

Result:
case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : a ∈ some (Classical.choose h_1)
h' : some (Classical.choose h_1) ∈ c
⊢ some a ∈ c

Proof state:
case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : a ∈ some (Classical.choose h_1)
h' : some (Classical.choose h_1) ∈ c
⊢ some a ∈ c

Tactic:
rw [← eq_some_iff] at h

Result:
case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : some (Classical.choose h_1) = some a
h' : some (Classical.choose h_1) ∈ c
⊢ some a ∈ c

Proof state:
case neg
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ¬∃ a, some a ∈ c
h : a ∈ none
⊢ some a ∈ c

Tactic:
rcases h with ⟨⟨⟩⟩

Result:
no goals

Proof state:
case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : some (Classical.choose h_1) = some a
h' : some (Classical.choose h_1) ∈ c
⊢ some (Classical.choose h_1) ∈ c

Tactic:
exact h'

Result:
no goals

Proof state:
case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : some (Classical.choose h_1) = some a
h' : some (Classical.choose h_1) ∈ c
⊢ some a ∈ c

Tactic:
rw [← h]

Result:
case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : some (Classical.choose h_1) = some a
h' : some (Classical.choose h_1) ∈ c
⊢ some (Classical.choose h_1) ∈ c

Proof state:
α : Type u_2
c : Chain (Part α)
a : α
h : a ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none
⊢ some a ∈ c

Tactic:
split_ifs at h with h_1

Result:
case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : a ∈ some (Classical.choose h_1)
⊢ some a ∈ c

case neg
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ¬∃ a, some a ∈ c
h : a ∈ none
⊢ some a ∈ c

Proof state:
α : Type u_2
c : Chain (Part α)
a : α
h : a ∈ Part.ωSup c
⊢ some a ∈ c

Tactic:
simp only [Part.ωSup] at h

Result:
α : Type u_2
c : Chain (Part α)
a : α
h : a ∈ if h : ∃ a, some a ∈ c then some (Classical.choose h) else none
⊢ some a ∈ c
-- Mathlib/Probability/Distributions/Gaussian.lean
/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `c * X`
has Gaussian law with mean `c * μ` and variance `c^2 * v`. -/
lemma gaussianReal_const_mul {X : Ω → ℝ} (hX : Measure.map X ℙ = gaussianReal μ v) (c : ℝ) :
    Measure.map (fun ω ↦ c * X ω) ℙ = gaussianReal (c * μ) (⟨c^2, sq_nonneg _⟩ * v)

Proof state:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
c : ℝ
hXm : AEMeasurable X ℙ
⊢ Measure.map ((fun ω => c * ω) ∘ X) ℙ = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Tactic:
rw [← AEMeasurable.map_map_of_aemeasurable (measurable_id'.const_mul c).aemeasurable hXm, hX]

Result:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
c : ℝ
hXm : AEMeasurable X ℙ
⊢ Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Proof state:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
c : ℝ
hXm : AEMeasurable X ℙ
⊢ Measure.map (fun x => c * x) (gaussianReal μ v) = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Tactic:
exact gaussianReal_map_const_mul c

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
c : ℝ
hXm : AEMeasurable X ℙ
⊢ Measure.map (fun ω => c * X ω) ℙ = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Tactic:
change Measure.map ((fun ω ↦ c * ω) ∘ X) ℙ = gaussianReal (c * μ) (⟨c^2, sq_nonneg _⟩ * v)

Result:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
c : ℝ
hXm : AEMeasurable X ℙ
⊢ Measure.map ((fun ω => c * ω) ∘ X) ℙ = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Proof state:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
c : ℝ
⊢ NeZero (Measure.map X ℙ)

Tactic:
rw [hX]

Result:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
c : ℝ
⊢ NeZero (gaussianReal μ v)

Proof state:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
c : ℝ
⊢ NeZero (gaussianReal μ v)

Tactic:
infer_instance

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
c : ℝ
⊢ Measure.map (fun ω => c * X ω) ℙ = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Tactic:
have hXm : AEMeasurable X := aemeasurable_of_map_neZero (by rw [hX]; infer_instance)

Result:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
c : ℝ
hXm : AEMeasurable X ℙ
⊢ Measure.map (fun ω => c * X ω) ℙ = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)
-- Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean
@[reassoc]
lemma map_opShiftFunctorEquivalence_unitIso_inv_app_unop (X : Cᵒᵖ) (n : ℤ) :
    F.map ((opShiftFunctorEquivalence C n).unitIso.inv.app X).unop =
      ((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj X.unop))).unop ≫
        (((F.op).commShiftIso n).hom.app X).unop⟦n⟧' ≫
        ((F.commShiftIso n).inv.app _)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map ((opShiftFunctorEquivalence C n).unitIso.inv.app X).unop =
    ((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctor D n).map ((F.op.commShiftIso n).hom.app X).unop ≫
        (F.commShiftIso n).inv.app (unop ((shiftFunctor Cᵒᵖ n).obj X))

Tactic:
rw [← cancel_mono (F.map ((opShiftFunctorEquivalence C n).unitIso.hom.app X).unop),
  ← F.map_comp, ← unop_comp, Iso.hom_inv_id_app,
  map_opShiftFunctorEquivalence_unitIso_hom_app_unop, assoc, assoc,
  Iso.inv_hom_id_app_assoc, ← Functor.map_comp_assoc, ← unop_comp]

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    ((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctor D n).map ((F.op.commShiftIso n).inv.app X ≫ (F.op.commShiftIso n).hom.app X).unop ≫
        ((opShiftFunctorEquivalence D n).unitIso.hom.app (op (F.obj (unop X)))).unop

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    ((opShiftFunctorEquivalence D n).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctor D n).map ((F.op.commShiftIso n).inv.app X ≫ (F.op.commShiftIso n).hom.app X).unop ≫
        ((opShiftFunctorEquivalence D n).unitIso.hom.app (op (F.obj (unop X)))).unop

Tactic:
simp

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Iic_subset_Iio_succ (a : α) : Iic a ⊆ Iio (succ a)

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Iic a ⊆ Iio (succ a)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem _root_.LinearMap.BilinForm.toQuadraticMap_isOrtho [IsCancelAdd R]
    [NoZeroDivisors R] [CharZero R] {B : BilinMap R M R} {x y : M} (h : B.IsSymm) :
    B.toQuadraticMap.IsOrtho x y ↔ B.IsOrtho x y

Proof state:
R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsCancelAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
⊢ B.toQuadraticMap.IsOrtho x y ↔ LinearMap.IsOrtho B x y

Tactic:
letI : AddCancelMonoid R := { ‹IsCancelAdd R›, (inferInstanceAs <| AddCommMonoid R) with }

Result:
R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsCancelAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst✝²;
  let __src_1 := inferInstanceAs (AddCommMonoid R);
  AddCancelMonoid.mk ⋯
⊢ B.toQuadraticMap.IsOrtho x y ↔ LinearMap.IsOrtho B x y

Proof state:
R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsCancelAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst✝²;
  let __src_1 := inferInstanceAs (AddCommMonoid R);
  AddCancelMonoid.mk ⋯
⊢ (B x) x + (B y) y + ((B y) x + (B x) y) = (B x) x + (B y) y ↔ (B x) y = 0

Tactic:
rw [add_right_eq_self (a := B x x + B y y), ← h, RingHom.id_apply, add_self_eq_zero]

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsCancelAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst✝²;
  let __src_1 := inferInstanceAs (AddCommMonoid R);
  AddCancelMonoid.mk ⋯
⊢ B.toQuadraticMap.IsOrtho x y ↔ LinearMap.IsOrtho B x y

Tactic:
simp_rw [isOrtho_def, LinearMap.isOrtho_def, B.toQuadraticMap_apply, map_add,
  LinearMap.add_apply, add_comm _ (B y y), add_add_add_comm _ _ (B y y), add_comm (B y y)]

Result:
R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsCancelAdd R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst✝²;
  let __src_1 := inferInstanceAs (AddCommMonoid R);
  AddCancelMonoid.mk ⋯
⊢ (B x) x + (B y) y + ((B y) x + (B x) y) = (B x) x + (B y) y ↔ (B x) y = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofInt_mul {n} (x y : Int) : BitVec.ofInt n (x * y) =
    BitVec.ofInt n x * BitVec.ofInt n y

Proof state:
n : Nat
x y : Int
⊢ BitVec.ofInt n (x * y) = BitVec.ofInt n x * BitVec.ofInt n y

Tactic:
apply eq_of_toInt_eq

Result:
case a
n : Nat
x y : Int
⊢ (BitVec.ofInt n (x * y)).toInt = (BitVec.ofInt n x * BitVec.ofInt n y).toInt

Proof state:
case a
n : Nat
x y : Int
⊢ (BitVec.ofInt n (x * y)).toInt = (BitVec.ofInt n x * BitVec.ofInt n y).toInt

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem exists_of_sep (P : Cᵒᵖ ⥤ D)
    (hsep :
      ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
        (∀ I : S.Arrow, P.map I.f.op x = P.map I.f.op y) → x = y)
    (X : C) (S : J.Cover X) (s : Meq (J.plusObj P) S) :
    ∃ t : ToType ((J.plusObj P).obj (op X)), Meq.mk S t = s

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
⊢ ∃ t, Meq.mk S t = s

Tactic:
have inj : ∀ X : C, Function.Injective ((J.toPlus P).app (op X)) := inj_of_sep _ hsep

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : PreservesLimits (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
inj : ∀ (X : C), Function.Injective ⇑(ConcreteCategory.hom ((J.toPlus P).app (op X)))
⊢ ∃ t, Meq.mk S t = s
-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma closure_insert_closure_eq_closure_insert (M : Matroid α) (e : α) (X : Set α) :
    M.closure (insert e (M.closure X)) = M.closure (insert e X)

Proof state:
α : Type u_2
M : Matroid α
e : α
X : Set α
⊢ M.closure (insert e (M.closure X)) = M.closure (insert e X)

Tactic:
simp_rw [← singleton_union, closure_union_closure_right_eq]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem nodup_tail_support_reverse {u : V} {p : G.Walk u u} :
    p.reverse.support.tail.Nodup ↔ p.support.tail.Nodup

Proof state:
case h
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.support[0]? = p.support.getLast?

Tactic:
rw [← getVert_eq_support_get? _ (by omega), List.getLast?_eq_getElem?,
  ← getVert_eq_support_get? _ (by rw [Walk.length_support]; omega)]

Result:
case h
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ some (p.getVert 0) = some (p.getVert (p.support.length - 1))

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.support.length - 1 ≤ p.length

Tactic:
rw [Walk.length_support]

Result:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.length + 1 - 1 ≤ p.length

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.length + 1 - 1 ≤ p.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.support.reverse.tail.Nodup ↔ p.support.tail.Nodup

Tactic:
refine List.nodup_tail_reverse p.support ?h

Result:
case h
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.support[0]? = p.support.getLast?

Proof state:
case h
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ some (p.getVert 0) = some (p.getVert (p.support.length - 1))

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.reverse.support.tail.Nodup ↔ p.support.tail.Nodup

Tactic:
rw [Walk.support_reverse]

Result:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ p.support.reverse.tail.Nodup ↔ p.support.tail.Nodup

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
⊢ 0 ≤ p.length

Tactic:
omega

Result:
no goals