harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem take_range (m n : Nat) : take m (range n) = range (min m n)

Proof state:
case hl
m n : Nat
⊢ (take m (range n)).length = (range (min m n)).length

Tactic:
simp

Result:
no goals

Proof state:
m n : Nat
⊢ take m (range n) = range (min m n)

Tactic:
apply List.ext_getElem

Result:
case hl
m n : Nat
⊢ (take m (range n)).length = (range (min m n)).length

case h
m n : Nat
⊢ ∀ (i : Nat) (h₁ : i < (take m (range n)).length) (h₂ : i < (range (min m n)).length),
    (take m (range n))[i] = (range (min m n))[i]

Proof state:
case h
m n : Nat
⊢ ∀ (i : Nat) (h₁ : i < (take m (range n)).length) (h₂ : i < (range (min m n)).length),
    (take m (range n))[i] = (range (min m n))[i]

Tactic:
simp +contextual [getElem_take, Nat.lt_min]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Star.lean
theorem star_ι (m : M) : star (ι Q m) = -ι 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
⊢ star ((ι Q) m) = -(ι Q) m

Tactic:
rw [star_def, involute_ι, map_neg, reverse_ι]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivWithinAt.mul_const (hc : HasFDerivWithinAt c c' s x) (d : 𝔸') :
    HasFDerivWithinAt (fun y => c y * d) (d • c') s x

Proof state:
case h.e'_12.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ d • c' = c'.smulRight d

Tactic:
ext z

Result:
case h.e'_12.h.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
z : E
⊢ (d • c') z = (c'.smulRight d) z

Proof state:
case h.e'_12.h.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
z : E
⊢ (d • c') z = (c'.smulRight d) z

Tactic:
apply mul_comm

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
⊢ HasFDerivWithinAt (fun y => c y * d) (d • c') s x

Tactic:
convert hc.mul_const' d

Result:
case h.e'_12.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ d • c' = c'.smulRight d
-- Mathlib/RingTheory/LocalRing/LocalSubring.lean
lemma toSubring_injective : Function.Injective (toSubring (R := R))

Proof state:
case mk.mk
R : Type u_1
inst✝ : CommRing R
a : Subring R
isLocalRing✝¹ : IsLocalRing ↥a
isLocalRing✝ : IsLocalRing ↥(mk a).toSubring
⊢ mk a = mk (mk a).toSubring

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ Function.Injective toSubring

Tactic:
rintro ⟨a, b⟩ ⟨c, d⟩ rfl

Result:
case mk.mk
R : Type u_1
inst✝ : CommRing R
a : Subring R
isLocalRing✝¹ : IsLocalRing ↥a
isLocalRing✝ : IsLocalRing ↥(mk a).toSubring
⊢ mk a = mk (mk a).toSubring
-- Mathlib/Probability/Martingale/Basic.lean
theorem Martingale.eq_zero_of_predictable [SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E}
    (hfmgle : Martingale f 𝒢 μ) (hfadp : Adapted 𝒢 fun n => f (n + 1)) (n : ℕ) : f n =ᵐ[μ] f 0

Proof state:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
n : ℕ
⊢ f n =ᶠ[ae μ] f 0

Tactic:
induction' n with k ih

Result:
case zero
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
⊢ f 0 =ᶠ[ae μ] f 0

case succ
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
k : ℕ
ih : f k =ᶠ[ae μ] f 0
⊢ f (k + 1) =ᶠ[ae μ] f 0

Proof state:
case zero
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
⊢ f 0 =ᶠ[ae μ] f 0

Tactic:
rfl

Result:
no goals

Proof state:
case succ
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
k : ℕ
ih : f k =ᶠ[ae μ] f 0
⊢ f (k + 1) =ᶠ[ae μ] f 0

Tactic:
exact ((Germ.coe_eq.mp (congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _) (hfadp _)
  (hfmgle.integrable _))).symm.trans (hfmgle.2 k (k + 1) k.le_succ)).trans ih

Result:
no goals
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem edist_le_of_fixedPoint (hf : ContractingWith K f) {x y} (h : edist x y ≠ ∞)
    (hy : IsFixedPt f y) : edist x y ≤ edist x (f x) / (1 - K)

Proof state:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ⊤
hy : IsFixedPt f y
⊢ edist x y ≤ edist x (f x) / (1 - ↑K)

Tactic:
simpa only [hy.eq, edist_self, add_zero] using hf.edist_inequality h

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `div_le_iff₀` for a version with multiplication on the other side. -/
lemma div_le_iff₀' (hc : 0 < c) : b / c ≤ a ↔ b ≤ c * a

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hc : 0 < c
this : MulPosMono G₀
⊢ b / c ≤ a ↔ b ≤ c * a

Tactic:
rw [div_le_iff₀ hc, mul_comm]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hc : 0 < c
⊢ b / c ≤ a ↔ b ≤ c * a

Tactic:
have := posMulMono_iff_mulPosMono.1 ‹_›

Result:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hc : 0 < c
this : MulPosMono G₀
⊢ b / c ≤ a ↔ b ≤ c * a
-- Mathlib/RingTheory/Valuation/ValExtension.lean
theorem ofComapInteger (h : vA.integer.comap (algebraMap K A) = vK.integer) :
    IsValExtension vK vA where
  val_isEquiv_comap

Proof state:
A : Type u_2
inst✝⁴ : Ring A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝¹ : LinearOrderedCommGroupWithZero ΓK
inst✝ : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
x : K
⊢ vK x ≤ 1 ↔ (comap (algebraMap K A) vA) x ≤ 1

Tactic:
simp_rw [← Valuation.mem_integer_iff, ← h, Subring.mem_comap, mem_integer_iff, comap_apply]

Result:
no goals

Proof state:
A : Type u_2
inst✝⁴ : Ring A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝¹ : LinearOrderedCommGroupWithZero ΓK
inst✝ : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
⊢ ∀ {x : K}, vK x ≤ 1 ↔ (comap (algebraMap K A) vA) x ≤ 1

Tactic:
intro x

Result:
A : Type u_2
inst✝⁴ : Ring A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝¹ : LinearOrderedCommGroupWithZero ΓK
inst✝ : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
x : K
⊢ vK x ≤ 1 ↔ (comap (algebraMap K A) vA) x ≤ 1

Proof state:
A : Type u_2
inst✝⁴ : Ring A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝¹ : LinearOrderedCommGroupWithZero ΓK
inst✝ : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
⊢ vK.IsEquiv (comap (algebraMap K A) vA)

Tactic:
rw [isEquiv_iff_val_le_one]

Result:
A : Type u_2
inst✝⁴ : Ring A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra K A
ΓA : Type u_7
ΓK : Type u_8
inst✝¹ : LinearOrderedCommGroupWithZero ΓK
inst✝ : LinearOrderedCommGroupWithZero ΓA
vK : Valuation K ΓK
vA : Valuation A ΓA
h : Subring.comap (algebraMap K A) vA.integer = vK.integer
⊢ ∀ {x : K}, vK x ≤ 1 ↔ (comap (algebraMap K A) vA) x ≤ 1
-- Mathlib/Algebra/Lie/Weights/Basic.lean
@[simp]
lemma iSup_genWeightSpaceOf_eq_top [IsTriangularizable R L M] (x : L) :
    ⨆ (φ : R), genWeightSpaceOf M φ x = ⊤

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsTriangularizable R L M
x : L
⊢ ⨆ i, ((toEnd R L M) x).maxGenEigenspace i = ⊤

Tactic:
exact IsTriangularizable.maxGenEigenspace_eq_top x

Result:
no goals

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsTriangularizable R L M
x : L
⊢ ⨆ φ, genWeightSpaceOf M φ x = ⊤

Tactic:
rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.iSup_toSubmodule,
  LieSubmodule.top_toSubmodule]

