harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Image.lean
theorem mem_range_iff_mem_finset_range_of_mod_eq' [DecidableEq α] {f : ℕ → α} {a : α} {n : ℕ}
    (hn : 0 < n) (h : ∀ i, f (i % n) = f i) :
    a ∈ Set.range f ↔ a ∈ (Finset.range n).image fun i => f i

Proof state:
case mp.intro
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
hi : f i = a
⊢ a ∈ image (fun i => f i) (range n)

Tactic:
simp only [mem_image, exists_prop, mem_range]

Result:
case mp.intro
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
hi : f i = a
⊢ ∃ a_1 < n, f a_1 = a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ Set.range f ↔ a ∈ image (fun i => f i) (range n)

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ Set.range f → a ∈ image (fun i => f i) (range n)

case mpr
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ image (fun i => f i) (range n) → a ∈ Set.range f

Proof state:
case mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
left✝ : i < n
ha : f i = a
⊢ ∃ y, f y = a

Tactic:
exact ⟨i, ha⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ Set.range f → a ∈ image (fun i => f i) (range n)

Tactic:
rintro ⟨i, hi⟩

Result:
case mp.intro
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
hi : f i = a
⊢ a ∈ image (fun i => f i) (range n)

Proof state:
case mpr
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h✝ : ∀ (i : ℕ), f (i % n) = f i
h : ∃ a_1 < n, f a_1 = a
⊢ ∃ y, f y = a

Tactic:
rcases h with ⟨i, _, ha⟩

Result:
case mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
left✝ : i < n
ha : f i = a
⊢ ∃ y, f y = a

Proof state:
case mpr
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ image (fun i => f i) (range n) → a ∈ Set.range f

Tactic:
rintro h

Result:
case mpr
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h✝ : ∀ (i : ℕ), f (i % n) = f i
h : a ∈ image (fun i => f i) (range n)
⊢ a ∈ Set.range f

Proof state:
case mpr
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h✝ : ∀ (i : ℕ), f (i % n) = f i
h : a ∈ image (fun i => f i) (range n)
⊢ a ∈ Set.range f

Tactic:
simp only [mem_image, exists_prop, Set.mem_range, mem_range] at *

Result:
case mpr
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h✝ : ∀ (i : ℕ), f (i % n) = f i
h : ∃ a_1 < n, f a_1 = a
⊢ ∃ y, f y = a

Proof state:
case mp.intro
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
hi : f i = a
⊢ ∃ a_1 < n, f a_1 = a

Tactic:
exact ⟨i % n, Nat.mod_lt i hn, (rfl.congr hi).mp (h i)⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem eventually_pow_one_div_le (x : ℝ≥0) {y : ℝ≥0} (hy : 1 < y) :
    ∀ᶠ n : ℕ in atTop, x ^ (1 / n : ℝ) ≤ y

Proof state:
x y : ℝ≥0
hy : 1 < y
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y

Tactic:
obtain ⟨m, hm⟩ := add_one_pow_unbounded_of_pos x (tsub_pos_of_lt hy)

Result:
case intro
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < (y - 1 + 1) ^ m
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y

Proof state:
case intro
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
n : ℕ
hn : n ≥ m + 1
⊢ x ^ (1 / ↑n) ≤ y

Tactic:
simp only [one_div]

Result:
case intro
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
n : ℕ
hn : n ≥ m + 1
⊢ x ^ (↑n)⁻¹ ≤ y

Proof state:
case intro
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
n : ℕ
hn : n ≥ m + 1
⊢ x ^ (↑n)⁻¹ ≤ y

Tactic:
simpa only [NNReal.rpow_inv_le_iff (Nat.cast_pos.2 <| m.succ_pos.trans_le hn),
  NNReal.rpow_natCast] using hm.le.trans (pow_right_mono₀ hy.le (m.le_succ.trans hn))

Result:
no goals

Proof state:
case intro
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < (y - 1 + 1) ^ m
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y

Tactic:
rw [tsub_add_cancel_of_le hy.le] at hm

Result:
case intro
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y

Proof state:
case intro
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
⊢ ∀ᶠ (n : ℕ) in atTop, x ^ (1 / ↑n) ≤ y

Tactic:
refine eventually_atTop.2 ⟨m + 1, fun n hn => ?_⟩

