harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem mem_of_span_eq_top_of_smul_pow_mem (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤)
    (x : M) (H : ∀ r : s, ∃ n : ℕ, ((r : R) ^ n : R) • x ∈ M') : x ∈ M'

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ M'
⊢ x ∈ M'

Tactic:
choose f hf using H

Result:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
f : ↑s → ℕ
hf : ∀ (r : ↑s), ↑r ^ f r • x ∈ M'
⊢ x ∈ M'

Proof state:
case H
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
f : ↑s → ℕ
hf : ∀ (r : ↑s), ↑r ^ f r • x ∈ M'
⊢ ∀ (r : ↑(Set.range fun x => ↑x ^ f x)), ↑r • x ∈ M'

Tactic:
rintro ⟨_, r, hr, rfl⟩

Result:
case H.mk.intro.refl
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
f : ↑s → ℕ
hf : ∀ (r : ↑s), ↑r ^ f r • x ∈ M'
r : ↑s
⊢ ↑⟨(fun x => ↑x ^ f x) r, ⋯⟩ • x ∈ M'

Proof state:
case H.mk.intro.refl
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
f : ↑s → ℕ
hf : ∀ (r : ↑s), ↑r ^ f r • x ∈ M'
r : ↑s
⊢ ↑⟨(fun x => ↑x ^ f x) r, ⋯⟩ • x ∈ M'

Tactic:
exact hf r

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
f : ↑s → ℕ
hf : ∀ (r : ↑s), ↑r ^ f r • x ∈ M'
⊢ x ∈ M'

Tactic:
apply M'.mem_of_span_top_of_smul_mem _ (Ideal.span_range_pow_eq_top s hs f)

Result:
case H
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
f : ↑s → ℕ
hf : ∀ (r : ↑s), ↑r ^ f r • x ∈ M'
⊢ ∀ (r : ↑(Set.range fun x => ↑x ^ f x)), ↑r • x ∈ M'
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma isIso_homologyπ (hf : S.f = 0) [S.HasHomology] :
    IsIso S.homologyπ

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
inst✝ : S.HasHomology
this : IsIso S.leftHomologyπ
⊢ IsIso (S.leftHomologyπ ≫ S.leftHomologyIso.hom)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
inst✝ : S.HasHomology
⊢ IsIso S.homologyπ

Tactic:
have := S.isIso_leftHomologyπ hf

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
inst✝ : S.HasHomology
this : IsIso S.leftHomologyπ
⊢ IsIso S.homologyπ

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
inst✝ : S.HasHomology
this : IsIso S.leftHomologyπ
⊢ IsIso S.homologyπ

Tactic:
dsimp only [homologyπ]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
inst✝ : S.HasHomology
this : IsIso S.leftHomologyπ
⊢ IsIso (S.leftHomologyπ ≫ S.leftHomologyIso.hom)
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Ordered.find?_some [@TransCmp α cmp] [IsStrictCut cmp cut] (ht : Ordered cmp t) :
    t.find? cut = some x ↔ x ∈ t ∧ cut x = .eq

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
x✝ : x ∈ t ∧ cut x = Ordering.eq
hx : x ∈ t
e : cut x = Ordering.eq
y : α
hy : find? cut t = some y
⊢ find? cut t = some x

Tactic:
exact ht.unique hx (find?_some_mem hy) ((IsStrictCut.exact e).trans (find?_some_eq_eq hy)) ▸ hy

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
⊢ find? cut t = some x ↔ x ∈ t ∧ cut x = Ordering.eq

Tactic:
refine ⟨fun h => ⟨find?_some_mem h, find?_some_eq_eq h⟩, fun ⟨hx, e⟩ => ?_⟩

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
x✝ : x ∈ t ∧ cut x = Ordering.eq
hx : x ∈ t
e : cut x = Ordering.eq
⊢ find? cut t = some x

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
x✝ : x ∈ t ∧ cut x = Ordering.eq
hx : x ∈ t
e : cut x = Ordering.eq
⊢ find? cut t = some x

Tactic:
have ⟨y, hy⟩ := ht.memP_iff_find?.1 (memP_def.2 ⟨_, hx, e⟩)

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
x✝ : x ∈ t ∧ cut x = Ordering.eq
hx : x ∈ t
e : cut x = Ordering.eq
y : α
hy : find? cut t = some y
⊢ find? cut t = some x
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma Nontrivial.mul_left : t.Nontrivial → s.Nonempty → (s * t).Nontrivial

Proof state:
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ ↑t
b : α
hb : b ∈ ↑t
hab : a ≠ b
c : α
hc : c ∈ s
⊢ c * a ≠ c * b

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s t : Finset α
⊢ t.Nontrivial → s.Nonempty → (s * t).Nontrivial

Tactic:
rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ ↑t
b : α
hb : b ∈ ↑t
hab : a ≠ b
c : α
hc : c ∈ s
⊢ (s * t).Nontrivial

Proof state:
case intro.intro.intro.intro.intro
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsLeftCancelMul α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ ↑t
b : α
hb : b ∈ ↑t
hab : a ≠ b
c : α
hc : c ∈ s
⊢ (s * t).Nontrivial

Tactic:
exact ⟨c * a, mul_mem_mul hc ha, c * b, mul_mem_mul hc hb, by simpa⟩

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem pow_succ_padicValNat_not_dvd {n : ℕ} [hp : Fact p.Prime] (hn : n ≠ 0) :
    ¬p ^ (padicValNat p n + 1) ∣ n

Proof state:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ ¬p ^ (padicValNat p n + 1) ∣ n

Tactic:
rw [padicValNat_dvd_iff_le hn, not_le]

Result:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ padicValNat p n < padicValNat p n + 1

Proof state:
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ padicValNat p n < padicValNat p n + 1

Tactic:
exact Nat.lt_succ_self _

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem integralSum_biUnion_partition (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F)
    (π : TaggedPrepartition I) (πi : ∀ J, Prepartition J) (hπi : ∀ J ∈ π, (πi J).IsPartition) :
    integralSum f vol (π.biUnionPrepartition πi) = integralSum f vol π

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ J ∈ π, (πi J).IsPartition
⊢ integralSum f vol (π.biUnionPrepartition πi) = integralSum f vol π

Tactic:
refine (π.sum_biUnion_boxes _ _).trans (sum_congr rfl fun J hJ => ?_)

Result:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ J ∈ π, (πi J).IsPartition
J : Box ι
hJ : J ∈ π.boxes
⊢ ∑ J' ∈ (πi J).boxes, (vol J') (f ((π.biUnionPrepartition πi).tag J')) = (vol J) (f (π.tag J))

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ J ∈ π, (πi J).IsPartition
J : Box ι
hJ : J ∈ π.boxes
J' : Box ι
hJ' : J' ∈ (πi J).boxes
⊢ (vol J') (f (π.tag (π.biUnionIndex πi J'))) = (vol J') (f (π.tag J))

Tactic:
rw [Prepartition.biUnionIndex_of_mem _ hJ hJ']

Result:
no goals

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
πi : (J : Box ι) → Prepartition J
hπi : ∀ J ∈ π, (πi J).IsPartition
J : Box ι
hJ : J ∈ π.boxes
⊢ ∑ J' ∈ (πi J).boxes, (vol J') (f ((π.biUnionPrepartition πi).tag J')) = (vol J) (f (π.tag J))

Tactic:
calc
  (∑ J' ∈ (πi J).boxes, vol J' (f (π.tag <| π.toPrepartition.biUnionIndex πi J'))) =
      ∑ J' ∈ (πi J).boxes, vol J' (f (π.tag J)) :=
    sum_congr rfl fun J' hJ' => by rw [Prepartition.biUnionIndex_of_mem _ hJ hJ']
  _ = vol J (f (π.tag J)) :=
    (vol.map ⟨⟨fun g : E →L[ℝ] F => g (f (π.tag J)), rfl⟩, fun _ _ => rfl⟩).sum_partition_boxes
      le_top (hπi J hJ)

Result:
no goals
-- Mathlib/Analysis/Normed/Group/HomCompletion.lean
theorem NormedAddGroupHom.completion_comp (f : NormedAddGroupHom G H) (g : NormedAddGroupHom H K) :
    g.completion.comp f.completion = (g.comp f).completion

Proof state:
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
⊢ (g.completion.comp f.completion) x = (g.comp f).completion x

Tactic:
rw [NormedAddGroupHom.coe_comp, NormedAddGroupHom.completion_def,
  NormedAddGroupHom.completion_coe_to_fun, NormedAddGroupHom.completion_coe_to_fun,
  Completion.map_comp g.uniformContinuous f.uniformContinuous]

Result:
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
⊢ Completion.map (⇑g ∘ ⇑f) x = Completion.map (⇑(g.comp f)) x

Proof state:
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
⊢ g.completion.comp f.completion = (g.comp f).completion

Tactic:
ext x

Result:
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
⊢ (g.completion.comp f.completion) x = (g.comp f).completion x

Proof state:
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
⊢ Completion.map (⇑g ∘ ⇑f) x = Completion.map (⇑(g.comp f)) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem measure_ge_le_exp_cgf [IsFiniteMeasure μ] (ε : ℝ) (ht : 0 ≤ t)
    (h_int : Integrable (fun ω => exp (t * X ω)) μ) :
    (μ {ω | ε ≤ X ω}).toReal ≤ exp (-t * ε + cgf X μ t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)

Tactic:
rw [exp_add]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε) * rexp (cgf X μ t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ (μ {ω | ε ≤ X ω}).toReal ≤ rexp (-t * ε + cgf X μ t)

Tactic:
refine (measure_ge_le_exp_mul_mgf ε ht h_int).trans ?_

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε) * rexp (cgf X μ t)

Tactic:
exact mul_le_mul le_rfl (le_exp_log _) mgf_nonneg (exp_pos _).le

Result:
no goals
-- Mathlib/Data/ENat/Basic.lean
@[simp] lemma add_one_eq_coe_top_iff {n : WithTop ℕ∞} : n + 1 = (⊤ : ℕ∞) ↔ n = (⊤ : ℕ∞)

Proof state:
n : WithTop ℕ∞
⊢ n + 1 = ↑⊤ ↔ n = ↑⊤

Tactic:
match n with
| ⊤ => exact Iff.rfl
| (⊤ : ℕ∞) => simp
| (n : ℕ) =>
  norm_cast
  simp only [coe_ne_top, iff_false, ne_eq]

Result:
no goals

Proof state:
n✝ : WithTop ℕ∞
n : ℕ
⊢ ↑(n + 1) = ⊤ ↔ ↑n = ⊤

Tactic:
simp only [coe_ne_top, iff_false, ne_eq]

Result:
no goals

Proof state:
n : WithTop ℕ∞
⊢ ↑⊤ + 1 = ↑⊤ ↔ ↑⊤ = ↑⊤

Tactic:
simp

Result:
no goals

Proof state:
n✝ : WithTop ℕ∞
n : ℕ
⊢ ↑n + 1 = ↑⊤ ↔ ↑n = ↑⊤

Tactic:
norm_cast

Result:
n✝ : WithTop ℕ∞
n : ℕ
⊢ ↑(n + 1) = ⊤ ↔ ↑n = ⊤

Proof state:
n : WithTop ℕ∞
⊢ ⊤ + 1 = ↑⊤ ↔ ⊤ = ↑⊤

Tactic:
exact Iff.rfl

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Positive.lean
theorem IsPositive.orthogonalProjection_comp {T : E →L[𝕜] E} (hT : T.IsPositive) (U : Submodule 𝕜 E)
    [CompleteSpace U] : (orthogonalProjection U ∘L T ∘L U.subtypeL).IsPositive

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
this : ((orthogonalProjection U).comp (T.comp (adjoint (orthogonalProjection U)))).IsPositive
⊢ ((orthogonalProjection U).comp (T.comp U.subtypeL)).IsPositive

Tactic:
rwa [U.adjoint_orthogonalProjection] at this

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ ((orthogonalProjection U).comp (T.comp U.subtypeL)).IsPositive

Tactic:
have := hT.conj_adjoint (orthogonalProjection U : E →L[𝕜] U)

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
this : ((orthogonalProjection U).comp (T.comp (adjoint (orthogonalProjection U)))).IsPositive
⊢ ((orthogonalProjection U).comp (T.comp U.subtypeL)).IsPositive
-- Mathlib/CategoryTheory/GradedObject.lean
@[simp, reassoc]
lemma mapMap_comp [Z.HasMap p] : mapMap (φ ≫ ψ) p = mapMap φ p ≫ mapMap ψ p

Proof state:
I : Type u_1
J : Type u_2
C : Type u_4
inst✝³ : Category.{u_5, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
ψ : Y ⟶ Z
p : I → J
inst✝² : X.HasMap p
inst✝¹ : Y.HasMap p
inst✝ : Z.HasMap p
⊢ mapMap (φ ≫ ψ) p = mapMap φ p ≫ mapMap ψ p

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.imp_or' [Decidable b] : (a → b ∨ c) ↔ (a → b) ∨ (a → c) :=
  if h : b then by simp [h] else by
    rw [eq_false h, false_or]; exact (or_iff_right_of_imp fun hx x => (hx x).elim).symm

Proof state:
b : Prop
a : Sort u_1
c : Prop
inst✝ : Decidable b
h : ¬b
⊢ a → c ↔ (a → False) ∨ (a → c)

Tactic:
exact (or_iff_right_of_imp fun hx x => (hx x).elim).symm

Result:
no goals

Proof state:
b : Prop
a : Sort u_1
c : Prop
inst✝ : Decidable b
h : ¬b
⊢ a → b ∨ c ↔ (a → b) ∨ (a → c)

Tactic:
rw [eq_false h, false_or]

Result:
b : Prop
a : Sort u_1
c : Prop
inst✝ : Decidable b
h : ¬b
⊢ a → c ↔ (a → False) ∨ (a → c)

Proof state:
b : Prop
a : Sort u_1
c : Prop
inst✝ : Decidable b
h : b
⊢ a → b ∨ c ↔ (a → b) ∨ (a → c)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
/-- The String representation produced by toDigitsCore has the proper length relative to
the number of digits in `n < e` for some base `b`. Since this works with any base greater
than one, it can be used for binary, decimal, and hex. -/
lemma toDigitsCore_length (b : Nat) (h : 2 <= b) (f n e : Nat)
    (hlt : n < b ^ e) (h_e_pos : 0 < e) : (Nat.toDigitsCore b f n []).length <= e

Proof state:
b : ℕ
h : 2 ≤ b
f n e : ℕ
hlt : n < b ^ (e + 1)
h_e_pos : 0 < e + 1
h_pred_pos : 0 < e
x✝ : 0 < b
ih : (b.toDigitsCore f (n / b) []).length ≤ e
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1

Tactic:
if hdiv_ten : n / b = 0 then
  simp only [hdiv_ten]; exact Nat.le.step h_pred_pos
else
  simp only [hdiv_ten,
    toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b), if_false]
  exact Nat.succ_le_succ ih

Result:
no goals

Proof state:
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
hlt : n < b ^ (0 + 1)
h_e_pos : 0 < 0 + 1
h_pred_pos : ¬0 < 0
x✝¹ : b ^ 1 = b
x✝ : n < b
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0 + 1

Tactic:
simp [(@Nat.div_eq_of_lt n b ‹n < b› : n / b = 0)]

Result:
no goals

Proof state:
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
hlt : n < b ^ (0 + 1)
h_e_pos : 0 < 0 + 1
h_pred_pos : ¬0 < 0
x✝ : b ^ 1 = b
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0 + 1

Tactic:
have _ : n < b := ‹b ^ 1 = b› ▸ hlt

Result:
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
hlt : n < b ^ (0 + 1)
h_e_pos : 0 < 0 + 1
h_pred_pos : ¬0 < 0
x✝¹ : b ^ 1 = b
x✝ : n < b
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0 + 1

Proof state:
case succ.zero
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
hlt : n < b ^ 0
h_e_pos : 0 < 0
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0

Tactic:
exact False.elim (Nat.lt_irrefl 0 h_e_pos)

Result:
no goals

Proof state:
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n e : ℕ
hlt : n < b ^ (e + 1)
h_e_pos : 0 < e + 1
h_pred_pos : ¬0 < e
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ e + 1

Tactic:
obtain rfl : e = 0 := Nat.eq_zero_of_not_pos h_pred_pos

Result:
b : ℕ
h : 2 ≤ b
f : ℕ
ih : ∀ (n e : ℕ), n < b ^ e → 0 < e → (b.toDigitsCore f n []).length ≤ e
n : ℕ
hlt : n < b ^ (0 + 1)
h_e_pos : 0 < 0 + 1
h_pred_pos : ¬0 < 0
⊢ (if n / b = 0 then [(n % b).digitChar] else b.toDigitsCore f (n / b) [(n % b).digitChar]).length ≤ 0 + 1
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem card_add_two_mul_card_eq_rank :
    nrRealPlaces K + 2 * nrComplexPlaces K = finrank ℚ K

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ nrRealPlaces K + 2 * nrComplexPlaces K = finrank ℚ K

Tactic:
rw [← card_real_embeddings, ← card_complex_embeddings, Fintype.card_subtype_compl,
  ← Embeddings.card K ℂ, Nat.add_sub_of_le]

Result:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card { φ // ComplexEmbedding.IsReal φ } ≤ card (K →+* ℂ)

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ nrRealPlaces K + 2 * nrComplexPlaces K = finrank ℚ K

Tactic:
classical
rw [← card_real_embeddings, ← card_complex_embeddings, Fintype.card_subtype_compl,
  ← Embeddings.card K ℂ, Nat.add_sub_of_le]
exact Fintype.card_subtype_le _

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card { φ // ComplexEmbedding.IsReal φ } ≤ card (K →+* ℂ)

Tactic:
exact Fintype.card_subtype_le _

Result:
no goals
-- Mathlib/Topology/Order/LowerUpperTopology.lean
theorem isLowerSet_of_isOpen (h : IsOpen s) : IsLowerSet s

Proof state:
case sUnion
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
S✝ : Set (Set α)
a✝ : ∀ s ∈ S✝, GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
ih : ∀ s ∈ S✝, IsLowerSet s
⊢ IsLowerSet (⋃₀ S✝)

Tactic:
exact isLowerSet_sUnion ih

Result:
no goals

Proof state:
case basic
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s u : Set α
h' : u ∈ {t | ∃ a, (Ici a)ᶜ = t}
⊢ IsLowerSet u

Tactic:
obtain ⟨a, rfl⟩ := h'

Result:
case basic.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
a : α
⊢ IsLowerSet (Ici a)ᶜ

Proof state:
case basic.intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
a : α
⊢ IsLowerSet (Ici a)ᶜ

Tactic:
exact (isUpperSet_Ici a).compl

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
h : IsOpen s
⊢ IsLowerSet s

Tactic:
replace h := isOpen_iff_generate_Ici_compl.1 h

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
h : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
⊢ IsLowerSet s

Proof state:
case univ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ IsLowerSet univ

Tactic:
exact isLowerSet_univ

Result:
no goals

Proof state:
case inter
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s u v : Set α
a✝¹ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} u
a✝ : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} v
hu2 : IsLowerSet u
hv2 : IsLowerSet v
⊢ IsLowerSet (u ∩ v)

Tactic:
exact hu2.inter hv2

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
h : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
⊢ IsLowerSet s

Tactic:
induction h with
| basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl
| univ => exact isLowerSet_univ
| inter u v _ _ hu2 hv2 => exact hu2.inter hv2
| sUnion _ _ ih => exact isLowerSet_sUnion ih

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_mk {data : Array α} {size : data.size = n} {i : Nat} :
    (Vector.mk data size)[i]? = data[i]?

Proof state:
α : Type u_1
data : Array α
i : Nat
⊢ { toArray := data, size_toArray := ⋯ }[i]? = data[i]?

Tactic:
simp [getElem?_def]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
data : Array α
size : data.size = n
i : Nat
⊢ { toArray := data, size_toArray := size }[i]? = data[i]?

Tactic:
subst size

Result:
α : Type u_1
data : Array α
i : Nat
⊢ { toArray := data, size_toArray := ⋯ }[i]? = data[i]?