Result:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsTriangularizable R L M
x : L
⊢ ⨆ i, ↑(genWeightSpaceOf M i x) = ⊤

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsTriangularizable R L M
x : L
⊢ ⨆ i, ↑(genWeightSpaceOf M i x) = ⊤

Tactic:
dsimp [genWeightSpaceOf]

Result:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : IsTriangularizable R L M
x : L
⊢ ⨆ i, ((toEnd R L M) x).maxGenEigenspace i = ⊤
-- Mathlib/Data/List/Iterate.lean
theorem iterate_eq_nil {f : α → α} {a : α} {n : ℕ} : iterate f a n = [] ↔ n = 0

Proof state:
α : Type u_1
f : α → α
a : α
n : ℕ
⊢ iterate f a n = [] ↔ n = 0

Tactic:
rw [← length_eq_zero, length_iterate]

Result:
no goals
-- Mathlib/Data/Nat/Lattice.lean
theorem sInf_eq_zero {s : Set ℕ} : sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

Proof state:
s : Set ℕ
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

Tactic:
cases eq_empty_or_nonempty s with
| inl h => subst h
           simp only [or_true, eq_self_iff_true, iInf, InfSet.sInf,
                      mem_empty_iff_false, exists_false, dif_neg, not_false_iff]
| inr h => simp only [h.ne_empty, or_false, Nat.sInf_def, h, Nat.find_eq_zero]

