harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Moments/Basic.lean
theorem mgf_const (c : ℝ) [IsProbabilityMeasure μ] : mgf (fun _ => c) μ t = exp (t * c)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t c : ℝ
inst✝ : IsProbabilityMeasure μ
⊢ mgf (fun x => c) μ t = rexp (t * c)

Tactic:
simp only [mgf_const', measure_univ, ENNReal.one_toReal, one_mul]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem cyclotomic_eq_minpoly {n : ℕ} {K : Type*} [Field K] {μ : K} (h : IsPrimitiveRoot μ n)
    (hpos : 0 < n) [CharZero K] : cyclotomic n ℤ = minpoly ℤ μ

Proof state:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ cyclotomic n ℤ = minpoly ℤ μ

Tactic:
refine eq_of_monic_of_dvd_of_natDegree_le (minpoly.monic (IsPrimitiveRoot.isIntegral h hpos))
  (cyclotomic.monic n ℤ) (h.minpoly_dvd_cyclotomic hpos) ?_

Result:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ (cyclotomic n ℤ).natDegree ≤ (minpoly ℤ μ).natDegree

Proof state:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ (cyclotomic n ℤ).natDegree ≤ (minpoly ℤ μ).natDegree

Tactic:
simpa [natDegree_cyclotomic n ℤ] using totient_le_degree_minpoly h

Result:
no goals
-- Mathlib/Analysis/Analytic/Uniqueness.lean
theorem Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero {n : ℕ} {p : E[×n]→L[𝕜] F}
    (h : (fun y => p fun _ => y) =O[𝓝 0] fun y => ‖y‖ ^ (n + 1)) (y : E) : (p fun _ => y) = 0

Proof state:
case intro.intro.intro.intro.intro.intro.intro.succ.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : ContinuousMultilinearMap 𝕜 (fun i => E) F
ht : ∀ y ∈ t, ‖p fun x => y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
k : 𝕜
k_pos : 0 < ‖k‖
k_norm : ‖k‖ < δ * ‖y‖⁻¹ ⊓ ε * (c * ‖y‖ ^ (n.succ + 1))⁻¹
⊢ ‖p fun x => y‖ ≤ 0 + ε

Tactic:
have h₁ : ‖k • y‖ < δ := by
  rw [norm_smul]
  exact inv_mul_cancel_right₀ hy.ne.symm δ ▸
    mul_lt_mul_of_pos_right (lt_of_lt_of_le k_norm (min_le_left _ _)) hy

Result:
case intro.intro.intro.intro.intro.intro.intro.succ.intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
y : E
c : ℝ
c_pos : c > 0
t : Set E
t_open : IsOpen t
δ : ℝ
δ_pos : δ > 0
δε : Metric.ball 0 δ ⊆ t
n : ℕ
p : ContinuousMultilinearMap 𝕜 (fun i => E) F
ht : ∀ y ∈ t, ‖p fun x => y‖ ≤ c * ‖‖y‖ ^ (n + 1 + 1)‖
hy : 0 < ‖y‖
ε : ℝ
ε_pos : 0 < ε
h₀ : 0 < c * ‖y‖ ^ (n.succ + 1)
k : 𝕜
k_pos : 0 < ‖k‖
k_norm : ‖k‖ < δ * ‖y‖⁻¹ ⊓ ε * (c * ‖y‖ ^ (n.succ + 1))⁻¹
h₁ : ‖k • y‖ < δ
⊢ ‖p fun x => y‖ ≤ 0 + ε
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_shiftConcat {x : BitVec w} {b : Bool} (h : i < w) :
    (x.shiftConcat b)[i] = if i = 0 then b else x[i-1]

Proof state:
w i : Nat
x : BitVec w
b : Bool
h : i < w
⊢ (x.shiftConcat b)[i] = if i = 0 then b else x[i - 1]

Tactic:
rw [← getLsbD_eq_getElem, getLsbD_shiftConcat, getLsbD_eq_getElem, decide_eq_true h, Bool.true_and]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean
lemma strictAnti_eulerMascheroniSeq' : StrictAnti eulerMascheroniSeq'

Proof state:
n : ℕ
hn : n > 0
⊢ ↑(n + 1) ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case inr.refine_1
n : ℕ
hn : n > 0
⊢ 0 < (↑(n + 1) / ↑n)⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ
hn : n > 0
⊢ ↑n ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case inr
n : ℕ
hn : n > 0
⊢ ↑(harmonic (n + 1)) - log ↑(n + 1) < ↑(harmonic n) - log ↑n

Tactic:
rw [← sub_pos, sub_sub_sub_comm,
  harmonic_succ, Rat.cast_add, ← sub_sub, sub_self, zero_sub, sub_eq_add_neg, neg_sub,
  ← sub_eq_neg_add, sub_pos, ← log_div (by positivity) (by positivity), ← neg_lt_neg_iff,
  ← log_inv]

Result:
case inr
n : ℕ
hn : n > 0
⊢ log (↑(n + 1) / ↑n)⁻¹ < -↑(↑(n + 1))⁻¹

Proof state:
case inr.refine_3
n : ℕ
hn : n > 0
⊢ (↑(n + 1) / ↑n)⁻¹ - 1 = -↑(↑(n + 1))⁻¹

Tactic:
field_simp

Result:
no goals

Proof state:
case inr
n : ℕ
hn : n > 0
⊢ log (↑(n + 1) / ↑n)⁻¹ < -↑(↑(n + 1))⁻¹

Tactic:
refine (log_lt_sub_one_of_pos ?_ ?_).trans_le (le_of_eq ?_)

Result:
case inr.refine_1
n : ℕ
hn : n > 0
⊢ 0 < (↑(n + 1) / ↑n)⁻¹

case inr.refine_2
n : ℕ
hn : n > 0
⊢ (↑(n + 1) / ↑n)⁻¹ ≠ 1

case inr.refine_3
n : ℕ
hn : n > 0
⊢ (↑(n + 1) / ↑n)⁻¹ - 1 = -↑(↑(n + 1))⁻¹

Proof state:
case inr
n : ℕ
hn : n > 0
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n

Tactic:
simp_rw [eulerMascheroniSeq', eq_false_intro hn.ne', reduceCtorEq, if_false]

Result:
case inr
n : ℕ
hn : n > 0
⊢ ↑(harmonic (n + 1)) - log ↑(n + 1) < ↑(harmonic n) - log ↑n

Proof state:
⊢ StrictAnti eulerMascheroniSeq'

Tactic:
refine strictAnti_nat_of_succ_lt (fun n ↦ ?_)

Result:
n : ℕ
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n

Proof state:
case inl

⊢ eulerMascheroniSeq' (0 + 1) < eulerMascheroniSeq' 0

Tactic:
simp [eulerMascheroniSeq']

Result:
no goals

Proof state:
n : ℕ
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | hn

Result:
case inl

⊢ eulerMascheroniSeq' (0 + 1) < eulerMascheroniSeq' 0

case inr
n : ℕ
hn : n > 0
⊢ eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n

Proof state:
case inr.refine_2
n : ℕ
hn : n > 0
⊢ (↑(n + 1) / ↑n)⁻¹ ≠ 1

Tactic:
field_simp

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem IsRotated.symm (h : l ~r l') : l' ~r l

Proof state:
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ (hd :: tl).rotate n ~r hd :: tl

Tactic:
use (hd :: tl).length * n - n

Result:
case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ((hd :: tl).rotate n).rotate ((hd :: tl).length * n - n) = hd :: tl

Proof state:
α : Type u
n : ℕ
hd : α
tl : List α
⊢ 0 < (hd :: tl).length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l l' : List α
h : l ~r l'
⊢ l' ~r l

Tactic:
obtain ⟨n, rfl⟩ := h

Result:
case intro
α : Type u
l : List α
n : ℕ
⊢ l.rotate n ~r l

Proof state:
case intro.nil
α : Type u
n : ℕ
⊢ [].rotate n ~r []

Tactic:
exists 0

Result:
no goals

Proof state:
case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n ≤ (hd :: tl).length * n

Tactic:
exact Nat.le_mul_of_pos_left _ (by simp)

Result:
no goals

Proof state:
case intro
α : Type u
l : List α
n : ℕ
⊢ l.rotate n ~r l

Tactic:
rcases l with - | ⟨hd, tl⟩

Result:
case intro.nil
α : Type u
n : ℕ
⊢ [].rotate n ~r []

case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ (hd :: tl).rotate n ~r hd :: tl

Proof state:
case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ((hd :: tl).rotate n).rotate ((hd :: tl).length * n - n) = hd :: tl

Tactic:
rw [rotate_rotate, Nat.add_sub_cancel', rotate_length_mul]

Result:
case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n ≤ (hd :: tl).length * n
-- Mathlib/GroupTheory/Exponent.lean
theorem exponent_ne_zero_iff_range_orderOf_finite (h : ∀ g : G, 0 < orderOf g) :
    exponent G ≠ 0 ↔ (Set.range (orderOf : G → ℕ)).Finite

Proof state:
case refine_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
htpos : 0 < t.prod id
⊢ exponent G ∣ t.prod id

Tactic:
rw [exponent_dvd]

Result:
case refine_2.intro
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
htpos : 0 < t.prod id
⊢ ∀ (g : G), orderOf g ∣ t.prod id

Proof state:
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
htpos : 0 < t.prod id
this : exponent G ∣ t.prod id
⊢ exponent G ≠ 0

Tactic:
intro h

Result:
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
htpos : 0 < t.prod id
this : exponent G ∣ t.prod id
h : exponent G = 0
⊢ False

Proof state:
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
htpos : 0 < t.prod id
g : G
⊢ orderOf g ∈ t

Tactic:
rw [← Finset.mem_coe, ht]

Result:
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
htpos : 0 < t.prod id
g : G
⊢ orderOf g ∈ Set.range orderOf

Proof state:
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
htpos : 0 < t.prod id
this : exponent G ∣ t.prod id
h : exponent G = 0
⊢ False

Tactic:
rw [h, zero_dvd_iff] at this

Result:
G : Type u
inst✝ : Monoid G
h✝ : ∀ (g : G), 0 < orderOf g
t : Finset ℕ
ht : ↑t = Set.range orderOf
exponent_ne_zero_iff_range_orderOf_finite✝ exponent_ne_zero_iff_range_orderOf_finite :
  (∀ (g : G), 0 < orderOf g) → (exponent G ≠ 0 ↔ (↑t).Finite)
htpos : 0 < t.prod id
this : t.prod id = 0
h : exponent G = 0
⊢ False
-- Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
@[simp]
lemma localized₀_top : (⊤ : Submodule R M).localized₀ p f = ⊤

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
x : N
a✝ : x ∈ ⊤
⊢ x ∈ localized₀ p f ⊤

Tactic:
obtain ⟨⟨x, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective p f x

Result:
case intro.mk
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
x : M
s : ↥p
a✝ : Function.uncurry (IsLocalizedModule.mk' f) (x, s) ∈ ⊤
⊢ Function.uncurry (IsLocalizedModule.mk' f) (x, s) ∈ localized₀ p f ⊤

Proof state:
case intro.mk
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
x : M
s : ↥p
a✝ : Function.uncurry (IsLocalizedModule.mk' f) (x, s) ∈ ⊤
⊢ Function.uncurry (IsLocalizedModule.mk' f) (x, s) ∈ localized₀ p f ⊤

Tactic:
exact ⟨x, trivial, s, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ localized₀ p f ⊤ = ⊤

Tactic:
rw [← top_le_iff]

Result:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ ⊤ ≤ localized₀ p f ⊤

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
⊢ ⊤ ≤ localized₀ p f ⊤

Tactic:
rintro x _

Result:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
x : N
a✝ : x ∈ ⊤
⊢ x ∈ localized₀ p f ⊤
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_mul_relfinrank_eq_inf_relfinrank (h : B ≤ C) :
    relfinrank A B * relfinrank B C = (A ⊓ B).relfinrank C

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B C : IntermediateField F E
h : B ≤ C
⊢ A.relfinrank B * B.relfinrank C = (A ⊓ B).relfinrank C

Tactic:
simpa using congr(toNat $(relrank_mul_relrank_eq_inf_relrank A h))

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem ack_two (n : ℕ) : ack 2 n = 2 * n + 3

Proof state:
n : ℕ
⊢ ack 2 n = 2 * n + 3

Tactic:
induction' n with n IH

Result:
case zero

⊢ ack 2 0 = 2 * 0 + 3

case succ
n : ℕ
IH : ack 2 n = 2 * n + 3
⊢ ack 2 (n + 1) = 2 * (n + 1) + 3

Proof state:
case succ
n : ℕ
IH : ack 2 n = 2 * n + 3
⊢ ack 2 (n + 1) = 2 * (n + 1) + 3

Tactic:
simpa [mul_succ]

Result:
no goals

Proof state:
case zero

⊢ ack 2 0 = 2 * 0 + 3

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem commMap_canonical_eq_mixed (x : K) :
    commMap K (canonicalEmbedding K x) = mixedEmbedding K x

Proof state:
K : Type u_1
inst✝ : Field K
x : K
⊢ (fun w => ((↑w).embedding x).re) = (Pi.ringHom fun w => embedding_of_isReal ⋯) x ∧
    (fun w => (↑w).embedding x) = (Pi.ringHom fun w => (↑w).embedding) x

Tactic:
exact ⟨rfl, rfl⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
x : K
⊢ (commMap K) ((canonicalEmbedding K) x) = (mixedEmbedding K) x

Tactic:
simp only [canonicalEmbedding, commMap, LinearMap.coe_mk, AddHom.coe_mk, Pi.ringHom_apply,
  mixedEmbedding, RingHom.prod_apply, Prod.mk.injEq]

Result:
K : Type u_1
inst✝ : Field K
x : K
⊢ (fun w => ((↑w).embedding x).re) = (Pi.ringHom fun w => embedding_of_isReal ⋯) x ∧
    (fun w => (↑w).embedding x) = (Pi.ringHom fun w => (↑w).embedding) x
-- Mathlib/Data/List/Basic.lean
theorem map_surjective_iff {f : α → β} : Surjective (map f) ↔ Surjective f

Proof state:
α : Type u
β : Type v
f : α → β
h : Surjective (map f)
x : β
y : α
hxy : map f [y] = [x]
⊢ ∃ a, f a = x

Tactic:
exact ⟨_, List.singleton_injective hxy⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
h : Surjective (map f)
x : β
⊢ ∃ a, f a = x

Tactic:
let ⟨[y], hxy⟩ := h [x]

Result:
α : Type u
β : Type v
f : α → β
h : Surjective (map f)
x : β
y : α
hxy : map f [y] = [x]
⊢ ∃ a, f a = x
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma image_coe_Icc (x y : ℝ) : Real.toEReal '' Icc x y = Icc ↑x ↑y

Proof state:
x y : ℝ
⊢ Real.toEReal '' Icc x y = Icc ↑x ↑y

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_

Result:
x y : ℝ
⊢ WithBot.some '' (WithTop.some '' Icc x y) = Icc ↑x ↑y

Proof state:
x y : ℝ
⊢ Icc ↑↑x ↑↑y = Icc ↑x ↑y

Tactic:
rfl

Result:
no goals

Proof state:
x y : ℝ
⊢ WithBot.some '' (WithTop.some '' Icc x y) = Icc ↑x ↑y

Tactic:
rw [WithTop.image_coe_Icc, WithBot.image_coe_Icc]

Result:
x y : ℝ
⊢ Icc ↑↑x ↑↑y = Icc ↑x ↑y
-- Mathlib/Order/Filter/Basic.lean
theorem eventually_or_distrib_left {f : Filter α} {p : Prop} {q : α → Prop} :
    (∀ᶠ x in f, p ∨ q x) ↔ p ∨ ∀ᶠ x in f, q x :=
  by_cases (fun h : p => by simp [h]) fun h => by simp [h]

Proof state:
α : Type u
f : Filter α
p : Prop
q : α → Prop
h : ¬p
⊢ (∀ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∀ᶠ (x : α) in f, q x

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u
f : Filter α
p : Prop
q : α → Prop
h : p
⊢ (∀ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∀ᶠ (x : α) in f, q x

Tactic:
simp [h]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
theorem Hom.ext {S₁ S₂ : Split C} (Φ₁ Φ₂ : Hom S₁ S₂) (h : ∀ n : ℕ, Φ₁.f n = Φ₂.f n) : Φ₁ = Φ₂

Proof state:
case mk.mk.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ }.f n = { F := F₂, f := f₁, comm := c₂ }.f n
n : ℕ
⊢ S₁.s.φ F₁ n = S₁.s.φ F₂ n

Tactic:
dsimp

Result:
case mk.mk.h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
S₁ S₂ : Split C
F₁ : S₁.X ⟶ S₂.X
f₁ : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n
c₁ : ∀ (n : ℕ), S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
F₂ : S₁.X ⟶ S₂.X
c₂ : ∀ (n : ℕ), S₁.s.ι n ≫ F₂.app (op ⦋n⦌) = f₁ n ≫ S₂.s.ι n
h : ∀ (n : ℕ), { F := F₁, f := f₁, comm := c₁ }.f n = { F := F₂, f := f₁, comm := c₂ }.f n
n : ℕ
⊢ S₁.s.ι n ≫ F₁.app (op ⦋n⦌) = S₁.s.ι n ≫ F₂.app (op ⦋n⦌)
-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem volume_closedBall {x : AddCircle T} (ε : ℝ) :
    volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
⊢ volume (Metric.closedBall x ε) = ENNReal.ofReal (T ⊓ 2 * ε)

Tactic:
have h₂ : (↑) ⁻¹' Metric.closedBall (0 : AddCircle T) ε ∩ I =
    if ε < T / 2 then Metric.closedBall (0 : ℝ) ε else I := by
  conv_rhs => rw [← if_ctx_congr (Iff.rfl : ε < T / 2 ↔ ε < T / 2) h₁ fun _ => rfl, ← hT']
  apply coe_real_preimage_closedBall_inter_eq
  simpa only [hT', Real.closedBall_eq_Icc, zero_add, zero_sub] using Ioc_subset_Icc_self

Result:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ : QuotientAddGroup.mk ⁻¹' Metric.closedBall 0 ε ∩ I = if ε < T / 2 then Metric.closedBall 0 ε else I
⊢ volume (Metric.closedBall x ε) = ENNReal.ofReal (T ⊓ 2 * ε)

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε
h₂ : QuotientAddGroup.mk ⁻¹' Metric.closedBall 0 ε ∩ I = if ε < T / 2 then Metric.closedBall 0 ε else I
hε : ¬ε < T / 2
⊢ T ≤ 2 * ε

Tactic:
linarith

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
⊢ Icc (-ε) ε ⊆ I

Tactic:
rintro y ⟨hy₁, hy₂⟩

Result:
case intro
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hT' : |T| = T
I : Set ℝ := Ioc (-(T / 2)) (T / 2)
hε : ε < T / 2
y : ℝ
hy₁ : -ε ≤ y
hy₂ : y ≤ ε
⊢ y ∈ I
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.prod_self (hl : la.HasBasis pa sa) :
    (la ×ˢ la).HasBasis pa fun i => sa i ×ˢ sa i :=
  hl.prod_same_index hl fun {i j} hi hj => by
    simpa only [exists_prop, subset_inter_iff] using
      hl.mem_iff.1 (inter_mem (hl.mem_of_mem hi) (hl.mem_of_mem hj))

Proof state:
α : Type u_1
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
hl : la.HasBasis pa sa
i j : ι
hi : pa i
hj : pa j
⊢ ∃ k, pa k ∧ sa k ⊆ sa i ∧ sa k ⊆ sa j

Tactic:
simpa only [exists_prop, subset_inter_iff] using
  hl.mem_iff.1 (inter_mem (hl.mem_of_mem hi) (hl.mem_of_mem hj))

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem nhds_order_unbounded [OrderTopology α] {a : α} (hu : ∃ u, a < u) (hl : ∃ l, l < a) :
    𝓝 a = ⨅ (l) (_ : l < a) (u) (_ : a < u), 𝓟 (Ioo l u)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
hu : ∃ u, a < u
hl : ∃ l, l < a
⊢ 𝓝 a = ⨅ l, ⨅ (_ : l < a), ⨅ u, ⨅ (_ : a < u), 𝓟 (Ioo l u)

Tactic:
simp only [nhds_eq_order, ← inf_biInf, ← biInf_inf, *, ← inf_principal, ← Ioi_inter_Iio]

Result:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
hu : ∃ u, a < u
hl : ∃ l, l < a
⊢ (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) = (⨅ i, ⨅ (_ : i < a), 𝓟 (Ioi i)) ⊓ ⨅ i, ⨅ (_ : a < i), 𝓟 (Iio i)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
hu : ∃ u, a < u
hl : ∃ l, l < a
⊢ (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b) = (⨅ i, ⨅ (_ : i < a), 𝓟 (Ioi i)) ⊓ ⨅ i, ⨅ (_ : a < i), 𝓟 (Iio i)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem closure_preimage_eq_top (s : Set G) : closure ((closure s).subtype ⁻¹' s) = ⊤

Proof state:
case a
G : Type u_1
inst✝ : Group G
s : Set G
⊢ map (closure s).subtype (closure (⇑(closure s).subtype ⁻¹' s)) = map (closure s).subtype ⊤

Tactic:
rw [MonoidHom.map_closure, ← MonoidHom.range_eq_map, range_subtype,
  Set.image_preimage_eq_of_subset]

Result:
case a
G : Type u_1
inst✝ : Group G
s : Set G
⊢ s ⊆ Set.range ⇑(closure s).subtype

Proof state:
case a
G : Type u_1
inst✝ : Group G
s : Set G
⊢ s ⊆ {x | x ∈ closure s}

Tactic:
exact subset_closure

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure (⇑(closure s).subtype ⁻¹' s) = ⊤

Tactic:
apply map_injective (closure s).subtype_injective

Result:
case a
G : Type u_1
inst✝ : Group G
s : Set G
⊢ map (closure s).subtype (closure (⇑(closure s).subtype ⁻¹' s)) = map (closure s).subtype ⊤

Proof state:
case a
G : Type u_1
inst✝ : Group G
s : Set G
⊢ s ⊆ Set.range ⇑(closure s).subtype

Tactic:
rw [coe_subtype, Subtype.range_coe_subtype]

Result:
case a
G : Type u_1
inst✝ : Group G
s : Set G
⊢ s ⊆ {x | x ∈ closure s}
-- Mathlib/RingTheory/Ideal/Span.lean
theorem ker_toSpanSingleton_eq_span :
    LinearMap.ker (LinearMap.toSpanSingleton R R e) = Ideal.span {1 - e} := SetLike.ext fun x ↦ by
  rw [Ideal.mem_span_singleton']
  refine ⟨fun h ↦ ⟨x, by rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]⟩, fun h ↦ ?_⟩
  obtain ⟨x, rfl⟩ := h
  show x * (1 - e) * e = 0
  rw [mul_assoc, sub_mul, one_mul, he, sub_self, mul_zero]

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * (1 - e) * e = 0

Tactic:
rw [mul_assoc, sub_mul, one_mul, he, sub_self, mul_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : ∃ a, a * (1 - e) = x
⊢ x ∈ LinearMap.ker (LinearMap.toSpanSingleton R R e)

Tactic:
obtain ⟨x, rfl⟩ := h

Result:
case intro
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * (1 - e) ∈ LinearMap.ker (LinearMap.toSpanSingleton R R e)

Proof state:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x ∈ LinearMap.ker (LinearMap.toSpanSingleton R R e) ↔ ∃ a, a * (1 - e) = x

Tactic:
refine ⟨fun h ↦ ⟨x, by rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]⟩, fun h ↦ ?_⟩

Result:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : ∃ a, a * (1 - e) = x
⊢ x ∈ LinearMap.ker (LinearMap.toSpanSingleton R R e)

Proof state:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : x ∈ LinearMap.ker (LinearMap.toSpanSingleton R R e)
⊢ x * (1 - e) = x

Tactic:
rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x ∈ LinearMap.ker (LinearMap.toSpanSingleton R R e) ↔ x ∈ Ideal.span {1 - e}

Tactic:
rw [Ideal.mem_span_singleton']

Result:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x ∈ LinearMap.ker (LinearMap.toSpanSingleton R R e) ↔ ∃ a, a * (1 - e) = x

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * (1 - e) ∈ LinearMap.ker (LinearMap.toSpanSingleton R R e)

Tactic:
show x * (1 - e) * e = 0

Result:
case intro
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * (1 - e) * e = 0
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem sSup_def {S : Set (Con M)} :
    sSup S = conGen (sSup ((⇑) '' S))

Proof state:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ (conGen fun x y => ∃ c ∈ S, c x y) = conGen (⨆ a ∈ S, ⇑a)

Tactic:
congr with (x y)

Result:
case e_r.h.h.a
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x y : M
⊢ (∃ c ∈ S, c x y) ↔ (⨆ a ∈ S, ⇑a) x y

Proof state:
case e_r.h.h.a
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x y : M
⊢ (∃ c ∈ S, c x y) ↔ (⨆ a ∈ S, ⇑a) x y

Tactic:
simp only [sSup_image, iSup_apply, iSup_Prop_eq, exists_prop, rel_eq_coe]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ sSup S = conGen (sSup (DFunLike.coe '' S))

Tactic:
rw [sSup_eq_conGen, sSup_image]

Result:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
⊢ (conGen fun x y => ∃ c ∈ S, c x y) = conGen (⨆ a ∈ S, ⇑a)