Result:
case intro
x y : ℝ≥0
hy : 1 < y
m : ℕ
hm : x < y ^ m
n : ℕ
hn : n ≥ m + 1
⊢ x ^ (1 / ↑n) ≤ y
-- Mathlib/Data/Tree/Basic.lean
theorem traverse_pure (t : Tree α) {m : Type u → Type*} [Applicative m] [LawfulApplicative m] :
    t.traverse (pure : α → m α) = pure t

Proof state:
α : Type u
t : Tree α
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
⊢ traverse pure t = pure t

Tactic:
induction t with
| nil => rw [traverse]
| node v l r hl hr =>
  rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]

Result:
no goals

Proof state:
case node
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
v : α
l r : Tree α
hl : traverse pure l = pure l
hr : traverse pure r = pure r
⊢ traverse pure (node v l r) = pure (node v l r)

Tactic:
rw [traverse, hl, hr, map_pure, pure_seq, seq_pure, map_pure, map_pure]

Result:
no goals

Proof state:
case nil
α : Type u
m : Type u → Type u_1
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
⊢ traverse pure nil = pure nil

Tactic:
rw [traverse]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_toOuterMeasure_eq_toOuterMeasure_restrict (h : MeasurableSet s) :
    (μ.restrict s).toOuterMeasure = OuterMeasure.restrict s μ.toOuterMeasure

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
⊢ (μ.restrict s).toOuterMeasure = (OuterMeasure.restrict s) μ.toOuterMeasure

Tactic:
simp_rw [restrict, restrictₗ, liftLinear, LinearMap.coe_mk, AddHom.coe_mk,
  toMeasure_toOuterMeasure, OuterMeasure.restrict_trim h, μ.trimmed]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
theorem Measure.MeasureDense.nonempty' (h𝒜 : μ.MeasureDense 𝒜) :
    {s | s ∈ 𝒜 ∧ μ s ≠ ∞}.Nonempty

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
⊢ μ ∅ ≠ ⊤

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
⊢ 0 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : μ (∅ ∆ t) < ENNReal.ofReal 1
⊢ {s | s ∈ 𝒜 ∧ μ s ≠ ⊤}.Nonempty

Tactic:
refine ⟨t, ht, ?_⟩

Result:
case intro.intro
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : μ (∅ ∆ t) < ENNReal.ofReal 1
⊢ μ t ≠ ⊤

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
⊢ {s | s ∈ 𝒜 ∧ μ s ≠ ⊤}.Nonempty

Tactic:
rcases h𝒜.approx ∅ MeasurableSet.empty (by simp) 1 (by norm_num) with ⟨t, ht, hμt⟩

Result:
case intro.intro
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : μ (∅ ∆ t) < ENNReal.ofReal 1
⊢ {s | s ∈ 𝒜 ∧ μ s ≠ ⊤}.Nonempty

Proof state:
case h.e'_2.h.e'_6
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : μ (∅ ∆ t) < ENNReal.ofReal 1
⊢ t = ∅ ∆ t

Tactic:
rw [← bot_eq_empty, bot_symmDiff]

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : μ (∅ ∆ t) < ENNReal.ofReal 1
⊢ μ t ≠ ⊤

Tactic:
convert ne_top_of_lt hμt

Result:
case h.e'_2.h.e'_6
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : μ (∅ ∆ t) < ENNReal.ofReal 1
⊢ t = ∅ ∆ t
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem pentagon_inv_hom_hom_hom_hom :
    (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom =
      (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom = (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom

Tactic:
simp [← cancel_epi ((α_ W X Y).hom ▷ Z)]

Result:
no goals
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem toΓSpec_preimage_basicOpen_eq (r : Γ.obj (op X)) :
    X.toΓSpecFun ⁻¹' basicOpen r = SetLike.coe (X.toRingedSpace.basicOpen r)

Proof state:
case h
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x✝ : ↑X.toTopCat
⊢ X.toΓSpecFun x✝ ∈ basicOpen r ↔ x✝ ∈ X.toRingedSpace.basicOpen r

Tactic:
rw [X.toRingedSpace.mem_top_basicOpen]

Result:
case h
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x✝ : ↑X.toTopCat
⊢ X.toΓSpecFun x✝ ∈ basicOpen r ↔ IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.Γgerm x✝)) r)

Proof state:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ X.toΓSpecFun ⁻¹' ↑(basicOpen r) = ↑(X.toRingedSpace.basicOpen r)

Tactic:
ext

Result:
case h
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x✝ : ↑X.toTopCat
⊢ x✝ ∈ X.toΓSpecFun ⁻¹' ↑(basicOpen r) ↔ x✝ ∈ ↑(X.toRingedSpace.basicOpen r)