Result:
no goals

Proof state:
case inr
s : Set ℕ
h : s.Nonempty
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

Tactic:
simp only [h.ne_empty, or_false, Nat.sInf_def, h, Nat.find_eq_zero]

Result:
no goals

Proof state:
case inl

⊢ sInf ∅ = 0 ↔ 0 ∈ ∅ ∨ ∅ = ∅

Tactic:
simp only [or_true, eq_self_iff_true, iInf, InfSet.sInf,
           mem_empty_iff_false, exists_false, dif_neg, not_false_iff]

Result:
no goals

Proof state:
case inl
s : Set ℕ
h : s = ∅
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

Tactic:
subst h

Result:
case inl

⊢ sInf ∅ = 0 ↔ 0 ∈ ∅ ∨ ∅ = ∅
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem map_add_swap [DecidableEq ι] {i j : ι} (hij : i ≠ j) :
    f v + f (v ∘ Equiv.swap i j) = 0

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ f (v ∘ ⇑(Equiv.swap i j)) + f v = 0

Tactic:
exact f.map_swap_add v hij

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ f v + f (v ∘ ⇑(Equiv.swap i j)) = 0

Tactic:
rw [add_comm]

Result:
R : Type u_1
inst✝⁵ : Semiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ f (v ∘ ⇑(Equiv.swap i j)) + f v = 0
-- Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
theorem nonneg_prod_iff [Preorder P] [AddLeftMono P]
    {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} :
    (∀ x, 0 ≤ (Q₁.prod Q₂) x) ↔ (∀ x, 0 ≤ Q₁ x) ∧ ∀ x, 0 ≤ Q₂ x

Proof state:
case mp.left
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : Preorder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
h : ∀ (a : M₁) (b : M₂), 0 ≤ Q₁ a + Q₂ b
x : M₁
⊢ 0 ≤ Q₁ x

Tactic:
simpa only [add_zero, map_zero] using h x 0

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem sub_one_sub_lt (h : i < n) : n - 1 - i < n

Proof state:
i n : Nat
h : i < n
⊢ n - 1 - i < n

Tactic:
rw [Nat.sub_right_comm]

Result:
i n : Nat
h : i < n
⊢ n - i - 1 < n

Proof state:
i n : Nat
h : i < n
⊢ n - i - 1 < n

Tactic:
exact Nat.sub_one_lt_of_le (Nat.sub_pos_of_lt h) (Nat.sub_le ..)

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem ite {f₁ f₂ : ℕ → ℕ} (hf₁ : Computable f₁) (hf₂ : Computable f₂)
    {c : ℕ → Prop} [DecidablePred c] (hc : ComputablePred c) :
    Computable fun k ↦ if c k then f₁ k else f₂ k

Proof state:
case intro
f₁ f₂ : ℕ → ℕ
hf₁ : Computable f₁
hf₂ : Computable f₂
c : ℕ → Prop
inst✝ inst : DecidablePred c
hc : Computable fun a => decide (c a)
⊢ Computable fun k => bif decide (c k) then f₁ k else f₂ k

Tactic:
convert hc.cond hf₁ hf₂

Result:
no goals

Proof state:
f₁ f₂ : ℕ → ℕ
hf₁ : Computable f₁
hf₂ : Computable f₂
c : ℕ → Prop
inst✝ : DecidablePred c
hc : ComputablePred c
⊢ Computable fun k => bif decide (c k) then f₁ k else f₂ k

