harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Group/Action.lean
theorem measurePreserving_smul : MeasurePreserving (c • ·) μ μ :=
  { measurable := measurable_const_smul c
    map_eq

Proof state:
case h
M : Type v
α : Type w
m : MeasurableSpace α
inst✝³ : MeasurableSpace M
inst✝² : SMul M α
inst✝¹ : MeasurableSMul M α
c : M
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
s : Set α
hs : MeasurableSet s
⊢ μ ((fun x => c • x) ⁻¹' s) = μ s

Tactic:
exact SMulInvariantMeasure.measure_preimage_smul c hs

Result:
no goals

Proof state:
M : Type v
α : Type w
m : MeasurableSpace α
inst✝³ : MeasurableSpace M
inst✝² : SMul M α
inst✝¹ : MeasurableSMul M α
c : M
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
⊢ Measure.map (fun x => c • x) μ = μ

Tactic:
ext1 s hs

Result:
case h
M : Type v
α : Type w
m : MeasurableSpace α
inst✝³ : MeasurableSpace M
inst✝² : SMul M α
inst✝¹ : MeasurableSMul M α
c : M
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
s : Set α
hs : MeasurableSet s
⊢ (Measure.map (fun x => c • x) μ) s = μ s

Proof state:
case h
M : Type v
α : Type w
m : MeasurableSpace α
inst✝³ : MeasurableSpace M
inst✝² : SMul M α
inst✝¹ : MeasurableSMul M α
c : M
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
s : Set α
hs : MeasurableSet s
⊢ (Measure.map (fun x => c • x) μ) s = μ s

Tactic:
rw [map_apply (measurable_const_smul c) hs]

Result:
case h
M : Type v
α : Type w
m : MeasurableSpace α
inst✝³ : MeasurableSpace M
inst✝² : SMul M α
inst✝¹ : MeasurableSMul M α
c : M
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
s : Set α
hs : MeasurableSet s
⊢ μ ((fun x => c • x) ⁻¹' s) = μ s
-- Mathlib/Data/Stream/Init.lean
theorem map_iterate (f : α → α) (a : α) : iterate f (f a) = map f (iterate f a)

Proof state:
case h.succ
α : Type u
f : α → α
a : α
n' : ℕ
ih : iterate f (f a) n' = map f (iterate f a) n'
⊢ f (iterate f (f a) n') = f (iterate f a (n' + 1))

Tactic:
rw [map, get] at ih

Result:
case h.succ
α : Type u
f : α → α
a : α
n' : ℕ
ih : iterate f (f a) n' = f (iterate f a n')
⊢ f (iterate f (f a) n') = f (iterate f a (n' + 1))

Proof state:
case h.succ
α : Type u
f : α → α
a : α
n' : ℕ
ih : iterate f (f a) n' = f (iterate f a n')
⊢ f (iterate f (f a) n') = f (iterate f a (n' + 1))

Tactic:
rw [iterate]

Result:
case h.succ
α : Type u
f : α → α
a : α
n' : ℕ
ih : iterate f (f a) n' = f (iterate f a n')
⊢ f (iterate f (f a) n') = f (f (iterate f a n'))

Proof state:
case h
α : Type u
f : α → α
a : α
n : ℕ
⊢ iterate f (f a) n = map f (iterate f a) n

Tactic:
induction' n with n' ih

Result:
case h.zero
α : Type u
f : α → α
a : α
⊢ iterate f (f a) 0 = map f (iterate f a) 0

case h.succ
α : Type u
f : α → α
a : α
n' : ℕ
ih : iterate f (f a) n' = map f (iterate f a) n'
⊢ iterate f (f a) (n' + 1) = map f (iterate f a) (n' + 1)

Proof state:
case h.succ
α : Type u
f : α → α
a : α
n' : ℕ
ih : iterate f (f a) n' = map f (iterate f a) n'
⊢ iterate f (f a) (n' + 1) = map f (iterate f a) (n' + 1)

Tactic:
unfold map iterate get

Result:
case h.succ
α : Type u
f : α → α
a : α
n' : ℕ
ih : iterate f (f a) n' = map f (iterate f a) n'
⊢ f (iterate f (f a) n') = f (iterate f a (n' + 1))

Proof state:
case h.zero
α : Type u
f : α → α
a : α
⊢ iterate f (f a) 0 = map f (iterate f a) 0

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
f : α → α
a : α
⊢ iterate f (f a) = map f (iterate f a)

