harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem disjoint_splitLower_splitUpper (I : Box ι) (i : ι) (x : ℝ) :
    Disjoint (I.splitLower i x) (I.splitUpper i x)

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (↑I ∩ {y | y i ≤ x}) (↑I ∩ {y | x < y i})

Tactic:
refine (Disjoint.inf_left' _ ?_).inf_right' _

Result:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint {y | y i ≤ x} {y | x < y i}

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint {y | y i ≤ x} {y | x < y i}

Tactic:
rw [Set.disjoint_left]

Result:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ∀ ⦃a : ι → ℝ⦄, a ∈ {y | y i ≤ x} → a ∉ {y | x < y i}

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (I.splitLower i x) (I.splitUpper i x)

Tactic:
rw [← disjoint_withBotCoe, coe_splitLower, coe_splitUpper]

Result:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (↑I ∩ {y | y i ≤ x}) (↑I ∩ {y | x < y i})

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ ∀ ⦃a : ι → ℝ⦄, a ∈ {y | y i ≤ x} → a ∉ {y | x < y i}

Tactic:
exact fun y (hle : y i ≤ x) hlt => not_lt_of_le hle hlt

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
@[to_additive]
lemma smul_smul_smul_comm [SMul α β] [SMul α γ] [SMul β δ] [SMul α δ] [SMul γ δ]
    [IsScalarTower α β δ] [IsScalarTower α γ δ] [SMulCommClass β γ δ] (a : α) (b : β) (c : γ)
    (d : δ) : (a • b) • c • d = (a • c) • b • d

Proof state:
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul α β
inst✝⁶ : SMul α γ
inst✝⁵ : SMul β δ
inst✝⁴ : SMul α δ
inst✝³ : SMul γ δ
inst✝² : IsScalarTower α β δ
inst✝¹ : IsScalarTower α γ δ
inst✝ : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
⊢ (a • b) • c • d = (a • c) • b • d

Tactic:
rw [smul_assoc, smul_assoc, smul_comm b]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem hasFTaylorSeriesUpTo_succ_nat_iff_right {n : ℕ} :
    HasFTaylorSeriesUpTo (n + 1 : ℕ) f p ↔
      (∀ x, (p x 0).curry0 = f x) ∧
        (∀ x, HasFDerivAt (fun y => p y 0) (p x 1).curryLeft x) ∧
          HasFTaylorSeriesUpTo n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1)) fun x =>
            (p x).shift

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ HasFTaylorSeriesUpTo (↑(n + 1)) f p ↔
    (∀ (x : E), (p x 0).curry0 = f x) ∧
      (∀ (x : E), HasFDerivAt (fun y => p y 0) (p x 1).curryLeft x) ∧
        HasFTaylorSeriesUpTo (↑n) (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) fun x => (p x).shift

Tactic:
simp only [hasFTaylorSeriesUpToOn_succ_nat_iff_right, ← hasFTaylorSeriesUpToOn_univ_iff, mem_univ,
  forall_true_left, hasFDerivWithinAt_univ]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iic_union_Icc (h : min c d ≤ b) : Iic b ∪ Icc c d = Iic (max b d)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
b c d : α
h : c ⊓ d ≤ b
⊢ Iic b ∪ Icc c d = Iic (b ⊔ d)

Tactic:
rcases le_or_lt c d with hcd | hcd <;> simp [hcd] at h

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : c ≤ d
h : c ≤ b
⊢ Iic b ∪ Icc c d = Iic (b ⊔ d)

case inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d < c
h : c ≤ b ∨ d ≤ b
⊢ Iic b ∪ Icc c d = Iic (b ⊔ d)

Proof state:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d < c
h : d ≤ b
⊢ Iic b ∪ Icc c d = Iic (b ⊔ d)

Tactic:
simp [*]

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d < c
h : c ≤ b
⊢ Iic b ∪ Icc c d = Iic (b ⊔ d)

Tactic:
have hdb : d ≤ b := hcd.le.trans h

Result:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d < c
h : c ≤ b
hdb : d ≤ b
⊢ Iic b ∪ Icc c d = Iic (b ⊔ d)

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d < c
h : c ≤ b ∨ d ≤ b
⊢ Iic b ∪ Icc c d = Iic (b ⊔ d)

Tactic:
rcases h with h | h

Result:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d < c
h : c ≤ b
⊢ Iic b ∪ Icc c d = Iic (b ⊔ d)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d < c
h : d ≤ b
⊢ Iic b ∪ Icc c d = Iic (b ⊔ d)

Proof state:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : d < c
h : c ≤ b
hdb : d ≤ b
⊢ Iic b ∪ Icc c d = Iic (b ⊔ d)