Proof state:
case h
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x✝ : ↑X.toTopCat
⊢ x✝ ∈ X.toΓSpecFun ⁻¹' ↑(basicOpen r) ↔ x✝ ∈ ↑(X.toRingedSpace.basicOpen r)

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

Result:
case h
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x✝ : ↑X.toTopCat
⊢ X.toΓSpecFun x✝ ∈ basicOpen r ↔ x✝ ∈ X.toRingedSpace.basicOpen r

Proof state:
case h
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
x✝ : ↑X.toTopCat
⊢ X.toΓSpecFun x✝ ∈ basicOpen r ↔ IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.Γgerm x✝)) r)

Tactic:
exact not_mem_prime_iff_unit_in_stalk ..

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem sieveOfSubfunctor_functorInclusion : sieveOfSubfunctor S.functorInclusion = S

Proof state:
case h.mp.intro.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f : Opposite.unop (Opposite.op Y✝) ⟶ X
hf : S.arrows f
⊢ S.arrows ↑⟨f, hf⟩

Tactic:
exact hf

Result:
no goals

Proof state:
case h.mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (∃ t, ↑t = f✝) → S.arrows f✝

Tactic:
rintro ⟨⟨f, hf⟩, rfl⟩

Result:
case h.mp.intro.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f : Opposite.unop (Opposite.op Y✝) ⟶ X
hf : S.arrows f
⊢ S.arrows ↑⟨f, hf⟩

Proof state:
case h.mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ S.arrows f✝ → ∃ t, ↑t = f✝

Tactic:
intro hf

Result:
case h.mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
hf : S.arrows f✝
⊢ ∃ t, ↑t = f✝

Proof state:
case h.mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
hf : S.arrows f✝
⊢ ∃ t, ↑t = f✝

Tactic:
exact ⟨⟨_, hf⟩, rfl⟩

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (∃ t, ↑t = f✝) ↔ S.arrows f✝

Tactic:
constructor

Result:
case h.mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (∃ t, ↑t = f✝) → S.arrows f✝

case h.mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ S.arrows f✝ → ∃ t, ↑t = f✝

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
⊢ sieveOfSubfunctor S.functorInclusion = S

Tactic:
ext

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (sieveOfSubfunctor S.functorInclusion).arrows f✝ ↔ S.arrows f✝

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (sieveOfSubfunctor S.functorInclusion).arrows f✝ ↔ S.arrows f✝

Tactic:
simp only [functorInclusion_app, sieveOfSubfunctor_apply]

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (∃ t, ↑t = f✝) ↔ S.arrows f✝
-- Mathlib/Order/WithBot.lean
@[simp, norm_cast] lemma coe_le_coe : (a : WithBot α) ≤ b ↔ a ≤ b

Proof state:
α : Type u_1
a b : α
inst✝ : LE α
⊢ ↑a ≤ ↑b ↔ a ≤ b

Tactic:
simp [le_def]

Result:
no goals
-- Mathlib/ModelTheory/DirectLimit.lean
theorem equiv_iff {x y : Σˣ f} {i : ι} (hx : x.1 ≤ i) (hy : y.1 ≤ i) :
    x ≈ y ↔ (f x.1 i hx) x.2 = (f y.1 i hy) y.2

