harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
lemma yonedaULiftEquiv_symm_naturality_right (X : C) {F F' : Sheaf J (Type (max v v'))}
    (f : F ⟶ F') (x : F.val.obj ⟨X⟩) :
      J.yonedaULiftEquiv.symm x ≫ f = J.yonedaULiftEquiv.symm (f.val.app ⟨X⟩ x)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
F F' : Sheaf J (Type (max v v'))
f : F ⟶ F'
x : F.val.obj (op X)
⊢ J.yonedaULiftEquiv.symm x ≫ f = J.yonedaULiftEquiv.symm (f.val.app (op X) x)

Tactic:
apply J.yonedaULiftEquiv.injective

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
F F' : Sheaf J (Type (max v v'))
f : F ⟶ F'
x : F.val.obj (op X)
⊢ J.yonedaULiftEquiv (J.yonedaULiftEquiv.symm x ≫ f) = J.yonedaULiftEquiv (J.yonedaULiftEquiv.symm (f.val.app (op X) x))

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
F F' : Sheaf J (Type (max v v'))
f : F ⟶ F'
x : F.val.obj (op X)
⊢ J.yonedaULiftEquiv (J.yonedaULiftEquiv.symm x ≫ f) = J.yonedaULiftEquiv (J.yonedaULiftEquiv.symm (f.val.app (op X) x))

Tactic:
simp [yonedaULiftEquiv_comp]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
theorem mul_eq_one_comm_of_equiv {A : Matrix m n R} {B : Matrix n m R} (e : m ≃ n) :
    A * B = 1 ↔ B * A = 1

Proof state:
n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ A * B = 1 ↔ B * A = 1

Tactic:
refine (reindex e e).injective.eq_iff.symm.trans ?_

Result:
n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ (reindex e e) (A * B) = (reindex e e) 1 ↔ B * A = 1

Proof state:
n : Type u_1
m : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ (reindex e e) (A * B) = (reindex e e) 1 ↔ B * A = 1

Tactic:
rw [reindex_apply, reindex_apply, submatrix_one_equiv, ← submatrix_mul_equiv _ _ _ (.refl _),
  mul_eq_one_comm, submatrix_mul_equiv, coe_refl, submatrix_id_id]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/SumCoeff.lean
theorem LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg (f : ℕ → ℝ) {l : ℝ}
    (hf : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / (n : ℝ)) atTop (𝓝 l))
    (hf' : ∀ n, 0 ≤ f n) :
    Tendsto (fun s : ℝ ↦ (s - 1) * LSeries (fun n ↦ f n) s) (𝓝[>] 1) (𝓝 l)

Proof state:
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑(↑n ^ 1)) atTop (𝓝 ?m.245580)

Tactic:
simpa

Result:
no goals

