harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem reverse_eq_iff {as bs : List α} : as.reverse = bs ↔ as = bs.reverse

Proof state:
case mpr
α : Type u_1
bs : List α
⊢ bs.reverse.reverse = bs

Tactic:
simp

Result:
no goals

Proof state:
case mpr
α : Type u_1
as bs : List α
⊢ as = bs.reverse → as.reverse = bs

Tactic:
rintro rfl

Result:
case mpr
α : Type u_1
bs : List α
⊢ bs.reverse.reverse = bs

Proof state:
α : Type u_1
as bs : List α
⊢ as.reverse = bs ↔ as = bs.reverse

Tactic:
constructor <;> (rintro rfl; simp)

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem addLECancellable_iff_ne {a : ℝ≥0∞} : AddLECancellable a ↔ a ≠ ∞

Proof state:
a : ℝ≥0∞
⊢ AddLECancellable a ↔ a ≠ ⊤

Tactic:
constructor

Result:
case mp
a : ℝ≥0∞
⊢ AddLECancellable a → a ≠ ⊤

case mpr
a : ℝ≥0∞
⊢ a ≠ ⊤ → AddLECancellable a

Proof state:
case mpr
a : ℝ≥0∞
⊢ a ≠ ⊤ → AddLECancellable a

Tactic:
rintro h b c hbc

Result:
case mpr
a : ℝ≥0∞
h : a ≠ ⊤
b c : ℝ≥0∞
hbc : a + b ≤ a + c
⊢ b ≤ c

Proof state:
case mpr
a : ℝ≥0∞
h : a ≠ ⊤
b c : ℝ≥0∞
hbc : a + b ≤ a + c
⊢ b ≤ c

Tactic:
apply ENNReal.le_of_add_le_add_left h hbc

Result:
no goals

Proof state:
case mp
h : AddLECancellable ⊤
⊢ ⊤ + 1 ≤ ⊤ + 0

Tactic:
simp

Result:
no goals

Proof state:
case mp
a : ℝ≥0∞
⊢ AddLECancellable a → a ≠ ⊤

Tactic:
rintro h rfl

Result:
case mp
h : AddLECancellable ⊤
⊢ False

Proof state:
case mp
h : AddLECancellable ⊤
⊢ False

Tactic:
refine zero_lt_one.not_le (h ?_)

Result:
case mp
h : AddLECancellable ⊤
⊢ ⊤ + 1 ≤ ⊤ + 0
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_one_sub_smoothingFn_gt_const_real (c : ℝ) (hc : c < 1) :
    ∀ᶠ (x : ℝ) in atTop, c < 1 - ε x

Proof state:
c : ℝ
hc : c < 1
h₁ : (∀ a' < 1, ∀ᶠ (b : ℝ) in atTop, a' < 1 - ε b) ∧ ∀ a' > 1, ∀ᶠ (b : ℝ) in atTop, 1 - ε b < a'
⊢ ∀ᶠ (x : ℝ) in atTop, c < 1 - ε x

Tactic:
exact h₁.1 c hc

Result:
no goals

Proof state:
c : ℝ
hc : c < 1
h₁ : Tendsto (fun x => 1 - ε x) atTop (𝓝 1)
⊢ ∀ᶠ (x : ℝ) in atTop, c < 1 - ε x

Tactic:
rw [tendsto_order] at h₁

Result:
c : ℝ
hc : c < 1
h₁ : (∀ a' < 1, ∀ᶠ (b : ℝ) in atTop, a' < 1 - ε b) ∧ ∀ a' > 1, ∀ᶠ (b : ℝ) in atTop, 1 - ε b < a'
⊢ ∀ᶠ (x : ℝ) in atTop, c < 1 - ε x

Proof state:
c : ℝ
hc : c < 1
⊢ Tendsto (fun x => 1 - ε x) atTop (𝓝 1)

Tactic:
rw [← isEquivalent_const_iff_tendsto one_ne_zero]