Proof state:
case mk.mk.intro.intro.intro.intro.intro
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
j : ι
w✝¹ : fst✝¹ ≤ j
w✝ : fst✝ ≤ j
h✝ : (f fst✝¹ j w✝¹) snd✝¹ = (f fst✝ j w✝) snd✝
k : ι
ik : i ≤ k
jk : j ≤ k
h : (f j k jk) ((f fst✝¹ j w✝¹) snd✝¹) = (f j k jk) ((f fst✝ j w✝) snd✝)
⊢ (f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd = (f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd

Tactic:
apply (f i k ik).injective

Result:
case mk.mk.intro.intro.intro.intro.intro.a
L : Language
ι : Type v
inst✝³ : Preorder ι
G : ι → Type w
inst✝² : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : DirectedSystem G fun i j h => ⇑(f i j h)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
j : ι
w✝¹ : fst✝¹ ≤ j
w✝ : fst✝ ≤ j
h✝ : (f fst✝¹ j w✝¹) snd✝¹ = (f fst✝ j w✝) snd✝
k : ι
ik : i ≤ k
jk : j ≤ k
h : (f j k jk) ((f fst✝¹ j w✝¹) snd✝¹) = (f j k jk) ((f fst✝ j w✝) snd✝)
⊢ (f i k ik) ((f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd) = (f i k ik) ((f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd)
-- Mathlib/RingTheory/Smooth/Kaehler.lean
@[simp]
lemma tensorKaehlerQuotKerSqEquiv_tmul_D (s t) :
    tensorKaehlerQuotKerSqEquiv R P S (s ⊗ₜ .D _ _ (Ideal.Quotient.mk _ t)) = s ⊗ₜ .D _ _ t

Proof state:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
s : S
t : P
⊢ (tensorKaehlerQuotKerSqEquiv R P S)
      (s ⊗ₜ[P ⧸ RingHom.ker (algebraMap P S) ^ 2]
        (D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t)) =
    s ⊗ₜ[P] (D R P) t

Tactic:
show s • (derivationQuotKerSq R P S).liftKaehlerDifferential (.D _ _ (Ideal.Quotient.mk _ t)) = _

Result:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
s : S
t : P
⊢ s •
      (derivationQuotKerSq R P S).liftKaehlerDifferential
        ((D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t)) =
    s ⊗ₜ[P] (D R P) t

Proof state:
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
s : S
t : P
⊢ s •
      (derivationQuotKerSq R P S).liftKaehlerDifferential
        ((D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t)) =
    s ⊗ₜ[P] (D R P) t

Tactic:
simp [smul_tmul']

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsLittleO.trans_isBigOWith (hfg : f =o[l] g) (hgk : IsBigOWith c l g k) (hc : 0 < c) :
    f =o[l] k

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hgk : IsBigOWith c l g k
hc : 0 < c
hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f k

Tactic:
intro c' c'pos

Result:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hgk : IsBigOWith c l g k
hc : 0 < c
hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
c' : ℝ
c'pos : 0 < c'
⊢ IsBigOWith c' l f k

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hgk : IsBigOWith c l g k
hc : 0 < c
hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
c' : ℝ
c'pos : 0 < c'
⊢ IsBigOWith c' l f k

Tactic:
have : 0 < c' / c := div_pos c'pos hc

Result:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hgk : IsBigOWith c l g k
hc : 0 < c
hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
c' : ℝ
c'pos : 0 < c'
this : 0 < c' / c
⊢ IsBigOWith c' l f k

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hgk : IsBigOWith c l g k
hc : 0 < c
hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
c' : ℝ
c'pos : 0 < c'
this : 0 < c' / c
⊢ IsBigOWith c' l f k

Tactic:
exact ((hfg this).trans hgk this.le).congr_const (div_mul_cancel₀ _ hc.ne')

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hfg : f =o[l] g
hgk : IsBigOWith c l g k
hc : 0 < c
⊢ f =o[l] k

Tactic:
simp only [IsLittleO_def] at *

Result:
α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hgk : IsBigOWith c l g k
hc : 0 < c
hfg : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f k
-- Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean
@[to_additive]
lemma id_apply (A : ProfiniteGrp.{u}) (a : A) :
    (𝟙 A : A ⟶ A) a = a

Proof state:
A : ProfiniteGrp.{u}
a : ↑A.toProfinite.toTop
⊢ (Hom.hom (𝟙 A)) a = a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_extract {hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) :
    (extractLsb hi lo x)[i] = getLsbD x (lo+i)

Proof state:
n hi lo : Nat
x : BitVec n
i : Nat
h : i < hi - lo + 1
⊢ (extractLsb hi lo x)[i] = x.getLsbD (lo + i)

Tactic:
simp [getElem_eq_testBit_toNat, getLsbD, h]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem map_symm_map (I : FractionalIdeal S P') (g : P ≃ₐ[R] P') :
    (I.map (g.symm : P' →ₐ[R] P)).map (g : P →ₐ[R] P') = I

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
I : FractionalIdeal S P'
g : P ≃ₐ[R] P'
⊢ map (↑g) (map (↑g.symm) I) = I

Tactic:
rw [← map_comp, g.comp_symm, map_id]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem dropn_cons (a : α) (s) (n) : drop (cons a s) (n + 1) = drop s n

Proof state:
case succ
α : Type u
a : α
s : WSeq α
n : ℕ
n_ih : (cons a s).drop (n + 1) = s.drop n
⊢ (cons a s).drop (n + 1 + 1) = s.drop (n + 1)

Tactic:
simp [drop, ← n_ih]

Result:
no goals

Proof state:
α : Type u
a : α
s : WSeq α
n : ℕ
⊢ (cons a s).drop (n + 1) = s.drop n

Tactic:
induction n with
| zero => simp [drop]
| succ n n_ih =>
  simp [drop, ← n_ih]

Result:
no goals

Proof state:
case zero
α : Type u
a : α
s : WSeq α
⊢ (cons a s).drop (0 + 1) = s.drop 0

Tactic:
simp [drop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_dropLast (xs : List α) : xs.dropLast.head? = if 1 < xs.length then xs.head? else none

Proof state:
case nil
α : Type u_1
⊢ [].dropLast.head? = if 1 < [].length then [].head? else none

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
xs : List α
⊢ xs.dropLast.head? = if 1 < xs.length then xs.head? else none

Tactic:
cases xs with
| nil => rfl
| cons x xs =>
  cases xs with
  | nil => rfl
  | cons y ys => simp [Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
x : α
⊢ [x].dropLast.head? = if 1 < [x].length then [x].head? else none

Tactic:
rfl

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
x y : α
ys : List α
⊢ (x :: y :: ys).dropLast.head? = if 1 < (x :: y :: ys).length then (x :: y :: ys).head? else none

Tactic:
simp [Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
case cons
α : Type u_1
x : α
xs : List α
⊢ (x :: xs).dropLast.head? = if 1 < (x :: xs).length then (x :: xs).head? else none

Tactic:
cases xs with
| nil => rfl
| cons y ys => simp [Nat.succ_lt_succ_iff]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem nim_equiv_iff_eq {o₁ o₂ : Ordinal} : (nim o₁ ≈ nim o₂) ↔ o₁ = o₂

Proof state:
o₁ o₂ : Ordinal.{u_1}
⊢ nim o₁ ≈ nim o₂ ↔ o₁ = o₂

Tactic:
rw [Impartial.equiv_iff_add_equiv_zero, nim_add_equiv_zero_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem toPlus_mk {X : C} {P : Cᵒᵖ ⥤ D} (S : J.Cover X) (x : ToType (P.obj (op X))) :
    (J.toPlus P).app _ x = mk (Meq.mk S x)

Proof state:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (S.index P) (multiequalizer (⊤.index P)) (fun I => Multiequalizer.ι (⊤.index P) (I.map e))
          ⋯))
      ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯)) x) =
    (Meq.equiv P S).symm (Meq.mk S x)

Tactic:
apply Concrete.multiequalizer_ext (C := D)

Result:
case h.h
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{max v u, w} D
FD : D → D → Type u_1
CD : D → Type (max v u)
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : PreservesLimits (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : ToType (P.obj (op X))
e : S ⟶ ⊤ := homOfLE ⋯
⊢ ∀ (t : S.shape.L),
    (ConcreteCategory.hom (Multiequalizer.ι (S.index P) t))
        ((ConcreteCategory.hom
            (Multiequalizer.lift (S.index P) (multiequalizer (⊤.index P))
              (fun I => Multiequalizer.ι (⊤.index P) (I.map e)) ⋯))
          ((ConcreteCategory.hom (Multiequalizer.lift (⊤.index P) (P.obj (op X)) (fun I => P.map I.f.op) ⋯)) x)) =
      (ConcreteCategory.hom (Multiequalizer.ι (S.index P) t)) ((Meq.equiv P S).symm (Meq.mk S x))
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_countable' [Countable α] [MeasurableSingletonClass α] (f : α → ℝ≥0∞) :
    ∫⁻ a, f a ∂μ = ∑' a, f a * μ {a}

Proof state:
case e_f.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ ∫⁻ (a : α), f a ∂μ {a} • dirac a = f a * μ {a}

Tactic:
rw [lintegral_smul_measure, lintegral_dirac, mul_comm]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α), f a ∂μ = ∑' (a : α), f a * μ {a}

Tactic:
conv_lhs => rw [← sum_smul_dirac μ, lintegral_sum_measure]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ ∑' (i : α), ∫⁻ (a : α), f a ∂μ {i} • dirac i = ∑' (a : α), f a * μ {a}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
⊢ ∑' (i : α), ∫⁻ (a : α), f a ∂μ {i} • dirac i = ∑' (a : α), f a * μ {a}

Tactic:
congr 1 with a : 1

Result:
case e_f.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ ∫⁻ (a : α), f a ∂μ {a} • dirac a = f a * μ {a}