Tactic:
obtain ⟨inst, hc⟩ := hc

Result:
case intro
f₁ f₂ : ℕ → ℕ
hf₁ : Computable f₁
hf₂ : Computable f₂
c : ℕ → Prop
inst✝ inst : DecidablePred c
hc : Computable fun a => decide (c a)
⊢ Computable fun k => bif decide (c k) then f₁ k else f₂ k

Proof state:
f₁ f₂ : ℕ → ℕ
hf₁ : Computable f₁
hf₂ : Computable f₂
c : ℕ → Prop
inst✝ : DecidablePred c
hc : ComputablePred c
⊢ Computable fun k => if c k then f₁ k else f₂ k

Tactic:
simp_rw [← Bool.cond_decide]

Result:
f₁ f₂ : ℕ → ℕ
hf₁ : Computable f₁
hf₂ : Computable f₂
c : ℕ → Prop
inst✝ : DecidablePred c
hc : ComputablePred c
⊢ Computable fun k => bif decide (c k) then f₁ k else f₂ k
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem smul_comap_le_comap_smul (f : M →ₗ[R] M') (S : Submodule R M') (I : Ideal R) :
    I • S.comap f ≤ (I • S).comap f

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : f x ∈ S
⊢ f (r • x) ∈ I • S

Tactic:
rw [f.map_smul]

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : f x ∈ S
⊢ r • f x ∈ I • S

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : f x ∈ S
⊢ r • f x ∈ I • S

Tactic:
exact Submodule.smul_mem_smul hr hx

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
⊢ I • comap f S ≤ comap f (I • S)

Tactic:
refine Submodule.smul_le.mpr fun r hr x hx => ?_

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : x ∈ comap f S
⊢ r • x ∈ comap f (I • S)

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : x ∈ comap f S
⊢ r • x ∈ comap f (I • S)