Result:
c : ℝ
hc : c < 1
⊢ (fun x => 1 - ε x) ~[atTop] Function.const ℝ 1

Proof state:
c : ℝ
hc : c < 1
⊢ ∀ᶠ (x : ℝ) in atTop, c < 1 - ε x

Tactic:
have h₁ : Tendsto (fun x => 1 - ε x) atTop (𝓝 1) := by
  rw [← isEquivalent_const_iff_tendsto one_ne_zero]
  exact isEquivalent_one_sub_smoothingFn_one

Result:
c : ℝ
hc : c < 1
h₁ : Tendsto (fun x => 1 - ε x) atTop (𝓝 1)
⊢ ∀ᶠ (x : ℝ) in atTop, c < 1 - ε x

Proof state:
c : ℝ
hc : c < 1
⊢ (fun x => 1 - ε x) ~[atTop] Function.const ℝ 1

Tactic:
exact isEquivalent_one_sub_smoothingFn_one

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_eq_size_eq_zero : m.1.isEmpty = (m.1.size == 0)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
⊢ m.val.isEmpty = (m.val.size == 0)

Tactic:
simp [Raw.isEmpty]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/SubboxInduction.lean
theorem distortion_unionComplToSubordinate (π₁ : TaggedPrepartition I) (π₂ : Prepartition I)
    (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → Ioi (0 : ℝ)) :
    (π₁.unionComplToSubordinate π₂ hU r).distortion = max π₁.distortion π₂.distortion

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
π₁ : TaggedPrepartition I
π₂ : Prepartition I
hU : π₂.iUnion = ↑I \ π₁.iUnion
r : (ι → ℝ) → ↑(Ioi 0)
⊢ (π₁.unionComplToSubordinate π₂ hU r).distortion = π₁.distortion ⊔ π₂.distortion

Tactic:
simp [unionComplToSubordinate]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem ι_sq_scalar (m : M) : ι Q m * ι Q m = algebraMap R _ (Q m)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (RingQuot.mkAlgHom R (Rel Q)).toLinearMap ((TensorAlgebra.ι R) m) *
      (RingQuot.mkAlgHom R (Rel Q)).toLinearMap ((TensorAlgebra.ι R) m) =
    (algebraMap R (CliffordAlgebra Q)) (Q m)

Tactic:
rw [AlgHom.toLinearMap_apply, ← map_mul (RingQuot.mkAlgHom R (Rel Q)),
  RingQuot.mkAlgHom_rel R (Rel.of m), AlgHom.commutes]

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (algebraMap R (RingQuot (Rel Q))) (Q m) = (algebraMap R (CliffordAlgebra Q)) (Q m)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (ι Q) m * (ι Q) m = (algebraMap R (CliffordAlgebra Q)) (Q m)

Tactic:
rw [ι]

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ((RingQuot.mkAlgHom R (Rel Q)).toLinearMap ∘ₗ TensorAlgebra.ι R) m *
      ((RingQuot.mkAlgHom R (Rel Q)).toLinearMap ∘ₗ TensorAlgebra.ι R) m =
    (algebraMap R (CliffordAlgebra Q)) (Q m)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ ((RingQuot.mkAlgHom R (Rel Q)).toLinearMap ∘ₗ TensorAlgebra.ι R) m *
      ((RingQuot.mkAlgHom R (Rel Q)).toLinearMap ∘ₗ TensorAlgebra.ι R) m =
    (algebraMap R (CliffordAlgebra Q)) (Q m)

Tactic:
erw [LinearMap.comp_apply]

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (RingQuot.mkAlgHom R (Rel Q)).toLinearMap ((TensorAlgebra.ι R) m) *
      (RingQuot.mkAlgHom R (Rel Q)).toLinearMap ((TensorAlgebra.ι R) m) =
    (algebraMap R (CliffordAlgebra Q)) (Q m)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ (algebraMap R (RingQuot (Rel Q))) (Q m) = (algebraMap R (CliffordAlgebra Q)) (Q m)

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_prod (α β : Type*) : Nat.card (α × β) = Nat.card α * Nat.card β