Tactic:
funext n

Result:
case h
α : Type u
f : α → α
a : α
n : ℕ
⊢ iterate f (f a) n = map f (iterate f a) n

Proof state:
case h.succ
α : Type u
f : α → α
a : α
n' : ℕ
ih : iterate f (f a) n' = f (iterate f a n')
⊢ f (iterate f (f a) n') = f (f (iterate f a n'))

Tactic:
exact congrArg f ih

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem one_smul (x : M ⊗[R] N) : (1 : R') • x = x :=
  have : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ n := fun _ _ _ => rfl
  x.induction_on (by rw [TensorProduct.smul_zero])
    (fun m n => by rw [this, one_smul])
    fun x y ihx ihy => by rw [TensorProduct.smul_add, ihx, ihy]

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
R' : Type u_2
inst✝⁶ : Monoid R'
M : Type u_5
N : Type u_6
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : DistribMulAction R' M
inst✝ : SMulCommClass R R' M
x : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
m : M
n : N
⊢ 1 • m ⊗ₜ[R] n = m ⊗ₜ[R] n

Tactic:
rw [this, one_smul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
R' : Type u_2
inst✝⁶ : Monoid R'
M : Type u_5
N : Type u_6
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : DistribMulAction R' M
inst✝ : SMulCommClass R R' M
x : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
⊢ 1 • 0 = 0

Tactic:
rw [TensorProduct.smul_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
R' : Type u_2
inst✝⁶ : Monoid R'
M : Type u_5
N : Type u_6
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : DistribMulAction R' M
inst✝ : SMulCommClass R R' M
x✝ : M ⊗[R] N
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : 1 • x = x
ihy : 1 • y = y
⊢ 1 • (x + y) = x + y

Tactic:
rw [TensorProduct.smul_add, ihx, ihy]

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/Basic.lean
theorem liftr_iff {α : Type u} (r : α → α → Prop) (x y : P α) :
    Liftr r x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ i, r (f₀ i) (f₁ i)

Proof state:
case h.right.left
P : PFunctor.{u}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t => (↑t).1) <$> u = x
yeq : (fun t => (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ y = ⟨a, fun i => (↑(f i)).2⟩

Tactic:
rw [← yeq, h]

Result:
case h.right.left
P : PFunctor.{u}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t => (↑t).1) <$> u = x
yeq : (fun t => (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun t => (↑t).2) <$> ⟨a, f⟩ = ⟨a, fun i => (↑(f i)).2⟩

Proof state:
case mp.intro.intro
P : PFunctor.{u}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t => (↑t).1) <$> u = x
yeq : (fun t => (↑t).2) <$> u = y
⊢ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)

Tactic:
rcases h : u with ⟨a, f⟩

Result:
case mp.intro.intro.mk
P : PFunctor.{u}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t => (↑t).1) <$> u = x
yeq : (fun t => (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)

Proof state:
case h.left
P : PFunctor.{u}
α : Type u
r : α → α → Prop
x y : ↑P α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = ⟨a, f₀⟩
yeq : y = ⟨a, f₁⟩
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ (fun t => (↑t).1) <$> ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩ = ⟨a, f₀⟩

Tactic:
rfl

Result:
no goals

Proof state:
case h.left
P : PFunctor.{u}
α : Type u
r : α → α → Prop
x y : ↑P α
u : ↑P { p // r p.1 p.2 }
xeq : (fun t => (↑t).1) <$> u = x
yeq : (fun t => (↑t).2) <$> u = y
a : P.A
f : P.B a → { p // r p.1 p.2 }
h : u = ⟨a, f⟩
⊢ (fun t => (↑t).1) <$> ⟨a, f⟩ = ⟨a, fun i => (↑(f i)).1⟩

Tactic:
rfl

Result:
no goals

Proof state:
P : PFunctor.{u}
α : Type u
r : α → α → Prop
x y : ↑P α
⊢ Liftr r x y ↔ ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)

Tactic:
constructor

Result:
case mp
P : PFunctor.{u}
α : Type u
r : α → α → Prop
x y : ↑P α
⊢ Liftr r x y → ∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)

case mpr
P : PFunctor.{u}
α : Type u
r : α → α → Prop
x y : ↑P α
⊢ (∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)) → Liftr r x y

Proof state:
case mpr
P : PFunctor.{u}
α : Type u
r : α → α → Prop
x y : ↑P α
⊢ (∃ a f₀ f₁, x = ⟨a, f₀⟩ ∧ y = ⟨a, f₁⟩ ∧ ∀ (i : P.B a), r (f₀ i) (f₁ i)) → Liftr r x y

Tactic:
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩

Result:
case mpr.intro.intro.intro.intro.intro
P : PFunctor.{u}
α : Type u
r : α → α → Prop
x y : ↑P α
a : P.A
f₀ f₁ : P.B a → α
xeq : x = ⟨a, f₀⟩
yeq : y = ⟨a, f₁⟩
h : ∀ (i : P.B a), r (f₀ i) (f₁ i)
⊢ Liftr r x y
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem IsSpanning.card_verts [Fintype V] {G' : Subgraph G} [Fintype G'.verts] (h : G'.IsSpanning) :
    G'.verts.toFinset.card = Fintype.card V

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
G' : G.Subgraph
inst✝ : Fintype ↑G'.verts
h : G'.IsSpanning
⊢ Finset.univ.card = Fintype.card V

Tactic:
congr

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
G' : G.Subgraph
inst✝ : Fintype ↑G'.verts
h : G'.IsSpanning
⊢ G'.verts.toFinset.card = Fintype.card V

Tactic:
simp only [isSpanning_iff.1 h, Set.toFinset_univ]

Result:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
G' : G.Subgraph
inst✝ : Fintype ↑G'.verts
h : G'.IsSpanning
⊢ Finset.univ.card = Fintype.card V
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem isometry_real_vadd (a : ℝ) : Isometry (a +ᵥ · : ℍ → ℍ) :=
  Isometry.of_dist_eq fun y₁ y₂ => by simp only [dist_eq, coe_vadd, vadd_im, dist_add_left]

Proof state:
a : ℝ
y₁ y₂ : ℍ
⊢ dist (a +ᵥ y₁) (a +ᵥ y₂) = dist y₁ y₂

Tactic:
simp only [dist_eq, coe_vadd, vadd_im, dist_add_left]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem _root_.ContinuousLinearMap.intervalIntegral_comp_comm [CompleteSpace E] (L : E →L[𝕜] F)
    (hf : IntervalIntegrable f μ a b) : (∫ x in a..b, L (f x) ∂μ) = L (∫ x in a..b, f x ∂μ)

Proof state:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedSpace ℝ F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
L : E →L[𝕜] F
hf : IntervalIntegrable f μ a b
⊢ ∫ (x : ℝ) in a..b, L (f x) ∂μ = L (∫ (x : ℝ) in a..b, f x ∂μ)

Tactic:
simp_rw [intervalIntegral, L.integral_comp_comm hf.1, L.integral_comp_comm hf.2, L.map_sub]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Unitor.lean
@[simp, reassoc]
lemma mapBifunctorLeftUnitorCofan_inj (j : J) :
    (mapBifunctorLeftUnitorCofan F X e p hp Y j).inj ⟨⟨0, j⟩, hp j⟩ =
      (F.map (singleObjApplyIso (0 : I) X).hom).app (Y j) ≫ e.hom.app (Y j)

Proof state:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{u_6, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y : GradedObject J D
j : J
⊢ Cofan.inj (mapBifunctorLeftUnitorCofan F X e p hp Y j) ⟨(0, j), ⋯⟩ =
    (F.map (singleObjApplyIso 0 X).hom).app (Y j) ≫ e.hom.app (Y j)

Tactic:
simp [mapBifunctorLeftUnitorCofan]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Free.lean
theorem mk_freeCommRing : #(FreeCommRing α) = max #α ℵ₀

Proof state:
α : Type u
⊢ #(FreeCommRing α) = #α ⊔ ℵ₀

Tactic:
cases isEmpty_or_nonempty α <;> simp [FreeCommRing]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem zero_eq_one_iff {n : Nat} [NeZero n] : (0 : Fin n) = 1 ↔ n = 1

Proof state:
case mpr
n : Nat
inst✝ : NeZero n
⊢ n = 1 → 0 = 1

Tactic:
rintro rfl

Result:
case mpr
inst✝ : NeZero 1
⊢ 0 = 1

Proof state:
n : Nat
inst✝ : NeZero n
⊢ 0 = 1 ↔ n = 1

Tactic:
constructor

Result:
case mp
n : Nat
inst✝ : NeZero n
⊢ 0 = 1 → n = 1

case mpr
n : Nat
inst✝ : NeZero n
⊢ n = 1 → 0 = 1

Proof state:
case mp
n : Nat
inst✝ : NeZero n
h : 0 = ↑1
⊢ n = 1

Tactic:
change 0 % n = 1 % n at h

Result:
case mp
n : Nat
inst✝ : NeZero n
h : 0 % n = 1 % n
⊢ n = 1

Proof state:
case mp
n : Nat
inst✝ : NeZero n
h : 0 % n = 1 % n
⊢ n = 1

Tactic:
rw [eq_comm] at h

Result:
case mp
n : Nat
inst✝ : NeZero n
h : 1 % n = 0 % n
⊢ n = 1

Proof state:
case mp
n : Nat
inst✝ : NeZero n
⊢ 0 = 1 → n = 1

Tactic:
intro h

Result:
case mp
n : Nat
inst✝ : NeZero n
h : 0 = 1
⊢ n = 1

Proof state:
case mp
n : Nat
inst✝ : NeZero n
h : 1 % n = 0 % n
⊢ n = 1

Tactic:
simpa using h

Result:
no goals

Proof state:
case mpr
inst✝ : NeZero 1
⊢ 0 = 1

Tactic:
simp

Result:
no goals

Proof state:
case mp
n : Nat
inst✝ : NeZero n
h : 0 = 1
⊢ n = 1

Tactic:
simp [Fin.ext_iff] at h

Result:
case mp
n : Nat
inst✝ : NeZero n
h : 0 = ↑1
⊢ n = 1
-- Mathlib/Data/Nat/Find.lean
lemma findGreatest_mono_right (P : ℕ → Prop) [DecidablePred P] {m n} (hmn : m ≤ n) :
    Nat.findGreatest P m ≤ Nat.findGreatest P n

Proof state:
case step
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
⊢ findGreatest P m ≤ findGreatest P m✝.succ

Tactic:
rw [findGreatest_succ]

Result:
case step
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
⊢ findGreatest P m ≤ if P (m✝ + 1) then m✝ + 1 else findGreatest P m✝

Proof state:
case neg
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
h✝ : ¬P (m✝ + 1)
⊢ findGreatest P m ≤ findGreatest P m✝

Tactic:
exact ih

Result:
no goals

Proof state:
case step
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
⊢ findGreatest P m ≤ if P (m✝ + 1) then m✝ + 1 else findGreatest P m✝

Tactic:
split_ifs

Result:
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
h✝ : P (m✝ + 1)
⊢ findGreatest P m ≤ m✝ + 1

case neg
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
h✝ : ¬P (m✝ + 1)
⊢ findGreatest P m ≤ findGreatest P m✝

Proof state:
case refl
P : ℕ → Prop
inst✝ : DecidablePred P
m n : ℕ
⊢ findGreatest P m ≤ findGreatest P m

Tactic:
simp

Result:
no goals

Proof state:
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
h✝ : P (m✝ + 1)
⊢ findGreatest P m ≤ m✝ + 1

Tactic:
exact le_trans ih <| le_trans (findGreatest_le _) (le_succ _)

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem setFinite_inter [ProperSpace E] [Finite ι] {s : Set E} (hs : Bornology.IsBounded s) :
    Set.Finite (s ∩ span ℤ (Set.range b))

Proof state:
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝¹ : ProperSpace E
inst✝ : Finite ι
s : Set E
hs : IsBounded s
⊢ (s ∩ ↑(span ℤ (Set.range ⇑b))).Finite

Tactic:
have : DiscreteTopology (span ℤ (Set.range b)) := inferInstance

Result:
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝¹ : ProperSpace E
inst✝ : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology ↥(span ℤ (Set.range ⇑b))
⊢ (s ∩ ↑(span ℤ (Set.range ⇑b))).Finite

Proof state:
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝¹ : ProperSpace E
inst✝ : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology ↥(span ℤ (Set.range ⇑b))
⊢ IsClosed ↑(span ℤ (Set.range ⇑b)).toAddSubgroup

Tactic:
exact AddSubgroup.isClosed_of_discrete

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝¹ : ProperSpace E
inst✝ : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology ↥(span ℤ (Set.range ⇑b))
⊢ IsClosed ↑(span ℤ (Set.range ⇑b))

Tactic:
rw [← coe_toAddSubgroup]

Result:
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝¹ : ProperSpace E
inst✝ : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology ↥(span ℤ (Set.range ⇑b))
⊢ IsClosed ↑(span ℤ (Set.range ⇑b)).toAddSubgroup

Proof state:
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝¹ : ProperSpace E
inst✝ : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology ↥(span ℤ (Set.range ⇑b))
⊢ (s ∩ ↑(span ℤ (Set.range ⇑b))).Finite

Tactic:
refine Metric.finite_isBounded_inter_isClosed hs ?_

Result:
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝¹ : ProperSpace E
inst✝ : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology ↥(span ℤ (Set.range ⇑b))
⊢ IsClosed ↑(span ℤ (Set.range ⇑b))
-- Mathlib/Combinatorics/Schnirelmann.lean
lemma schnirelmannDensity_setOf_modeq_one {m : ℕ} :
    schnirelmannDensity {n | n ≡ 1 [MOD m]} = (m⁻¹ : ℝ)

Proof state:
case inr.h
m : ℕ
hm : m ≠ 1
⊢ {n | n ≡ 1 [MOD m]} = {n | n % m = 1}

Tactic:
ext n

Result:
case inr.h.h
m : ℕ
hm : m ≠ 1
n : ℕ
⊢ n ∈ {n | n ≡ 1 [MOD m]} ↔ n ∈ {n | n % m = 1}

Proof state:
case inl

⊢ schnirelmannDensity {n | n ≡ 1 [MOD 1]} = (↑1)⁻¹

Tactic:
simp [Nat.modEq_one]

Result:
no goals

Proof state:
case inr
m : ℕ
hm : m ≠ 1
⊢ schnirelmannDensity {n | n ≡ 1 [MOD m]} = schnirelmannDensity {n | n % m = 1}

Tactic:
apply schnirelmannDensity_congr

Result:
case inr.h
m : ℕ
hm : m ≠ 1
⊢ {n | n ≡ 1 [MOD m]} = {n | n % m = 1}

Proof state:
m : ℕ
⊢ schnirelmannDensity {n | n ≡ 1 [MOD m]} = (↑m)⁻¹

Tactic:
rcases eq_or_ne m 1 with rfl | hm

Result:
case inl

⊢ schnirelmannDensity {n | n ≡ 1 [MOD 1]} = (↑1)⁻¹

case inr
m : ℕ
hm : m ≠ 1
⊢ schnirelmannDensity {n | n ≡ 1 [MOD m]} = (↑m)⁻¹

Proof state:
case inr
m : ℕ
hm : m ≠ 1
⊢ schnirelmannDensity {n | n ≡ 1 [MOD m]} = (↑m)⁻¹

Tactic:
rw [← schnirelmannDensity_setOf_mod_eq_one hm]

Result:
case inr
m : ℕ
hm : m ≠ 1
⊢ schnirelmannDensity {n | n ≡ 1 [MOD m]} = schnirelmannDensity {n | n % m = 1}

Proof state:
case inr.h.h
m : ℕ
hm : m ≠ 1
n : ℕ
⊢ n ∈ {n | n ≡ 1 [MOD m]} ↔ n ∈ {n | n % m = 1}

Tactic:
simp only [Set.mem_setOf_eq, Nat.ModEq, Nat.one_mod_eq_one.mpr hm]

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedFDeriv_eq_equiv_comp : iteratedFDeriv 𝕜 n f =
    ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F ∘ iteratedDeriv n f

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedFDeriv 𝕜 n f = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDeriv n f

Tactic:
rw [iteratedDeriv_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm,
  Function.id_comp]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Basic.lean
theorem eventually_nhds_norm_smul_sub_lt (c : 𝕜) (x : E) {ε : ℝ} (h : 0 < ε) :
    ∀ᶠ y in 𝓝 x, ‖c • (y - x)‖ < ε :=
  have : Tendsto (fun y ↦ ‖c • (y - x)‖) (𝓝 x) (𝓝 0) :=
    Continuous.tendsto' (by fun_prop) _ _ (by simp)
  this.eventually (gt_mem_nhds h)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
ε : ℝ
h : 0 < ε
⊢ Continuous fun y => ‖c • (y - x)‖

Tactic:
fun_prop

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
ε : ℝ
h : 0 < ε
⊢ ‖c • (x - x)‖ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean
/-- `A` is a localization of a commutative semiring `R` with respect to `S` iff
the associated linear map `R →ₗ[R] A` is a localization of modules with respect to `S`. -/
lemma isLocalizedModule_iff_isLocalization' :
    IsLocalizedModule S (Algebra.linearMap R A) ↔ IsLocalization S A

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ IsLocalizedModule S (Algebra.linearMap R A) ↔ IsLocalization S A

Tactic:
convert isLocalizedModule_iff_isLocalization (S := S) (A := R) (Aₛ := A)

Result:
case h.e'_2.h.e'_3
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ S = Algebra.algebraMapSubmonoid R S

Proof state:
case h.e'_2.h.e'_3
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
⊢ S = Algebra.algebraMapSubmonoid R S

Tactic:
exact (Submonoid.map_id S).symm

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_union_Ioi (h : c ≤ max a b) : Ioc a b ∪ Ioi c = Ioi (min a c)

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
h : c ≤ b
⊢ Ioc a b ∪ Ioi c = Ioi (a ⊓ c)

Tactic:
exact Ioc_union_Ioi' h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : c ≤ a ⊔ b
⊢ Ioc a b ∪ Ioi c = Ioi (a ⊓ c)

Tactic:
rcases le_total a b with hab | hab <;> simp [hab] at h

Result:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
h : c ≤ b
⊢ Ioc a b ∪ Ioi c = Ioi (a ⊓ c)

case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b ≤ a
h : c ≤ a
⊢ Ioc a b ∪ Ioi c = Ioi (a ⊓ c)

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : b ≤ a
h : c ≤ a
⊢ Ioc a b ∪ Ioi c = Ioi (a ⊓ c)

Tactic:
simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insertMany_list_of_contains_eq_false [LawfulBEq α] (h : m.1.WF)
    {l : List ((a : α) × β a)} {k : α}
    (h' : (l.map Sigma.fst).contains k = false) :
    (m.insertMany l).1.get? k = m.get? k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k : α
h' : (List.map Sigma.fst l).contains k = false
⊢ (m.insertMany l).val.get? k = m.get? k

Tactic:
simp_to_model [insertMany] using List.getValueCast?_insertList_of_contains_eq_false

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Seminorm.lean
theorem seminorm_one_eq_one_iff_ne_zero (hp : p 1 ≤ 1) : p 1 = 1 ↔ p ≠ 0

Proof state:
case inl
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : p 1 = 0
⊢ p 1 = 1

Tactic:
exfalso

Result:
case inl
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : p 1 = 0
⊢ False

Proof state:
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
⊢ p 1 = 1 ↔ p ≠ 0

Tactic:
refine
  ⟨fun h => ne_zero_iff.mpr ⟨1, by rw [h]; exact one_ne_zero⟩,
    fun h => ?_⟩

Result:
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
⊢ p 1 = 1

Proof state:
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p 1 = 1
⊢ p 1 ≠ 0

Tactic:
rw [h]

Result:
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p 1 = 1
⊢ 1 ≠ 0

Proof state:
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p 1 = 1
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : p 1 = 0
x : R
⊢ p x ≤ 0

Tactic:
simpa only [hp0, mul_one, mul_zero] using map_mul_le_mul p x 1

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : p 1 = 0
⊢ False

Tactic:
refine h (ext fun x => (apply_nonneg _ _).antisymm' ?_)

Result:
case inl
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : p 1 = 0
x : R
⊢ p x ≤ 0

Proof state:
case inr
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : 0 < p 1
⊢ p 1 ≤ p 1 * p 1

Tactic:
simpa only [one_mul] using map_mul_le_mul p (1 : R) _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
⊢ p 1 = 1

Tactic:
obtain hp0 | hp0 := (apply_nonneg p (1 : R)).eq_or_gt

Result:
case inl
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : p 1 = 0
⊢ p 1 = 1

case inr
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : 0 < p 1
⊢ p 1 = 1

Proof state:
case inr
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : 0 < p 1
⊢ p 1 = 1

Tactic:
refine hp.antisymm ((le_mul_iff_one_le_left hp0).1 ?_)

Result:
case inr
R : Type u_1
inst✝ : Ring R
p : RingSeminorm R
hp : p 1 ≤ 1
h : p ≠ 0
hp0 : 0 < p 1
⊢ p 1 ≤ p 1 * p 1
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem omega0_lt_omega1 : ω < ω₁

Proof state:
⊢ 0 < 1

Tactic:
exact zero_lt_one

Result:
no goals

Proof state:
⊢ ω < ω_ 1

Tactic:
rw [← omega_zero, omega_lt_omega]

Result:
⊢ 0 < 1