harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Distributions/Gaussian.lean
/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `X * c`
has Gaussian law with mean `c * μ` and variance `c^2 * v`. -/
lemma gaussianReal_mul_const {X : Ω → ℝ} (hX : Measure.map X ℙ = gaussianReal μ v) (c : ℝ) :
    Measure.map (fun ω ↦ X ω * c) ℙ = gaussianReal (c * μ) (⟨c^2, sq_nonneg _⟩ * v)

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

Tactic:
simp_rw [mul_comm _ c]

Result:
μ : ℝ
v : ℝ≥0
Ω : Type
inst✝ : MeasureSpace Ω
X : Ω → ℝ
hX : Measure.map X ℙ = gaussianReal μ v
c : ℝ
⊢ 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 : ℝ
⊢ Measure.map (fun ω => c * X ω) ℙ = gaussianReal (c * μ) (⟨c ^ 2, ⋯⟩ * v)

Tactic:
exact gaussianReal_const_mul hX c

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.rec_heq {β : List α → Sort _} {f : ∀ a l, β l → β (a :: l)} {b : β []} {l l' : List α}
    (hl : l ~ l') (f_congr : ∀ {a l l' b b'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b'))
    (f_swap : ∀ {a a' l b}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))) :
    HEq (@List.rec α β b f l) (@List.rec α β b f l')

Proof state:
case nil
α : Type u_1
β : List α → Sort u_2
f : (a : α) → (l : List α) → β l → β (a :: l)
b : β []
l l' : List α
f_congr : ∀ {a : α} {l l' : List α} {b : β l} {b' : β l'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b')
f_swap : ∀ {a a' : α} {l : List α} {b : β l}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))
⊢ HEq (List.rec b f []) (List.rec b f [])

Tactic:
rfl

Result:
no goals

Proof state:
case trans
α : Type u_1
β : List α → Sort u_2
f : (a : α) → (l : List α) → β l → β (a :: l)
b : β []
l l' : List α
f_congr : ∀ {a : α} {l l' : List α} {b : β l} {b' : β l'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b')
f_swap : ∀ {a a' : α} {l : List α} {b : β l}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))
l₁✝ l₂✝ l₃✝ : List α
_h₁ : l₁✝ ~ l₂✝
_h₂ : l₂✝ ~ l₃✝
ih₁ : HEq (List.rec b f l₁✝) (List.rec b f l₂✝)
ih₂ : HEq (List.rec b f l₂✝) (List.rec b f l₃✝)
⊢ HEq (List.rec b f l₁✝) (List.rec b f l₃✝)

Tactic:
exact ih₁.trans ih₂

Result:
no goals

Proof state:
α : Type u_1
β : List α → Sort u_2
f : (a : α) → (l : List α) → β l → β (a :: l)
b : β []
l l' : List α
hl : l ~ l'
f_congr : ∀ {a : α} {l l' : List α} {b : β l} {b' : β l'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b')
f_swap : ∀ {a a' : α} {l : List α} {b : β l}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))
⊢ HEq (List.rec b f l) (List.rec b f l')

Tactic:
induction hl with
| nil => rfl
| cons a h ih => exact f_congr h ih
| swap a a' l => exact f_swap
| trans _h₁ _h₂ ih₁ ih₂ => exact ih₁.trans ih₂

Result:
no goals

Proof state:
case swap
α : Type u_1
β : List α → Sort u_2
f : (a : α) → (l : List α) → β l → β (a :: l)
b : β []
l✝ l' : List α
f_congr : ∀ {a : α} {l l' : List α} {b : β l} {b' : β l'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b')
f_swap : ∀ {a a' : α} {l : List α} {b : β l}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))
a a' : α
l : List α
⊢ HEq (List.rec b f (a' :: a :: l)) (List.rec b f (a :: a' :: l))

Tactic:
exact f_swap

Result:
no goals

Proof state:
case cons
α : Type u_1
β : List α → Sort u_2
f : (a : α) → (l : List α) → β l → β (a :: l)
b : β []
l l' : List α
f_congr : ∀ {a : α} {l l' : List α} {b : β l} {b' : β l'}, l ~ l' → HEq b b' → HEq (f a l b) (f a l' b')
f_swap : ∀ {a a' : α} {l : List α} {b : β l}, HEq (f a (a' :: l) (f a' l b)) (f a' (a :: l) (f a l b))
a : α
l₁✝ l₂✝ : List α
h : l₁✝ ~ l₂✝
ih : HEq (List.rec b f l₁✝) (List.rec b f l₂✝)
⊢ HEq (List.rec b f (a :: l₁✝)) (List.rec b f (a :: l₂✝))

Tactic:
exact f_congr h ih

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
/-- Binary **rearrangement inequality**. -/
lemma smul_add_smul_le_smul_add_smul' (ha : a₂ ≤ a₁) (hb : b₂ ≤ b₁) :
    a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ ≤ a₁
hb : b₂ ≤ b₁
⊢ a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Tactic:
simp_rw [add_comm (a₁ • _)]

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ ≤ a₁
hb : b₂ ≤ b₁
⊢ a₂ • b₁ + a₁ • b₂ ≤ a₂ • b₂ + a₁ • b₁

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ ≤ a₁
hb : b₂ ≤ b₁
⊢ a₂ • b₁ + a₁ • b₂ ≤ a₂ • b₂ + a₁ • b₁

Tactic:
exact smul_add_smul_le_smul_add_smul ha hb

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem continuousOn_iff_continuousOn_comp_right {f : Y → Z} {s : Set Y} (h : s ⊆ e.target) :
    ContinuousOn f s ↔ ContinuousOn (f ∘ e) (e.source ∩ e ⁻¹' s)

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Y → Z
s : Set Y
h : s ⊆ e.target
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔ ∀ ⦃x : Y⦄, x ∈ s → ContinuousWithinAt (f ∘ ↑e) (↑e.symm '' s) (↑e.symm x)

Tactic:
refine forall₂_congr fun x hx => ?_

Result:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Y → Z
s : Set Y
h : s ⊆ e.target
x : Y
hx : x ∈ s
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e.symm '' s) (↑e.symm x)

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Y → Z
s : Set Y
h : s ⊆ e.target
x : Y
hx : x ∈ s
⊢ e.source ∈ 𝓝 (↑e.symm x)

Tactic:
exact IsOpen.mem_nhds e.open_source (e.map_target (h hx))

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Y → Z
s : Set Y
h : s ⊆ e.target
⊢ ContinuousOn f s ↔ ContinuousOn (f ∘ ↑e) (e.source ∩ ↑e ⁻¹' s)

Tactic:
simp only [← e.symm_image_eq_source_inter_preimage h, ContinuousOn, forall_mem_image]

Result:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Y → Z
s : Set Y
h : s ⊆ e.target
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔ ∀ ⦃x : Y⦄, x ∈ s → ContinuousWithinAt (f ∘ ↑e) (↑e.symm '' s) (↑e.symm x)

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Y → Z
s : Set Y
h : s ⊆ e.target
x : Y
hx : x ∈ s
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑e.symm '' s) (↑e.symm x)

Tactic:
rw [e.continuousWithinAt_iff_continuousWithinAt_comp_right (h hx),
  e.symm_image_eq_source_inter_preimage h, inter_comm, continuousWithinAt_inter]

Result:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Y → Z
s : Set Y
h : s ⊆ e.target
x : Y
hx : x ∈ s
⊢ e.source ∈ 𝓝 (↑e.symm x)
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffOn_infty_iff_fderiv_of_isOpen (hs : IsOpen s) :
    ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (fderiv 𝕜 f) s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
⊢ DifferentiableOn 𝕜 f s ∧ (∞ = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (fderiv 𝕜 f) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (fderiv 𝕜 f) s

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
⊢ ContDiffOn 𝕜 ∞ f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 ∞ (fderiv 𝕜 f) s

Tactic:
rw [← ENat.coe_top_add_one, contDiffOn_succ_iff_fderiv_of_isOpen hs]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hs : IsOpen s
⊢ DifferentiableOn 𝕜 f s ∧ (∞ = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 ∞ (fderiv 𝕜 f) s ↔
    DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (∞ + 1) (fderiv 𝕜 f) s
-- Mathlib/Order/WithBot.lean
lemma lt_unbot_iff (hy : y ≠ ⊥) : a < unbot y hy ↔ a < y

Proof state:
case intro
α : Type u_1
a : α
inst✝ : LT α
y : α
hy : ↑y ≠ ⊥
⊢ a < (↑y).unbot hy ↔ ↑a < ↑y

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : LT α
y : WithBot α
hy : y ≠ ⊥
⊢ a < y.unbot hy ↔ ↑a < y

Tactic:
lift y to α using id hy

Result:
case intro
α : Type u_1
a : α
inst✝ : LT α
y : α
hy : ↑y ≠ ⊥
⊢ a < (↑y).unbot hy ↔ ↑a < ↑y
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem spanningCoe_inj : G₁.spanningCoe = G₂.spanningCoe ↔ G₁.Adj = G₂.Adj

Proof state:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
⊢ G₁.spanningCoe = G₂.spanningCoe ↔ G₁.Adj = G₂.Adj

Tactic:
simp [Subgraph.spanningCoe]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem of_lintegral_ne_top {f : α →ₛ ℝ≥0∞} (h : f.lintegral μ ≠ ∞) : f.FinMeasSupp μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
h : f.lintegral μ ≠ ⊤
⊢ f.FinMeasSupp μ

Tactic:
refine finMeasSupp_iff.2 fun b hb => ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
h : f.lintegral μ ≠ ⊤
b : ℝ≥0∞
hb : b ≠ 0
⊢ μ (⇑f ⁻¹' {b}) < ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
b : ℝ≥0∞
h : ∑ x ∈ insert b (f.range \ {0}), x * μ (⇑f ⁻¹' {x}) ≠ ⊤
hb : b ≠ 0
⊢ b * μ (⇑f ⁻¹' {b}) ≠ ⊤

Tactic:
exact (lt_top_of_sum_ne_top h (Finset.mem_insert_self _ _)).ne

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
h : f.lintegral μ ≠ ⊤
b : ℝ≥0∞
hb : b ≠ 0
⊢ μ (⇑f ⁻¹' {b}) < ⊤

Tactic:
rw [f.lintegral_eq_of_subset' (Finset.subset_insert b _)] at h

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
b : ℝ≥0∞
h : ∑ x ∈ insert b (f.range \ {0}), x * μ (⇑f ⁻¹' {x}) ≠ ⊤
hb : b ≠ 0
⊢ μ (⇑f ⁻¹' {b}) < ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
b : ℝ≥0∞
h : ∑ x ∈ insert b (f.range \ {0}), x * μ (⇑f ⁻¹' {x}) ≠ ⊤
hb : b ≠ 0
⊢ μ (⇑f ⁻¹' {b}) < ⊤

Tactic:
refine ENNReal.lt_top_of_mul_ne_top_right ?_ hb

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
b : ℝ≥0∞
h : ∑ x ∈ insert b (f.range \ {0}), x * μ (⇑f ⁻¹' {x}) ≠ ⊤
hb : b ≠ 0
⊢ b * μ (⇑f ⁻¹' {b}) ≠ ⊤
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem congr_set {s t : Set H} {x : H} {f : H → H'} (hu : s =ᶠ[𝓝 x] t) : P f s x ↔ P f t x

Proof state:
case intro.intro.intro
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
host : o ⊆ {x | (fun x => x ∈ s ↔ x ∈ t) x}
ho : IsOpen o
hxo : x ∈ o
⊢ P f s x ↔ P f t x

Tactic:
simp_rw [subset_def, mem_setOf, ← and_congr_left_iff, ← mem_inter_iff, ← Set.ext_iff] at host

Result:
case intro.intro.intro
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
ho : IsOpen o
hxo : x ∈ o
host : s ∩ o = t ∩ o
⊢ P f s x ↔ P f t x

Proof state:
case intro.intro.intro
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
ho : IsOpen o
hxo : x ∈ o
host : s ∩ o = t ∩ o
⊢ P f s x ↔ P f t x

Tactic:
rw [hG.is_local ho hxo, host, ← hG.is_local ho hxo]

Result:
no goals

Proof state:
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
⊢ P f s x ↔ P f t x

Tactic:
obtain ⟨o, host, ho, hxo⟩ := mem_nhds_iff.mp hu.mem_iff

Result:
case intro.intro.intro
H : Type u_1
H' : Type u_3
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace H'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
hG : G.LocalInvariantProp G' P
s t : Set H
x : H
f : H → H'
hu : s =ᶠ[𝓝 x] t
o : Set H
host : o ⊆ {x | (fun x => x ∈ s ↔ x ∈ t) x}
ho : IsOpen o
hxo : x ∈ o
⊢ P f s x ↔ P f t x
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem χ₄_int_eq_if_mod_four (n : ℤ) :
    χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1

Proof state:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ χ₄ ↑(n % ↑4) = if n % 4 % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1

Tactic:
exact help (n % 4) (Int.emod_nonneg n (by omega)) (Int.emod_lt n (by omega))

Result:
no goals

Proof state:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ 2 ∣ 4

Tactic:
omega

Result:
no goals

Proof state:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ 4 ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
n : ℤ
⊢ χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1

Tactic:
have help : ∀ m : ℤ, 0 ≤ m → m < 4 → χ₄ m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1 := by
  decide

Result:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1

Proof state:
n : ℤ
⊢ ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1

Tactic:
decide

Result:
no goals

Proof state:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1

Tactic:
rw [← Int.emod_emod_of_dvd n (by omega : (2 : ℤ) ∣ 4), ← ZMod.intCast_mod n 4]

Result:
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ χ₄ ↑(n % ↑4) = if n % 4 % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
lemma cons_tail_eq (p : G.Walk x y) (hp : ¬ p.Nil) :
    cons (p.adj_snd hp) p.tail = p

Proof state:
V : Type u
G : SimpleGraph V
x y : V
p : G.Walk x y
hp : ¬p.Nil
⊢ cons ⋯ p.tail = p

Tactic:
cases p with
| nil => simp at hp
| cons h q =>
  simp only [getVert_cons_succ, tail_cons_eq, cons_copy, copy_rfl_rfl]

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
x : V
hp : ¬nil.Nil
⊢ cons ⋯ nil.tail = nil

Tactic:
simp at hp

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
x y v✝ : V
h : G.Adj x v✝
q : G.Walk v✝ y
hp : ¬(cons h q).Nil
⊢ cons ⋯ (cons h q).tail = cons h q

Tactic:
simp only [getVert_cons_succ, tail_cons_eq, cons_copy, copy_rfl_rfl]

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem ret_supports {S k} (H₁ : contSupp k ⊆ S) : TM2.SupportsStmt S (tr (Λ'.ret k))

Proof state:
case fix
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type ?u.200775} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
R : ∀ {α : Type ?u.200797} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t
s : Option Γ'
⊢ (bif natEnd s.iget then Λ'.ret a✝ else Λ'.clear natEnd main (trNormal a✝¹ (Cont'.fix a✝¹ a✝))) ∈ S

Tactic:
cases natEnd s.iget

Result:
case fix.false
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type ?u.200775} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
R : ∀ {α : Type ?u.200797} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t
s : Option Γ'
⊢ (bif false then Λ'.ret a✝ else Λ'.clear natEnd main (trNormal a✝¹ (Cont'.fix a✝¹ a✝))) ∈ S

case fix.true
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type ?u.200775} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
R : ∀ {α : Type ?u.200797} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t
s : Option Γ'
⊢ (bif true then Λ'.ret a✝ else Λ'.clear natEnd main (trNormal a✝¹ (Cont'.fix a✝¹ a✝))) ∈ S

Proof state:
case fix.false
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
a✝¹ : Code
a✝ : Cont'
H₁ : codeSupp a✝¹ (Cont'.fix a✝¹ a✝) ⊆ S
L : ∀ {α : Type ?u.200775} [inst : DecidableEq α] {s : Finset α} {a : α} (t : Finset α), a ∈ s → a ∈ s ∪ t
R : ∀ {α : Type ?u.200797} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t
s : Option Γ'
⊢ (bif false then Λ'.ret a✝ else Λ'.clear natEnd main (trNormal a✝¹ (Cont'.fix a✝¹ a✝))) ∈ S

Tactic:
refine H₁ (R _ <| L _ <| R _ <| R _ <| L _ W)

Result:
no goals
-- Mathlib/Order/Ideal.lean
theorem inter_nonempty [IsDirected P (· ≥ ·)] (I J : Ideal P) : (I ∩ J : Set P).Nonempty

Proof state:
case intro
P : Type u_1
inst✝¹ : LE P
inst✝ : IsDirected P fun x1 x2 => x1 ≥ x2
I J : Ideal P
a : P
ha : a ∈ ↑I
⊢ (↑I ∩ ↑J).Nonempty

Tactic:
obtain ⟨b, hb⟩ := J.nonempty

Result:
case intro.intro
P : Type u_1
inst✝¹ : LE P
inst✝ : IsDirected P fun x1 x2 => x1 ≥ x2
I J : Ideal P
a : P
ha : a ∈ ↑I
b : P
hb : b ∈ ↑J
⊢ (↑I ∩ ↑J).Nonempty

Proof state:
case intro.intro.intro.intro
P : Type u_1
inst✝¹ : LE P
inst✝ : IsDirected P fun x1 x2 => x1 ≥ x2
I J : Ideal P
a : P
ha : a ∈ ↑I
b : P
hb : b ∈ ↑J
c : P
hac : c ≤ a
hbc : c ≤ b
⊢ (↑I ∩ ↑J).Nonempty

Tactic:
exact ⟨c, I.lower hac ha, J.lower hbc hb⟩

Result:
no goals

Proof state:
P : Type u_1
inst✝¹ : LE P
inst✝ : IsDirected P fun x1 x2 => x1 ≥ x2
I J : Ideal P
⊢ (↑I ∩ ↑J).Nonempty

Tactic:
obtain ⟨a, ha⟩ := I.nonempty

Result:
case intro
P : Type u_1
inst✝¹ : LE P
inst✝ : IsDirected P fun x1 x2 => x1 ≥ x2
I J : Ideal P
a : P
ha : a ∈ ↑I
⊢ (↑I ∩ ↑J).Nonempty

Proof state:
case intro.intro
P : Type u_1
inst✝¹ : LE P
inst✝ : IsDirected P fun x1 x2 => x1 ≥ x2
I J : Ideal P
a : P
ha : a ∈ ↑I
b : P
hb : b ∈ ↑J
⊢ (↑I ∩ ↑J).Nonempty

Tactic:
obtain ⟨c, hac, hbc⟩ := exists_le_le a b

Result:
case intro.intro.intro.intro
P : Type u_1
inst✝¹ : LE P
inst✝ : IsDirected P fun x1 x2 => x1 ≥ x2
I J : Ideal P
a : P
ha : a ∈ ↑I
b : P
hb : b ∈ ↑J
c : P
hac : c ≤ a
hbc : c ≤ b
⊢ (↑I ∩ ↑J).Nonempty
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem unattach_attachWith {p : α → Prop} {l : List α}
    {H : ∀ a ∈ l, p a} :
    (l.attachWith p H).unattach = l

Proof state:
case cons
α : Type u_1
p : α → Prop
a : α
l : List α
ih : ∀ {H : ∀ (a : α), a ∈ l → p a}, map (fun x => x.val) (l.attachWith p H) = l
H : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ map (fun x => x.val) ((a :: l).attachWith p H) = a :: l

Tactic:
simp [ih, Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : List α
H : ∀ (a : α), a ∈ l → p a
⊢ map (fun x => x.val) (l.attachWith p H) = l

Tactic:
induction l with
| nil => simp
| cons a l ih => simp [ih, Function.comp_def]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Prop
H : ∀ (a : α), a ∈ [] → p a
⊢ map (fun x => x.val) ([].attachWith p H) = []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : List α
H : ∀ (a : α), a ∈ l → p a
⊢ (l.attachWith p H).unattach = l

Tactic:
unfold unattach

Result:
α : Type u_1
p : α → Prop
l : List α
H : ∀ (a : α), a ∈ l → p a
⊢ map (fun x => x.val) (l.attachWith p H) = l
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.inner_finsupp_eq_sum_right {v : ι → E} (hv : Orthonormal 𝕜 v) (l₁ l₂ : ι →₀ 𝕜) :
    ⟪linearCombination 𝕜 v l₁, linearCombination 𝕜 v l₂⟫ = l₂.sum fun i y => conj (l₁ i) * y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l₁ l₂ : ι →₀ 𝕜
⊢ inner ((linearCombination 𝕜 v) l₁) ((linearCombination 𝕜 v) l₂) = l₂.sum fun i y => (starRingEnd 𝕜) (l₁ i) * y

Tactic:
simp only [l₂.linearCombination_apply _, Finsupp.inner_sum, hv.inner_left_finsupp, mul_comm,
           smul_eq_mul]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
/--
Induction on integers: prove a proposition `p i` by proving the base case `p 0`,
the upwards induction step `p i → p (i + 1)` and the downwards induction step `p (-i) → p (-i - 1)`.

It is used as the default induction principle for the `induction` tactic.
-/
@[elab_as_elim, induction_eliminator] protected lemma induction_on {p : ℤ → Prop} (i : ℤ)
    (hz : p 0) (hp : ∀ i : ℕ, p i → p (i + 1)) (hn : ∀ i : ℕ, p (-i) → p (-i - 1)) : p i

Proof state:
p : ℤ → Prop
i : ℤ
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
⊢ p i

Tactic:
cases i with
| ofNat i =>
  induction i with
  | zero => exact hz
  | succ i ih => exact hp _ ih
| negSucc i =>
  suffices ∀ n : ℕ, p (-n) from this (i + 1)
  intro n; induction n with
  | zero => simp [hz]
  | succ n ih => simpa [ofNat_succ, Int.neg_add, Int.sub_eq_add_neg] using hn _ ih

Result:
no goals

Proof state:
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i n : ℕ
⊢ p (-↑n)

Tactic:
induction n with
| zero => simp [hz]
| succ n ih => simpa [ofNat_succ, Int.neg_add, Int.sub_eq_add_neg] using hn _ ih

Result:
no goals

Proof state:
case ofNat
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p (ofNat i)

Tactic:
induction i with
| zero => exact hz
| succ i ih => exact hp _ ih

Result:
no goals

Proof state:
case negSucc.succ
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i n : ℕ
ih : p (-↑n)
⊢ p (-↑(n + 1))

Tactic:
simpa [ofNat_succ, Int.neg_add, Int.sub_eq_add_neg] using hn _ ih

Result:
no goals

Proof state:
case ofNat.succ
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
ih : p (ofNat i)
⊢ p (ofNat (i + 1))

Tactic:
exact hp _ ih

Result:
no goals

Proof state:
case ofNat.zero
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
⊢ p (ofNat 0)

Tactic:
exact hz

Result:
no goals

Proof state:
case negSucc.zero
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p (-↑0)

Tactic:
simp [hz]

Result:
no goals

Proof state:
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ p -[i+1]

Tactic:
suffices ∀ n : ℕ, p (-n) from this (i + 1)

Result:
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ ∀ (n : ℕ), p (-↑n)

Proof state:
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i : ℕ
⊢ ∀ (n : ℕ), p (-↑n)

Tactic:
intro n

Result:
case negSucc
p : ℤ → Prop
hz : p 0
hp : ∀ (i : ℕ), p ↑i → p (↑i + 1)
hn : ∀ (i : ℕ), p (-↑i) → p (-↑i - 1)
i n : ℕ
⊢ p (-↑n)