Proof state:
α : Type u_3
β : Type u_4
⊢ Nat.card (α × β) = Nat.card α * Nat.card β

Tactic:
simp only [Nat.card, mk_prod, toNat_mul, toNat_lift]

Result:
no goals
-- Mathlib/Analysis/Convex/Intrinsic.lean
theorem Set.Nonempty.intrinsicInterior (hscv : Convex ℝ s) (hsne : s.Nonempty) :
    (intrinsicInterior ℝ s).Nonempty

Proof state:
case intro
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩
⊢ Convex ℝ (⇑(AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph ⁻¹' (Subtype.val ⁻¹' s))

Tactic:
exact hscv.affine_preimage
  ((_root_.affineSpan ℝ s).subtype.comp
    (AffineIsometryEquiv.constVSub ℝ p').symm.toAffineEquiv.toAffineMap)

Result:
no goals

Proof state:
case intro
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
⊢ (intrinsicInterior ℝ s).Nonempty

Tactic:
let p' : _root_.affineSpan ℝ s := ⟨p, subset_affineSpan _ _ hp⟩

Result:
case intro
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩
⊢ (intrinsicInterior ℝ s).Nonempty

Proof state:
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
hsne : s.Nonempty
⊢ (intrinsicInterior ℝ s).Nonempty

Tactic:
haveI := hsne.coe_sort

Result:
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
hsne : s.Nonempty
this : Nonempty ↑s
⊢ (intrinsicInterior ℝ s).Nonempty

Proof state:
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
hsne : s.Nonempty
this : Nonempty ↑s
⊢ (intrinsicInterior ℝ s).Nonempty

Tactic:
obtain ⟨p, hp⟩ := hsne

Result:
case intro
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
⊢ (intrinsicInterior ℝ s).Nonempty

Proof state:
case intro
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩
⊢ (intrinsicInterior ℝ s).Nonempty

Tactic:
rw [intrinsicInterior, image_nonempty,
  aux (AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph,
  Convex.interior_nonempty_iff_affineSpan_eq_top, AffineIsometryEquiv.coe_toHomeomorph, ←
  AffineIsometryEquiv.coe_toAffineEquiv, ← comap_span, affineSpan_coe_preimage_eq_top, comap_top]

Result:
case intro
V : Type u_2
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
hscv : Convex ℝ s
this : Nonempty ↑s
p : V
hp : p ∈ s
p' : ↥(_root_.affineSpan ℝ s) := ⟨p, ⋯⟩
⊢ Convex ℝ (⇑(AffineIsometryEquiv.constVSub ℝ p').symm.toHomeomorph ⁻¹' (Subtype.val ⁻¹' s))
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem Equiv.hasProd_iff_of_mulSupport {g : γ → α} (e : mulSupport f ≃ mulSupport g)
    (he : ∀ x : mulSupport f, g (e x) = f x) : HasProd f a ↔ HasProd g a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : γ → α
e : ↑(mulSupport f) ≃ ↑(mulSupport g)
he : ∀ (x : ↑(mulSupport f)), g ↑(e x) = f ↑x
this : (g ∘ Subtype.val) ∘ ⇑e = f ∘ Subtype.val
⊢ HasProd f a ↔ HasProd g a

Tactic:
rw [← hasProd_subtype_mulSupport, ← this, e.hasProd_iff, hasProd_subtype_mulSupport]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : γ → α
e : ↑(mulSupport f) ≃ ↑(mulSupport g)
he : ∀ (x : ↑(mulSupport f)), g ↑(e x) = f ↑x
⊢ HasProd f a ↔ HasProd g a

Tactic:
have : (g ∘ (↑)) ∘ e = f ∘ (↑) := funext he

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
g : γ → α
e : ↑(mulSupport f) ≃ ↑(mulSupport g)
he : ∀ (x : ↑(mulSupport f)), g ↑(e x) = f ↑x
this : (g ∘ Subtype.val) ∘ ⇑e = f ∘ Subtype.val
⊢ HasProd f a ↔ HasProd g a
-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem norm_iteratedFDeriv_clm_apply_const {f : E → F →L[𝕜] G} {c : F} {x : E}
    {N : WithTop ℕ∞} {n : ℕ} (hf : ContDiffAt 𝕜 N f x) (hn : n ≤ N) :
    ‖iteratedFDeriv 𝕜 n (fun y : E => (f y) c) x‖ ≤ ‖c‖ * ‖iteratedFDeriv 𝕜 n f x‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
c : F
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffAt 𝕜 N f x
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun y => (f y) c) x‖ ≤ ‖c‖ * ‖iteratedFDeriv 𝕜 n f x‖

Tactic:
simp only [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
c : F
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffAt 𝕜 N f x
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) univ x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f univ x‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
c : F
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffAt 𝕜 N f x
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) univ x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f univ x‖

Tactic:
exact norm_iteratedFDerivWithin_clm_apply_const hf.contDiffWithinAt uniqueDiffOn_univ
  (Set.mem_univ x) hn

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_toBlocks (M : Matrix (n ⊕ o) (l ⊕ m) α) :
    fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ = M

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ = M

Tactic:
ext i j

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
i : n ⊕ o
j : l ⊕ m
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ i j = M i j

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
M : Matrix (n ⊕ o) (l ⊕ m) α
i : n ⊕ o
j : l ⊕ m
⊢ fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ i j = M i j

Tactic:
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem getElem?_insertIdx {l : List α} {x : α} {n k : Nat} :
    (insertIdx n x l)[k]? =
      if k < n then
        l[k]?
      else
        if k = n then
          if k ≤ l.length then some x else none
        else
          l[k-1]?

Proof state:
α : Type u
l : List α
x : α
n k : Nat
⊢ (if h : k < (insertIdx n x l).length then some (insertIdx n x l)[k] else none) =
    if k < n then l[k]? else if k = n then if k ≤ l.length then some x else none else l[k - 1]?

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u
l : List α
x : α
n k : Nat
h : k < (insertIdx n x l).length
⊢ some (insertIdx n x l)[k] =
    if k < n then l[k]? else if k = n then if k ≤ l.length then some x else none else l[k - 1]?

case isFalse
α : Type u
l : List α
x : α
n k : Nat
h : ¬k < (insertIdx n x l).length
⊢ none = if k < n then l[k]? else if k = n then if k ≤ l.length then some x else none else l[k - 1]?

Proof state:
case isFalse.isTrue
α : Type u
l : List α
x : α
n k : Nat
h : ¬k < if n ≤ l.length then l.length + 1 else l.length
h₁ : k < n
⊢ l.length ≤ k

Tactic:
split at h <;> omega

Result:
no goals

Proof state:
case isTrue
α : Type u
l : List α
x : α
n k : Nat
h✝ : k < (insertIdx n x l).length
h : k < if n ≤ l.length then l.length + 1 else l.length
⊢ some (if h₁ : k < n then l[k] else if h₂ : k = n then x else l[k - 1]) =
    if k < n then l[k]? else if k = n then if k ≤ l.length then some x else none else l[k - 1]?

Tactic:
split <;> rename_i h₁

Result:
case isTrue.isTrue
α : Type u
l : List α
x : α
n k : Nat
h✝ : k < (insertIdx n x l).length
h : k < if n ≤ l.length then l.length + 1 else l.length
h₁ : k < n
⊢ some l[k] = l[k]?

case isTrue.isFalse
α : Type u
l : List α
x : α
n k : Nat
h✝ : k < (insertIdx n x l).length
h : k < if n ≤ l.length then l.length + 1 else l.length
h₁ : ¬k < n
⊢ some (if h₂ : k = n then x else l[k - 1]) = if k = n then if k ≤ l.length then some x else none else l[k - 1]?

Proof state:
case isFalse.isFalse
α : Type u
l : List α
x : α
n k : Nat
h : ¬k < if n ≤ l.length then l.length + 1 else l.length
h₁ : ¬k < n
⊢ none = if k = n then if k ≤ l.length then some x else none else l[k - 1]?

Tactic:
split <;> rename_i h₂

Result:
case isFalse.isFalse.isTrue
α : Type u
l : List α
x : α
n k : Nat
h : ¬k < if n ≤ l.length then l.length + 1 else l.length
h₁ : ¬k < n
h₂ : k = n
⊢ none = if k ≤ l.length then some x else none

case isFalse.isFalse.isFalse
α : Type u
l : List α
x : α
n k : Nat
h : ¬k < if n ≤ l.length then l.length + 1 else l.length
h₁ : ¬k < n
h₂ : ¬k = n
⊢ none = l[k - 1]?
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_mapFinIdx (f : (i : Nat) → α → (h : i < n) → β) (v : Vector α n) :
    (v.mapFinIdx f).toList =
      v.toList.mapFinIdx (fun i a h => f i a (by simpa [v.size_toArray] using h))

Proof state:
α : Type u_1
n : Nat
β : Type u_2
f : (i : Nat) → α → i < n → β
v : Vector α n
⊢ (v.mapFinIdx f).toList = v.toList.mapFinIdx fun i a h => f i a ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.58283
n : Nat
β : Type ?u.58287
f : (i : Nat) → α → i < n → β
v : Vector α n
i : Nat
a : α
h : i < v.toList.length
⊢ i < n

Tactic:
simpa [v.size_toArray] using h

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Sigma.lean
theorem prod_finset_product_right (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α)
    (h : ∀ p : α × γ, p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α × γ → β} :
    ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (a, c)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (a, c)

Tactic:
refine Eq.trans ?_ (prod_sigma s t fun p => f (p.2, p.1))

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∏ p ∈ r, f p = ∏ x ∈ s.sigma t, f (x.snd, x.fst)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∏ p ∈ r, f p = ∏ x ∈ s.sigma t, f (x.snd, x.fst)

Tactic:
apply prod_equiv ((Equiv.prodComm _ _).trans (Equiv.sigmaEquivProd _ _).symm) <;> simp [h]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
theorem tendsto_IicSnd_atTop {s : Set α} (hs : MeasurableSet s) :
    Tendsto (fun r : ℚ ↦ ρ.IicSnd r s) atTop (𝓝 (ρ.fst s))

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r => (ρ.IicSnd ↑r) s) atTop (𝓝 (ρ.fst s))

Tactic:
simp_rw [ρ.IicSnd_apply _ hs, fst_apply hs, ← prod_univ]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atTop (𝓝 (ρ (s ×ˢ univ)))

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atTop (𝓝 (ρ (s ×ˢ univ)))

Tactic:
rw [← Real.iUnion_Iic_rat, prod_iUnion]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atTop (𝓝 (ρ (⋃ i, s ×ˢ Iic ↑i)))

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun r => ρ (s ×ˢ Iic ↑r)) atTop (𝓝 (ρ (⋃ i, s ×ˢ Iic ↑i)))

Tactic:
apply tendsto_measure_iUnion_atTop

Result:
case hm
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Monotone fun r => s ×ˢ Iic ↑r

Proof state:
case hm
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Monotone fun r => s ×ˢ Iic ↑r

Tactic:
exact monotone_const.set_prod Rat.cast_mono.Iic

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
lemma rightShift_v (a n' : ℤ) (hn' : n' + a = n) (p q : ℤ) (hpq : p + n' = q)
    (p' : ℤ) (hp' : p + n = p') :
    (γ.rightShift a n' hn').v p q hpq = γ.v p p' hp' ≫
      (L.shiftFunctorObjXIso a q p' (by rw [← hp', ← hpq, ← hn', add_assoc])).inv

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p + n = p'
⊢ (γ.rightShift a n' hn').v p q hpq = γ.v p p' hp' ≫ (L.shiftFunctorObjXIso a q p' ⋯).inv

Tactic:
subst hp'

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
⊢ (γ.rightShift a n' hn').v p q hpq = γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + n) ⋯).inv

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
⊢ (mk fun p q hpq => γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + n) ⋯).inv).v p q hpq =
    γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + n) ⋯).inv