Tactic:
simp [*]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
b c d : α
hcd : c ≤ d
h : c ≤ b
⊢ Iic b ∪ Icc c d = Iic (b ⊔ d)

Tactic:
exact Iic_union_Icc' h

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem decay_add_le_aux (k n : ℕ) (f g : 𝓢(E, F)) (x : E) :
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n ((f : E → F) + (g : E → F)) x‖ ≤
      ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ + ‖x‖ ^ k * ‖iteratedFDeriv ℝ n g x‖

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤ ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖

Tactic:
rw [iteratedFDeriv_add_apply (f.smooth _).contDiffAt (g.smooth _).contDiffAt]

Result:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖iteratedFDeriv ℝ n (⇑f) x + iteratedFDeriv ℝ n (⇑g) x‖ ≤ ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ 0 ≤ ‖x‖ ^ k

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤ ‖x‖ ^ k * (‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖)

Tactic:
refine mul_le_mul_of_nonneg_left ?_ (by positivity)

Result:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤ ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑g) x‖

Tactic:
rw [← mul_add]

Result:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f + ⇑g) x‖ ≤ ‖x‖ ^ k * (‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖)

Proof state:
E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖iteratedFDeriv ℝ n (⇑f) x + iteratedFDeriv ℝ n (⇑g) x‖ ≤ ‖iteratedFDeriv ℝ n (⇑f) x‖ + ‖iteratedFDeriv ℝ n (⇑g) x‖

Tactic:
exact norm_add_le _ _

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDense.lean
theorem nearestPtInd_le (e : ℕ → α) (N : ℕ) (x : α) : nearestPtInd e N x ≤ N

Proof state:
case succ
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
⊢ (nearestPtInd e (N + 1)) x ≤ N + 1

Tactic:
simp only [nearestPtInd_succ]

Result:
case succ
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
⊢ (if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N) x) ≤ N + 1

Proof state:
case succ
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
⊢ (if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N) x) ≤ N + 1

Tactic:
split_ifs

Result:
case pos
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
h✝ : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ N + 1 ≤ N + 1

case neg
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
h✝ : ¬∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ (nearestPtInd e N) x ≤ N + 1

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ (nearestPtInd e N) x ≤ N

Tactic:
induction' N with N ihN

Result:
case zero
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
⊢ (nearestPtInd e 0) x ≤ 0

case succ
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
⊢ (nearestPtInd e (N + 1)) x ≤ N + 1

Proof state:
case zero
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
⊢ (nearestPtInd e 0) x ≤ 0

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
h✝ : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ N + 1 ≤ N + 1

case neg
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N) x ≤ N
h✝ : ¬∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ (nearestPtInd e N) x ≤ N + 1