Proof state:
case refine_2
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ (fun n => ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n => ↑n ^ 1

Tactic:
exact isBigO_atTop_natCast_rpow_of_tendsto_div_rpow (by simpa)

Result:
no goals

Proof state:
case refine_2
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ LSeriesSummable (fun n => ↑(f n)) ↑s

Tactic:
refine LSeriesSummable_of_sum_norm_bigO_and_nonneg ?_ hf' zero_le_one hs

Result:
case refine_2
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ (fun n => ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n => ↑n ^ 1

Proof state:
case refine_1
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
x✝ : ℕ
⊢ ↑((∑ k ∈ Icc 1 x✝, f k) / ↑x✝) = (∑ k ∈ Icc 1 x✝, (fun n => ↑(f n)) k) / ↑x✝

Tactic:
simp

Result:
no goals

Proof state:
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
⊢ Tendsto (fun s => (↑s - 1) * LSeries (fun n => ↑(f n)) ↑s) (𝓝[>] 1) (𝓝 ↑l)

Tactic:
refine  LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div (f := fun n ↦ f n)
  (hf.ofReal.congr fun _ ↦ ?_) fun s hs ↦ ?_

Result:
case refine_1
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
x✝ : ℕ
⊢ ↑((∑ k ∈ Icc 1 x✝, f k) / ↑x✝) = (∑ k ∈ Icc 1 x✝, (fun n => ↑(f n)) k) / ↑x✝

case refine_2
f : ℕ → ℝ
l : ℝ
hf : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hf' : ∀ (n : ℕ), 0 ≤ f n
s : ℝ
hs : 1 < s
⊢ LSeriesSummable (fun n => ↑(f n)) ↑s
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem Adapted.measurable_upcrossingsBefore (hf : Adapted ℱ f) (hab : a < b) :
    Measurable (upcrossingsBefore a b f N)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hab : a < b
⊢ Measurable (upcrossingsBefore a b f N)

Tactic:
have : upcrossingsBefore a b f N = fun ω =>
    ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i := by
  ext ω
  exact upcrossingsBefore_eq_sum hab

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hab : a < b
this :
  upcrossingsBefore a b f N = fun ω => ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i
⊢ Measurable (upcrossingsBefore a b f N)

Proof state:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hab : a < b
ω : Ω
⊢ upcrossingsBefore a b f N ω = ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i

Tactic:
exact upcrossingsBefore_eq_sum hab

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hab : a < b
this :
  upcrossingsBefore a b f N = fun ω => ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i
⊢ Measurable (upcrossingsBefore a b f N)

Tactic:
rw [this]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hab : a < b
this :
  upcrossingsBefore a b f N = fun ω => ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i
⊢ Measurable fun ω => ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hab : a < b
⊢ upcrossingsBefore a b f N = fun ω => ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i

Tactic:
ext ω

Result:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hab : a < b
ω : Ω
⊢ upcrossingsBefore a b f N ω = ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
hab : a < b
this :
  upcrossingsBefore a b f N = fun ω => ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i
⊢ Measurable fun ω => ∑ i ∈ Finset.Ico 1 (N + 1), {n | upperCrossingTime a b f N n ω < N}.indicator 1 i

Tactic:
exact Finset.measurable_sum _ fun i _ => Measurable.indicator measurable_const <|
  ℱ.le N _ (hf.isStoppingTime_upperCrossingTime.measurableSet_lt_of_pred N)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem data_takeWhile (p) : ∀ {s}, Valid s →
    (s.takeWhile p).toString.1 = s.toString.1.takeWhile p
  | _, h => let ⟨_, _, _, h⟩ := h.validFor; by simp [(h.takeWhile _).toString, h.toString]

Proof state:
p : Char → Bool
x✝ : Substring
h✝ : x✝.Valid
w✝² w✝¹ w✝ : List Char
h : ValidFor w✝² w✝¹ w✝ x✝
⊢ (x✝.takeWhile p).toString.data = List.takeWhile p x✝.toString.data

Tactic:
simp [(h.takeWhile _).toString, h.toString]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem InjOn.image_biInter_eq {p : ι → Prop} {s : ∀ i, p i → Set α} (hp : ∃ i, p i)
    {f : α → β} (h : InjOn f (⋃ (i) (hi), s i hi)) :
    (f '' ⋂ (i) (hi), s i hi) = ⋂ (i) (hi), f '' s i hi

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
⊢ f '' ⋂ i, ⋂ (hi : p i), s i hi = ⋂ i, ⋂ (hi : p i), f '' s i hi

Tactic:
simp only [iInter, iInf_subtype']

Result:
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
⊢ f '' ⨅ x, s ↑x ⋯ = ⨅ x, f '' s ↑x ⋯

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ f '' ⨅ x, s ↑x ⋯ = ⨅ x, f '' s ↑x ⋯

Tactic:
apply InjOn.image_iInter_eq

Result:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ InjOn f (⋃ i, s ↑i ⋯)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
⊢ f '' ⨅ x, s ↑x ⋯ = ⨅ x, f '' s ↑x ⋯

Tactic:
haveI : Nonempty { i // p i } := nonempty_subtype.2 hp

Result:
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ f '' ⨅ x, s ↑x ⋯ = ⨅ x, f '' s ↑x ⋯

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ InjOn f (⋃ i, s ↑i ⋯)

Tactic:
simpa only [iUnion, iSup_subtype'] using h

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem dedup_cons {a : α} {s : Multiset α} : dedup (a ::ₘ s) = ndinsert a (dedup s)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (a ::ₘ s).dedup = ndinsert a s.dedup

Tactic:
by_cases h : a ∈ s <;> simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_mono_nnnorm_ae {f : α → F} {g : α → G} (h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) :
    eLpNorm f p μ ≤ eLpNorm g p μ

Proof state:
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
⊢ (if p = 0 then 0 else if p = ⊤ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = 0 then 0 else if p = ⊤ then eLpNormEssSup g μ else eLpNorm' g p.toReal μ

Tactic:
split_ifs

Result:
case pos
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
h✝ : p = 0
⊢ 0 ≤ 0

case pos
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
h✝¹ : ¬p = 0
h✝ : p = ⊤
⊢ eLpNormEssSup f μ ≤ eLpNormEssSup g μ

case neg
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
h✝¹ : ¬p = 0
h✝ : ¬p = ⊤
⊢ eLpNorm' f p.toReal μ ≤ eLpNorm' g p.toReal μ

Proof state:
case neg
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
h✝¹ : ¬p = 0
h✝ : ¬p = ⊤
⊢ eLpNorm' f p.toReal μ ≤ eLpNorm' g p.toReal μ

Tactic:
exact eLpNorm'_mono_nnnorm_ae ENNReal.toReal_nonneg h

Result:
no goals

Proof state:
case pos
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
h✝ : p = 0
⊢ 0 ≤ 0

Tactic:
exact le_rfl

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
⊢ eLpNorm f p μ ≤ eLpNorm g p μ

Tactic:
simp only [eLpNorm]

Result:
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
⊢ (if p = 0 then 0 else if p = ⊤ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = 0 then 0 else if p = ⊤ then eLpNormEssSup g μ else eLpNorm' g p.toReal μ

Proof state:
case pos
α : Type u_1
F : Type u_4
G : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
h✝¹ : ¬p = 0
h✝ : p = ⊤
⊢ eLpNormEssSup f μ ≤ eLpNormEssSup g μ

Tactic:
exact essSup_mono_ae (h.mono fun x hx => ENNReal.coe_le_coe.mpr hx)

Result:
no goals
-- Mathlib/Data/Rat/Floor.lean
theorem Nat.coprime_sub_mul_floor_rat_div_of_coprime {n d : ℕ} (n_coprime_d : n.Coprime d) :
    ((n : ℤ) - d * ⌊(n : ℚ) / d⌋).natAbs.Coprime d

Proof state:
n d : ℕ
n_coprime_d : n.Coprime d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ (↑n - ↑d * ⌊↑n / ↑d⌋).natAbs.Coprime d

Tactic:
rw [← this]

Result:
n d : ℕ
n_coprime_d : n.Coprime d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ (↑n % ↑d).natAbs.Coprime d

Proof state:
n d : ℕ
n_coprime_d : n.Coprime d
this✝ : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
this : d.Coprime n
⊢ (↑n % ↑d).natAbs.Coprime d

Tactic:
rwa [Nat.Coprime, Nat.gcd_rec] at this

Result:
no goals

Proof state:
n d : ℕ
n_coprime_d : n.Coprime d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ (↑n % ↑d).natAbs.Coprime d

Tactic:
have : d.Coprime n := n_coprime_d.symm

Result:
n d : ℕ
n_coprime_d : n.Coprime d
this✝ : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
this : d.Coprime n
⊢ (↑n % ↑d).natAbs.Coprime d

Proof state:
n d : ℕ
n_coprime_d : n.Coprime d
⊢ (↑n - ↑d * ⌊↑n / ↑d⌋).natAbs.Coprime d

Tactic:
have : (n : ℤ) % d = n - d * ⌊(n : ℚ) / d⌋ := Int.mod_nat_eq_sub_mul_floor_rat_div

Result:
n d : ℕ
n_coprime_d : n.Coprime d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ (↑n - ↑d * ⌊↑n / ↑d⌋).natAbs.Coprime d
-- Mathlib/Algebra/Vertex/VertexOperator.lean
theorem ncoeff_eq_zero_of_lt_order (A : VertexOperator R V) (n : ℤ) (x : V)
    (h : -n - 1 < HahnSeries.order ((HahnModule.of R).symm (A x))) : (A [[n]]) x = 0

Proof state:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
x : V
h : -n - 1 < ((HahnModule.of R).symm (A x)).order
⊢ (A[[n]]) x = 0

Tactic:
simp only [ncoeff, HVertexOperator.coeff, LinearMap.coe_mk, AddHom.coe_mk]

Result:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
x : V
h : -n - 1 < ((HahnModule.of R).symm (A x)).order
⊢ ((HahnModule.of R).symm (A x)).coeff (-n - 1) = 0

Proof state:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
x : V
h : -n - 1 < ((HahnModule.of R).symm (A x)).order
⊢ ((HahnModule.of R).symm (A x)).coeff (-n - 1) = 0

Tactic:
exact HahnSeries.coeff_eq_zero_of_lt_order h

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem nim_birthday (o : Ordinal) : (nim o).birthday = o

Proof state:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, (nim k).birthday = k
⊢ ((lsub fun i => (nim ↑(o.enumIsoToType.symm i)).birthday) ⊔ lsub fun i => (nim ↑(o.enumIsoToType.symm i)).birthday) =
    o

Tactic:
rw [max_eq_right le_rfl]

Result:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, (nim k).birthday = k
⊢ (lsub fun i => (nim ↑(o.enumIsoToType.symm i)).birthday) = o

Proof state:
o : Ordinal.{u_1}
⊢ (nim o).birthday = o

Tactic:
induction' o using Ordinal.induction with o IH

Result:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, (nim k).birthday = k
⊢ (nim o).birthday = o

Proof state:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, (nim k).birthday = k
⊢ (nim o).birthday = o

Tactic:
rw [nim, birthday_def]

Result:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, (nim k).birthday = k
⊢ ((lsub fun i =>
        ((mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)).moveLeft
            i).birthday) ⊔
      lsub fun i =>
        ((mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x =>
                nim ↑(o.enumIsoToType.symm x)).moveRight
            i).birthday) =
    o

Proof state:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, (nim k).birthday = k
⊢ ((lsub fun i =>
        ((mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)).moveLeft
            i).birthday) ⊔
      lsub fun i =>
        ((mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x =>
                nim ↑(o.enumIsoToType.symm x)).moveRight
            i).birthday) =
    o

Tactic:
dsimp

Result:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, (nim k).birthday = k
⊢ ((lsub fun i => (nim ↑(o.enumIsoToType.symm i)).birthday) ⊔ lsub fun i => (nim ↑(o.enumIsoToType.symm i)).birthday) =
    o

Proof state:
case h.e'_2.h.e'_2.h
o : Ordinal.{u_1}
IH : ∀ k < o, (nim k).birthday = k
i : o.toType
⊢ (nim ↑(o.enumIsoToType.symm i)).birthday = (typein fun x1 x2 => x1 < x2).toRelEmbedding i

Tactic:
exact IH _ (typein_lt_self i)

Result:
no goals

Proof state:
case h
o : Ordinal.{u_1}
IH : ∀ k < o, (nim k).birthday = k
⊢ (lsub fun i => (nim ↑(o.enumIsoToType.symm i)).birthday) = o

Tactic:
convert lsub_typein o with i

Result:
case h.e'_2.h.e'_2.h
o : Ordinal.{u_1}
IH : ∀ k < o, (nim k).birthday = k
i : o.toType
⊢ (nim ↑(o.enumIsoToType.symm i)).birthday = (typein fun x1 x2 => x1 < x2).toRelEmbedding i
-- Mathlib/Algebra/Quaternion.lean
theorem finrank_eq_four [StrongRankCondition R] : Module.finrank R ℍ[R,c₁,c₂,c₃] = 4

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
⊢ Module.finrank R ℍ[R,c₁,c₂,c₃] = 4

Tactic:
rw [Module.finrank, rank_eq_four, Cardinal.toNat_ofNat]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_update_zero (p : R[X]) (n : ℕ) : support (p.update n 0) = p.support.erase n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p.update n 0).support = p.support.erase n

Tactic:
rw [update_zero_eq_erase, support_erase]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem bind_singleton (f : α → β) : (s.bind fun x => ({f x} : Multiset β)) = map f s :=
  Multiset.induction_on s (by rw [zero_bind, map_zero]) (by simp [singleton_add])

Proof state:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ ∀ (a : α) (s : Multiset α), (s.bind fun x => {f x}) = map f s → ((a ::ₘ s).bind fun x => {f x}) = map f (a ::ₘ s)

Tactic:
simp [singleton_add]

Result:
no goals

Proof state:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ (bind 0 fun x => {f x}) = map f 0

Tactic:
rw [zero_bind, map_zero]

Result:
no goals
-- Mathlib/Algebra/Star/Pointwise.lean
@[simp]
lemma StarMemClass.star_coe_eq {S α : Type*} [InvolutiveStar α] [SetLike S α]
    [StarMemClass S α] (s : S) : star (s : Set α) = s

Proof state:
case h
S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
x : α
⊢ star x ∈ s ↔ x ∈ s

Tactic:
exact ⟨by simpa only [star_star] using star_mem (s := s) (r := star x), star_mem⟩

Result:
no goals

Proof state:
S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
⊢ star ↑s = ↑s

Tactic:
ext x

Result:
case h
S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
x : α
⊢ x ∈ star ↑s ↔ x ∈ ↑s

Proof state:
S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
x : α
⊢ star x ∈ s → x ∈ s

Tactic:
simpa only [star_star] using star_mem (s := s) (r := star x)

Result:
no goals

Proof state:
case h
S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
x : α
⊢ x ∈ star ↑s ↔ x ∈ ↑s

Tactic:
simp only [Set.mem_star, SetLike.mem_coe]

Result:
case h
S : Type u_1
α : Type u_2
inst✝² : InvolutiveStar α
inst✝¹ : SetLike S α
inst✝ : StarMemClass S α
s : S
x : α
⊢ star x ∈ s ↔ x ∈ s
-- Mathlib/MeasureTheory/Group/Integral.lean
theorem integral_div_left_eq_self (f : G → E) (μ : Measure G) [IsInvInvariant μ]
    [IsMulLeftInvariant μ] (x' : G) : (∫ x, f (x' / x) ∂μ) = ∫ x, f x ∂μ

Proof state:
G : Type u_4
E : Type u_5
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → E
μ : Measure G
inst✝¹ : μ.IsInvInvariant
inst✝ : μ.IsMulLeftInvariant
x' : G
⊢ ∫ (x : G), f (x' / x) ∂μ = ∫ (x : G), f x ∂μ

Tactic:
simp_rw [div_eq_mul_inv, integral_inv_eq_self (fun x => f (x' * x)) μ,
  integral_mul_left_eq_self f x']

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem closure_preimage_le (f : G →* N) (s : Set N) : closure (f ⁻¹' s) ≤ (closure s).comap f :=
  (closure_le _).2 fun x hx => by rw [SetLike.mem_coe, mem_comap]; exact subset_closure hx

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
s : Set N
x : G
hx : x ∈ ⇑f ⁻¹' s
⊢ f x ∈ closure s

Tactic:
exact subset_closure hx

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
s : Set N
x : G
hx : x ∈ ⇑f ⁻¹' s
⊢ x ∈ ↑(comap f (closure s))

Tactic:
rw [SetLike.mem_coe, mem_comap]

Result:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
s : Set N
x : G
hx : x ∈ ⇑f ⁻¹' s
⊢ f x ∈ closure s
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
/-- The following diagram is a pullback
```
X --f--> Z
|        |
id       id
v        v
X --f--> Z
```
-/
lemma id_vert (f : X ⟶ Z) : IsPullback f (𝟙 X) (𝟙 Z) f :=
  of_vert_isIso ⟨by simp only [Category.id_comp, Category.comp_id]⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
f : X ⟶ Z
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp only [Category.id_comp, Category.comp_id]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_le_of_le_log (hy : 0 < y) (h : log x ≤ z * log y) : x ≤ y ^ z

Proof state:
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
⊢ x ≤ y ^ z

Tactic:
obtain hx | hx := le_or_lt x 0

Result:
case inl
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : x ≤ 0
⊢ x ≤ y ^ z

case inr
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : 0 < x
⊢ x ≤ y ^ z

Proof state:
case inl
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : x ≤ 0
⊢ x ≤ y ^ z

Tactic:
exact hx.trans (rpow_pos_of_pos hy _).le

Result:
no goals

Proof state:
case inr
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : 0 < x
⊢ x ≤ y ^ z

Tactic:
exact (le_rpow_iff_log_le hx hy).2 h

Result:
no goals
-- Mathlib/Order/PartialSups.lean
@[simp]
lemma upperBounds_range_partialSups (f : ι → α) :
    upperBounds (Set.range (partialSups f)) = upperBounds (Set.range f)

Proof state:
case h
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
a : α
⊢ a ∈ upperBounds (Set.range ⇑(partialSups f)) ↔ a ∈ upperBounds (Set.range f)

Tactic:
simp only [mem_upperBounds, Set.forall_mem_range, partialSups_le_iff]

Result:
case h
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
a : α
⊢ (∀ (i j : ι), j ≤ i → f j ≤ a) ↔ ∀ (i : ι), f i ≤ a

Proof state:
case h
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
a : α
⊢ (∀ (i j : ι), j ≤ i → f j ≤ a) ↔ ∀ (i : ι), f i ≤ a

Tactic:
exact ⟨fun h _ ↦ h _ _ le_rfl, fun h _ _ _ ↦ h _⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
⊢ upperBounds (Set.range ⇑(partialSups f)) = upperBounds (Set.range f)

Tactic:
ext a

Result:
case h
α : Type u_1
ι : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
a : α
⊢ a ∈ upperBounds (Set.range ⇑(partialSups f)) ↔ a ∈ upperBounds (Set.range f)