Tactic:
simp only [mk_v]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
⊢ (γ.rightShift a n' hn').v p q hpq = γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + n) ⋯).inv

Tactic:
dsimp only [rightShift]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
⊢ (mk fun p q hpq => γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + n) ⋯).inv).v p q hpq =
    γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + n) ⋯).inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p + n = p'
⊢ p' = q + a

Tactic:
rw [← hp', ← hpq, ← hn', add_assoc]

Result:
no goals
-- Mathlib/ModelTheory/Satisfiability.lean
theorem IsMaximal.mem_of_models (h : T.IsMaximal) {φ : L.Sentence} (hφ : T ⊨ᵇ φ) : φ ∈ T

Proof state:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : T ⊨ᵇ φ
con : Formula.not φ ∈ T
⊢ False

Tactic:
rw [models_iff_not_satisfiable, Set.union_singleton, Set.insert_eq_of_mem con] at hφ

Result:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : ¬T.IsSatisfiable
con : Formula.not φ ∈ T
⊢ False

Proof state:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ φ ∈ T

Tactic:
refine (h.mem_or_not_mem φ).resolve_right fun con => ?_

Result:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : T ⊨ᵇ φ
con : Formula.not φ ∈ T
⊢ False

Proof state:
L : Language
T : L.Theory
h : T.IsMaximal
φ : L.Sentence
hφ : ¬T.IsSatisfiable
con : Formula.not φ ∈ T
⊢ False