Tactic:
exacts [le_rfl, ihN.trans N.le_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem ne_and_not_mem_of_not_mem_push {a y : α} {l : Array α} : a ∉ l.push y → a ≠ y ∧ a ∉ l

Proof state:
α : Type u_1
a y : α
l : Array α
⊢ ¬a ∈ l.push y → a ≠ y ∧ ¬a ∈ l

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Defs.lean
theorem xgcd_zero_left {s t r' s' t' : R} : xgcdAux 0 s t r' s' t' = (r', s', t')

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s t r' s' t' : R
⊢ (if _hr : 0 = 0 then (r', s', t')
    else
      let q := r' / 0;
      let_fun x := ⋯;
      xgcdAux (r' % 0) (s' - q * s) (t' - q * t) 0 s t) =
    (r', s', t')

Tactic:
exact if_pos rfl

Result:
no goals

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s t r' s' t' : R
⊢ xgcdAux 0 s t r' s' t' = (r', s', t')

Tactic:
unfold xgcdAux

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
s t r' s' t' : R
⊢ (if _hr : 0 = 0 then (r', s', t')
    else
      let q := r' / 0;
      let_fun x := ⋯;
      xgcdAux (r' % 0) (s' - q * s) (t' - q * t) 0 s t) =
    (r', s', t')
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem sum_lt_prod {ι} (f g : ι → Cardinal) (H : ∀ i, f i < g i) : sum f < prod g :=
  lt_of_not_ge fun ⟨F⟩ => by
    have : Inhabited (∀ i : ι, (g i).out)

Proof state:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ⇑F
sG : Surjective G
C : (i : ι) → Quotient.out (g i)
hc : ∀ (i : ι) (a : Quotient.out (f i)), G ⟨i, a⟩ i ≠ C i
i : ι
a : Quotient.out (f i)
h : G ⟨i, a⟩ = C
⊢ False

Tactic:
exact hc i a (congr_fun h _)

Result:
no goals

Proof state:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
⊢ False

Tactic:
let G := invFun F

Result:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : sum f ≥ prod g
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ⇑F
⊢ False
-- Mathlib/RingTheory/WittVector/WittPolynomial.lean
theorem xInTermsOfW_aux [Invertible (p : R)] (n : ℕ) :
    xInTermsOfW p R n * C ((p : R) ^ n) =
      X n - ∑ i ∈ range n, C ((p : R) ^ i) * xInTermsOfW p R i ^ p ^ (n - i)

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible ↑p
n : ℕ
⊢ xInTermsOfW p R n * C (↑p ^ n) = X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)

Tactic:
rw [xInTermsOfW_eq, mul_assoc, ← C_mul, ← mul_pow, invOf_mul_self,
  one_pow, C_1, mul_one]

Result:
no goals
-- Mathlib/Topology/Perfect.lean
theorem perfectSpace_iff_forall_not_isolated : PerfectSpace X ↔ ∀ x : X, Filter.NeBot (𝓝[≠] x)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ PerfectSpace X ↔ ∀ (x : X), (𝓝[≠] x).NeBot

Tactic:
simp [perfectSpace_def, Preperfect, AccPt]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/ModuleTopology.lean
theorem continuous_bilinear_of_finite_left [Module.Finite R A]
    (bil : A →ₗ[R] B →ₗ[R] C) : Continuous (fun ab ↦ bil ab.1 ab.2 : (A × B → C))

Proof state:
case intro.intro
R : Type u_1
inst✝¹² : TopologicalSpace R
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsTopologicalRing R
A : Type u_2
inst✝⁹ : AddCommGroup A
inst✝⁸ : Module R A
aA : TopologicalSpace A
inst✝⁷ : IsModuleTopology R A
B : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module R B
aB : TopologicalSpace B
inst✝⁴ : IsModuleTopology R B
C : Type u_4
inst✝³ : AddCommGroup C
inst✝² : Module R C
aC : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
inst✝ : Module.Finite R A
bil : A →ₗ[R] B →ₗ[R] C
m : ℕ
f : (Fin m → R) →ₗ[R] A
hf : Function.Surjective ⇑f
bil' : (Fin m → R) →ₗ[R] B →ₗ[R] C := bil ∘ₗ f
φ : (Fin m → R) × B →ₗ[R] A × B := f.prodMap LinearMap.id
⊢ Continuous fun ab => (bil ab.1) ab.2

Tactic:
have hφ : Function.Surjective φ := Function.Surjective.prodMap hf fun b ↦ ⟨b, rfl⟩

Result:
case intro.intro
R : Type u_1
inst✝¹² : TopologicalSpace R
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsTopologicalRing R
A : Type u_2
inst✝⁹ : AddCommGroup A
inst✝⁸ : Module R A
aA : TopologicalSpace A
inst✝⁷ : IsModuleTopology R A
B : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module R B
aB : TopologicalSpace B
inst✝⁴ : IsModuleTopology R B
C : Type u_4
inst✝³ : AddCommGroup C
inst✝² : Module R C
aC : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
inst✝ : Module.Finite R A
bil : A →ₗ[R] B →ₗ[R] C
m : ℕ
f : (Fin m → R) →ₗ[R] A
hf : Function.Surjective ⇑f
bil' : (Fin m → R) →ₗ[R] B →ₗ[R] C := bil ∘ₗ f
φ : (Fin m → R) × B →ₗ[R] A × B := f.prodMap LinearMap.id
hφ : Function.Surjective ⇑φ
⊢ Continuous fun ab => (bil ab.1) ab.2
-- Mathlib/Computability/Halting.lean
theorem to_re {p : α → Prop} (hp : ComputablePred p) : REPred p

Proof state:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ REPred fun a => f a = true

Tactic:
unfold REPred

Result:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ Partrec fun a => Part.assert ((fun a => f a = true) a) fun x => Part.some ()

Proof state:
α : Type u_1
inst✝ : Primcodable α
p : α → Prop
hp : ComputablePred p
⊢ REPred p

Tactic:
obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp

Result:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ REPred fun a => f a = true

Proof state:
case intro.intro.unit
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
⊢ (PUnit.unit ∈ bif f n then Part.some () else Part.none) ↔ PUnit.unit ∈ Part.assert (f n = true) fun x => Part.some ()

Tactic:
cases f n <;> simp

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
a : Unit
⊢ (a ∈ bif f n then Part.some () else Part.none) ↔ a ∈ Part.assert (f n = true) fun x => Part.some ()

Tactic:
cases a

Result:
case intro.intro.unit
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
⊢ (PUnit.unit ∈ bif f n then Part.some () else Part.none) ↔ PUnit.unit ∈ Part.assert (f n = true) fun x => Part.some ()

Proof state:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ Partrec fun a => Part.assert ((fun a => f a = true) a) fun x => Part.some ()

Tactic:
dsimp only []

Result:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ Partrec fun a => Part.assert (f a = true) fun x => Part.some ()

Proof state:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
⊢ Partrec fun a => Part.assert (f a = true) fun x => Part.some ()

Tactic:
refine
  (Partrec.cond hf (Decidable.Partrec.const' (Part.some ())) Partrec.none).of_eq fun n =>
    Part.ext fun a => ?_

Result:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → Bool
hf : Computable f
hp : ComputablePred fun a => f a = true
n : α
a : Unit
⊢ (a ∈ bif f n then Part.some () else Part.none) ↔ a ∈ Part.assert (f n = true) fun x => Part.some ()
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_cons_concat_apply_last (x y : α) (xs : List α) :
    formPerm (x :: (xs ++ [y])) y = x

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
z : α
xs : List α
IH : ∀ (x y : α), (x :: (xs ++ [y])).formPerm y = x
x y : α
⊢ (x :: (z :: xs ++ [y])).formPerm y = x

Tactic:
simp [IH]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (x :: ([] ++ [y])).formPerm y = x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
⊢ (x :: (xs ++ [y])).formPerm y = x

Tactic:
induction' xs with z xs IH generalizing x y

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (x :: ([] ++ [y])).formPerm y = x

case cons
α : Type u_1
inst✝ : DecidableEq α
z : α
xs : List α
IH : ∀ (x y : α), (x :: (xs ++ [y])).formPerm y = x
x y : α
⊢ (x :: (z :: xs ++ [y])).formPerm y = x
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem range_mkQ : range p.mkQ = ⊤ :=
  eq_top_iff'.2 <| by rintro ⟨x⟩; exact ⟨x, rfl⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
⊢ ∀ (x : M ⧸ p), x ∈ range p.mkQ

Tactic:
rintro ⟨x⟩

Result:
case mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x✝ : M ⧸ p
x : M
⊢ Quot.mk (⇑p.quotientRel) x ∈ range p.mkQ

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x✝ : M ⧸ p
x : M
⊢ Quot.mk (⇑p.quotientRel) x ∈ range p.mkQ

Tactic:
exact ⟨x, rfl⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_closedBall_eq_addHaar_ball [Nontrivial E] (x : E) (r : ℝ) :
    μ (closedBall x r) = μ (ball x r)

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ μ (closedBall x r) = μ (ball x r)

Tactic:
by_cases h : r < 0

Result:
case pos
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
h : r < 0
⊢ μ (closedBall x r) = μ (ball x r)

case neg
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
h : ¬r < 0
⊢ μ (closedBall x r) = μ (ball x r)

Proof state:
case pos
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
h : r < 0
⊢ μ (closedBall x r) = μ (ball x r)

Tactic:
rw [Metric.closedBall_eq_empty.mpr h, Metric.ball_eq_empty.mpr h.le]

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
h : 0 ≤ r
⊢ μ (closedBall x r) = μ (ball x r)

Tactic:
rw [addHaar_closedBall μ x h, addHaar_ball μ x h]

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
h : ¬r < 0
⊢ μ (closedBall x r) = μ (ball x r)

Tactic:
push_neg at h

Result:
case neg
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
h : 0 ≤ r
⊢ μ (closedBall x r) = μ (ball x r)
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_sub_const_Iio : (fun x => x - a) ⁻¹' Iio b = Iio (b + a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => x - a) ⁻¹' Iio b = Iio (b + a)

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Zip.lean
theorem go_get {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr)
    (lhs rhs : RefVec aig len) (f : (aig : AIG α) → BinaryInput aig → Entrypoint α)
    [LawfulOperator α BinaryInput f] [chainable : LawfulZipOperator α f] :
    ∀ (idx : Nat) (hidx : idx < curr),
      (go aig curr s hcurr lhs rhs f).vec.get idx (by omega)
        =
      (s.get idx hidx).cast (by apply go_le_size)

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig curr s hcurr lhs rhs f).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Tactic:
apply go_get_aux

Result:
no goals

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx : idx < curr
⊢ aig.decls.size ≤ (go aig curr s hcurr lhs rhs f).aig.decls.size

Tactic:
apply go_le_size

Result:
no goals

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
⊢ ∀ (idx : Nat) (hidx : idx < curr), (go aig curr s hcurr lhs rhs f).vec.get idx ⋯ = (s.get idx hidx).cast ⋯

Tactic:
intros

Result:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig curr s hcurr lhs rhs f).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
aig✝ : AIG α
len : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ len
s : aig.RefVec curr
lhs rhs : aig.RefVec len
f : (aig : AIG α) → aig.BinaryInput → Entrypoint α
inst✝ : LawfulOperator α BinaryInput f
chainable : LawfulZipOperator α f
idx : Nat
hidx : idx < curr
⊢ idx < len

Tactic:
omega

Result:
no goals