Tactic:
rw [Submodule.mem_comap] at hx ⊢

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
r : R
hr : r ∈ I
x : M
hx : f x ∈ S
⊢ f (r • x) ∈ I • S
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem eventually_nonempty_inter_smul_of_density_one (s : Set E) (x : E)
    (h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)) (t : Set E)
    (ht : MeasurableSet t) (h't : μ t ≠ 0) :
    ∀ᶠ r in 𝓝[>] (0 : ℝ), (s ∩ ({x} + r • t)).Nonempty

Proof state:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ⊤
⊢ ∀ (a : ℝ), 0 < μ (s ∩ ({x} + a • t')) / μ ({x} + a • t') → (s ∩ ({x} + a • t)).Nonempty

Tactic:
intro r hr

Result:
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
t' : Set E
t'_meas : MeasurableSet t'
t't : t' ⊆ t
t'pos : 0 < μ t'
t'top : μ t' < ⊤
r : ℝ
hr : 0 < μ (s ∩ ({x} + r • t')) / μ ({x} + r • t')
⊢ (s ∩ ({x} + r • t)).Nonempty
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : List α) : map f l = l

Proof state:
α : Type u_1
f : α → α
h : ∀ (x : α), f x = x
l : List α
⊢ map f l = l

Tactic:
simp [show f = id from funext h]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lTensor_pow (f : N →ₗ[R] N) (n : ℕ) : f.lTensor M ^ n = (f ^ n).lTensor M

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : N →ₗ[R] N
n : ℕ
⊢ lTensor M f ^ n = lTensor M (f ^ n)

Tactic:
have h := TensorProduct.map_pow (id : M →ₗ[R] M) f n

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : N →ₗ[R] N
n : ℕ
h : map id f ^ n = map (id ^ n) (f ^ n)
⊢ lTensor M f ^ n = lTensor M (f ^ n)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : N →ₗ[R] N
n : ℕ
h : map id f ^ n = map (id ^ n) (f ^ n)
⊢ lTensor M f ^ n = lTensor M (f ^ n)

Tactic:
rwa [id_pow] at h

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem isPreconnected_sUnion (x : α) (c : Set (Set α)) (H1 : ∀ s ∈ c, x ∈ s)
    (H2 : ∀ s ∈ c, IsPreconnected s) : IsPreconnected (⋃₀ c)

Proof state:
case intro.intro
α : Type u
inst✝ : TopologicalSpace α
x : α
c : Set (Set α)
H1 : ∀ s ∈ c, x ∈ s
H2 : ∀ s ∈ c, IsPreconnected s
y : α
s : Set α
sc : s ∈ c
ys : y ∈ s
⊢ ∃ t ⊆ ⋃₀ c, x ∈ t ∧ y ∈ t ∧ IsPreconnected t

Tactic:
exact ⟨s, subset_sUnion_of_mem sc, H1 s sc, ys, H2 s sc⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
c : Set (Set α)
H1 : ∀ s ∈ c, x ∈ s
H2 : ∀ s ∈ c, IsPreconnected s
⊢ ∀ y ∈ ⋃₀ c, ∃ t ⊆ ⋃₀ c, x ∈ t ∧ y ∈ t ∧ IsPreconnected t

Tactic:
rintro y ⟨s, sc, ys⟩

Result:
case intro.intro
α : Type u
inst✝ : TopologicalSpace α
x : α
c : Set (Set α)
H1 : ∀ s ∈ c, x ∈ s
H2 : ∀ s ∈ c, IsPreconnected s
y : α
s : Set α
sc : s ∈ c
ys : y ∈ s
⊢ ∃ t ⊆ ⋃₀ c, x ∈ t ∧ y ∈ t ∧ IsPreconnected t

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
c : Set (Set α)
H1 : ∀ s ∈ c, x ∈ s
H2 : ∀ s ∈ c, IsPreconnected s
⊢ IsPreconnected (⋃₀ c)

Tactic:
apply isPreconnected_of_forall x

Result:
α : Type u
inst✝ : TopologicalSpace α
x : α
c : Set (Set α)
H1 : ∀ s ∈ c, x ∈ s
H2 : ∀ s ∈ c, IsPreconnected s
⊢ ∀ y ∈ ⋃₀ c, ∃ t ⊆ ⋃₀ c, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem setOf_isUnit_inter_mul_comm (a b : A) :
    {r | IsUnit r} ∩ σ (a * b) = {r | IsUnit r} ∩ σ (b * a)

Proof state:
case h
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : R
⊢ r ∈ {r | IsUnit r} ∩ σ (a * b) ↔ r ∈ {r | IsUnit r} ∩ σ (b * a)

Tactic:
simpa using fun hr : IsUnit r ↦ unit_mem_mul_comm (r := hr.unit)

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
⊢ {r | IsUnit r} ∩ σ (a * b) = {r | IsUnit r} ∩ σ (b * a)

Tactic:
ext r

Result:
case h
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a b : A
r : R
⊢ r ∈ {r | IsUnit r} ∩ σ (a * b) ↔ r ∈ {r | IsUnit r} ∩ σ (b * a)
-- Mathlib/Data/Set/Image.lean
theorem exists_subtype_range_iff {p : range f → Prop} :
    (∃ a : range f, p a) ↔ ∃ i, p ⟨f i, mem_range_self _⟩ :=
  ⟨fun ⟨⟨a, i, hi⟩, ha⟩ => by
    subst a
    exact ⟨i, ha⟩,
   fun ⟨_, hi⟩ => ⟨_, hi⟩⟩

Proof state:
α : Type u_1
ι : Sort u_4
f : ι → α
p : ↑(range f) → Prop
x✝ : ∃ a, p a
a : α
i : ι
hi : f i = a
ha : p ⟨a, ⋯⟩
⊢ ∃ i, p ⟨f i, ⋯⟩

Tactic:
subst a

Result:
α : Type u_1
ι : Sort u_4
f : ι → α
p : ↑(range f) → Prop
x✝ : ∃ a, p a
i : ι
ha : p ⟨f i, ⋯⟩
⊢ ∃ i, p ⟨f i, ⋯⟩

Proof state:
α : Type u_1
ι : Sort u_4
f : ι → α
p : ↑(range f) → Prop
x✝ : ∃ a, p a
i : ι
ha : p ⟨f i, ⋯⟩
⊢ ∃ i, p ⟨f i, ⋯⟩

Tactic:
exact ⟨i, ha⟩

Result:
no goals