Tactic:
exact hφ h.1

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
lemma NNReal.le_add_nndist (a b : ℝ≥0) : a ≤ b + nndist a b

Proof state:
a b : ℝ≥0
this : ↑a ≤ ↑b + dist a b
⊢ a ≤ b + nndist a b

Tactic:
rwa [← NNReal.coe_le_coe, NNReal.coe_add, coe_nndist]

Result:
no goals

Proof state:
a b : ℝ≥0
⊢ a ≤ b + nndist a b

Tactic:
suffices (a : ℝ) ≤ (b : ℝ) + dist a b by
  rwa [← NNReal.coe_le_coe, NNReal.coe_add, coe_nndist]

Result:
a b : ℝ≥0
⊢ ↑a ≤ ↑b + dist a b

Proof state:
a b : ℝ≥0
⊢ ↑a - ↑b ≤ dist a b

Tactic:
exact le_of_abs_le (dist_eq a b).ge

Result:
no goals

Proof state:
a b : ℝ≥0
⊢ ↑a ≤ ↑b + dist a b

Tactic:
rw [← sub_le_iff_le_add']

Result:
a b : ℝ≥0
⊢ ↑a - ↑b ≤ dist a b
-- Mathlib/FieldTheory/Normal/Closure.lean
/-- `normalClosure F K L` is a valid normal closure if `K/F` is algebraic
  and all minimal polynomials of `K/F` splits in `L/F`. -/
lemma isNormalClosure_normalClosure : IsNormalClosure F K (normalClosure F K L)

Proof state:
case right
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
splits : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
f : K →ₐ[F] L
⊢ f.fieldRange ≤
    IntermediateField.map (⨆ f, f.fieldRange).val (f.codRestrict (⨆ f, f.fieldRange).toSubalgebra ⋯).fieldRange

Tactic:
rw [AlgHom.map_fieldRange, val, AlgHom.val_comp_codRestrict]

Result:
no goals