harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Relation.lean
@[simp] lemma transGen_reflGen : TransGen (ReflGen r) = ReflTransGen r

Proof state:
case h.h.a.refine_2.inl
α : Type u_1
r : α → α → Prop
y : α
h : ReflTransGen r y y
⊢ TransGen (ReflGen r) y y

Tactic:
exact .single .refl

Result:
no goals

Proof state:
case h.h.a.refine_2.inr
α : Type u_1
r : α → α → Prop
x y : α
h✝ : ReflTransGen r x y
h : TransGen r x y
⊢ TransGen (ReflGen r) x y

Tactic:
exact TransGen.mono (fun _ _ ↦ .single) h

Result:
no goals

Proof state:
case h.h.a.refine_2
α : Type u_1
r : α → α → Prop
x y : α
h : ReflTransGen r x y
⊢ TransGen (ReflGen r) x y

Tactic:
obtain (rfl | h) := reflTransGen_iff_eq_or_transGen.mp h

Result:
case h.h.a.refine_2.inl
α : Type u_1
r : α → α → Prop
y : α
h : ReflTransGen r y y
⊢ TransGen (ReflGen r) y y

case h.h.a.refine_2.inr
α : Type u_1
r : α → α → Prop
x y : α
h✝ : ReflTransGen r x y
h : TransGen r x y
⊢ TransGen (ReflGen r) x y

Proof state:
case h.h.a
α : Type u_1
r : α → α → Prop
x y : α
⊢ TransGen (ReflGen r) x y ↔ ReflTransGen r x y

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case h.h.a.refine_1
α : Type u_1
r : α → α → Prop
x y : α
h : TransGen (ReflGen r) x y
⊢ ReflTransGen r x y

case h.h.a.refine_2
α : Type u_1
r : α → α → Prop
x y : α
h : ReflTransGen r x y
⊢ TransGen (ReflGen r) x y

Proof state:
α : Type u_1
r : α → α → Prop
⊢ TransGen (ReflGen r) = ReflTransGen r

Tactic:
ext x y

Result:
case h.h.a
α : Type u_1
r : α → α → Prop
x y : α
⊢ TransGen (ReflGen r) x y ↔ ReflTransGen r x y

Proof state:
case h.h.a.refine_1
α : Type u_1
r : α → α → Prop
x y : α
h : TransGen (ReflGen r) x y
⊢ ReflTransGen r x y

Tactic:
simpa [reflTransGen_idem]
  using TransGen.to_reflTransGen <| TransGen.mono (fun _ _ ↦ ReflGen.to_reflTransGen) h

Result:
no goals
-- Mathlib/Data/Finsupp/AList.lean
theorem mem_toAlist {f : α →₀ M} {x : α} : x ∈ f.toAList ↔ f x ≠ 0

Proof state:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ x ∈ f.toAList ↔ f x ≠ 0

Tactic:
rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
x : α
⊢ x ∈ f.toAList ↔ f x ≠ 0

Tactic:
classical rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem length_tails (l : List α) : length (tails l) = length l + 1

Proof state:
α : Type u_1
l : List α
⊢ l.tails.length = l.length + 1

Tactic:
induction' l with x l IH

Result:
case nil
α : Type u_1
⊢ [].tails.length = [].length + 1

case cons
α : Type u_1
x : α
l : List α
IH : l.tails.length = l.length + 1
⊢ (x :: l).tails.length = (x :: l).length + 1

Proof state:
case nil
α : Type u_1
⊢ [].tails.length = [].length + 1

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
x : α
l : List α
IH : l.tails.length = l.length + 1
⊢ (x :: l).tails.length = (x :: l).length + 1

Tactic:
simpa using IH

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
lemma exists_mem_ne (hs : 1 < #s) (a : α) : ∃ b ∈ s, b ≠ a

Proof state:
α : Type u_1
s : Finset α
hs : 1 < #s
a : α
⊢ ∃ b ∈ s, b ≠ a

Tactic:
have : Nonempty α := ⟨a⟩

Result:
α : Type u_1
s : Finset α
hs : 1 < #s
a : α
this : Nonempty α
⊢ ∃ b ∈ s, b ≠ a

Proof state:
α : Type u_1
s : Finset α
hs : 1 < #s
a : α
this✝ : Nonempty α
this : ∀ b ∈ s, b = a
⊢ False

Tactic:
exact hs.not_le (card_le_one_iff_subset_singleton.2 ⟨a, subset_singleton_iff'.2 this⟩)

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
hs : 1 < #s
a : α
this : Nonempty α
⊢ ∃ b ∈ s, b ≠ a

Tactic:
by_contra!

Result:
α : Type u_1
s : Finset α
hs : 1 < #s
a : α
this✝ : Nonempty α
this : ∀ b ∈ s, b = a
⊢ False
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem tag_index_eq_self_of_mem_smul_span {x : ι → ℝ} (hx : x ∈ (n : ℝ)⁻¹ • L) :
    tag n (index n x) = x

Proof state:
case h.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
x : ι → ℝ
hx : ∀ (i : ι), ↑n * x i ∈ Set.range ⇑(algebraMap ℤ ℝ)
i : ι
a : ℤ
ha : ↑a = ↑n * x i
⊢ tag n (index n x) i = x i

Tactic:
rwa [tag_apply, index_apply, Int.cast_sub, Int.cast_one, sub_add_cancel, ← ha, Int.ceil_intCast,
  div_eq_iff (NeZero.ne _), mul_comm]

Result:
no goals

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
x : ι → ℝ
hx : x ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))
⊢ tag n (index n x) = x

Tactic:
rw [mem_smul_span_iff] at hx

Result:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
x : ι → ℝ
hx : ∀ (i : ι), ↑n * x i ∈ Set.range ⇑(algebraMap ℤ ℝ)
⊢ tag n (index n x) = x

Proof state:
case h
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
x : ι → ℝ
hx : ∀ (i : ι), ↑n * x i ∈ Set.range ⇑(algebraMap ℤ ℝ)
i : ι
⊢ tag n (index n x) i = x i

Tactic:
obtain ⟨a, ha⟩ : ∃ a : ℤ, a = n * x i := hx i

Result:
case h.intro
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
x : ι → ℝ
hx : ∀ (i : ι), ↑n * x i ∈ Set.range ⇑(algebraMap ℤ ℝ)
i : ι
a : ℤ
ha : ↑a = ↑n * x i
⊢ tag n (index n x) i = x i

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
x : ι → ℝ
hx : ∀ (i : ι), ↑n * x i ∈ Set.range ⇑(algebraMap ℤ ℝ)
⊢ tag n (index n x) = x

Tactic:
ext i

Result:
case h
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
x : ι → ℝ
hx : ∀ (i : ι), ↑n * x i ∈ Set.range ⇑(algebraMap ℤ ℝ)
i : ι
⊢ tag n (index n x) i = x i
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem moebius_apply_prime_pow {p k : ℕ} (hp : p.Prime) (hk : k ≠ 0) :
    μ (p ^ k) = if k = 1 then -1 else 0

Proof state:
case neg
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree (p ^ k)

Tactic:
rw [squarefree_pow_iff hp.ne_one hk, not_and_or]

Result:
case neg
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree p ∨ ¬k = 1

Proof state:
case neg
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree p ∨ ¬k = 1

Tactic:
exact Or.inr h

Result:
no goals

Proof state:
case pos
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : k = 1
⊢ μ (p ^ k) = -1

Tactic:
rw [h, pow_one, moebius_apply_prime hp]

Result:
no goals

Proof state:
case neg
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ μ (p ^ k) = 0

Tactic:
rw [moebius_eq_zero_of_not_squarefree]

Result:
case neg
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ ¬Squarefree (p ^ k)

Proof state:
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
⊢ μ (p ^ k) = if k = 1 then -1 else 0

Tactic:
split_ifs with h

Result:
case pos
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : k = 1
⊢ μ (p ^ k) = -1

case neg
p k : ℕ
hp : Nat.Prime p
hk : k ≠ 0
h : ¬k = 1
⊢ μ (p ^ k) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attach_append (xs : Vector α n) (ys : Vector α m) :
    (xs ++ ys).attach = xs.attach.map (fun ⟨x, h⟩ => (⟨x, mem_append_left ys h⟩ : { x // x ∈ xs ++ ys })) ++
      ys.attach.map (fun ⟨y, h⟩ => (⟨y, mem_append_right xs h⟩ : { y // y ∈ xs ++ ys }))

Proof state:
case mk
α : Type u_1
m : Nat
ys : Vector α m
xs : Array α
⊢ ({ toArray := xs, size_toArray := ⋯ } ++ ys).attach =
    map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        { toArray := xs, size_toArray := ⋯ }.attach ++
      map
        (fun x =>
          match x with
          | ⟨y, h⟩ => ⟨y, ⋯⟩)
        ys.attach

Tactic:
rcases ys with ⟨ys, rfl⟩

Result:
case mk.mk
α : Type u_1
xs ys : Array α
⊢ ({ toArray := xs, size_toArray := ⋯ } ++ { toArray := ys, size_toArray := ⋯ }).attach =
    map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        { toArray := xs, size_toArray := ⋯ }.attach ++
      map
        (fun x =>
          match x with
          | ⟨y, h⟩ => ⟨y, ⋯⟩)
        { toArray := ys, size_toArray := ⋯ }.attach

Proof state:
α : Type u_1
n m : Nat
xs : Vector α n
ys : Vector α m
⊢ (xs ++ ys).attach =
    map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        xs.attach ++
      map
        (fun x =>
          match x with
          | ⟨y, h⟩ => ⟨y, ⋯⟩)
        ys.attach

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
ys : Vector α m
xs : Array α
⊢ ({ toArray := xs, size_toArray := ⋯ } ++ ys).attach =
    map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        { toArray := xs, size_toArray := ⋯ }.attach ++
      map
        (fun x =>
          match x with
          | ⟨y, h⟩ => ⟨y, ⋯⟩)
        ys.attach

Proof state:
case mk.mk
α : Type u_1
xs ys : Array α
⊢ ({ toArray := xs, size_toArray := ⋯ } ++ { toArray := ys, size_toArray := ⋯ }).attach =
    map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        { toArray := xs, size_toArray := ⋯ }.attach ++
      map
        (fun x =>
          match x with
          | ⟨y, h⟩ => ⟨y, ⋯⟩)
        { toArray := ys, size_toArray := ⋯ }.attach

Tactic:
simp [Array.map_attachWith]

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
lemma span_selfAdjoint : span ℂ (selfAdjoint A : Set A) = ⊤

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
⊢ span ℂ ↑(selfAdjoint A) = ⊤

Tactic:
refine eq_top_iff'.mpr fun x ↦ ?_

Result:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
⊢ x ∈ span ℂ ↑(selfAdjoint A)

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
⊢ ↑(ℜ x) + I • ↑(ℑ x) ∈ span ℂ ↑(selfAdjoint A)

Tactic:
exact add_mem (subset_span (ℜ x).property) <|
  SMulMemClass.smul_mem _ <| subset_span (ℑ x).property

Result:
no goals

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
⊢ x ∈ span ℂ ↑(selfAdjoint A)

Tactic:
rw [← realPart_add_I_smul_imaginaryPart x]

Result:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
⊢ ↑(ℜ x) + I • ↑(ℑ x) ∈ span ℂ ↑(selfAdjoint A)
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma XYIdeal_eq₁ (x y L : R) : XYIdeal W x (C y) = XYIdeal W x (linePolynomial x y L)

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
x y L : R
⊢ XYIdeal W x (C y) = XYIdeal W x (linePolynomial x y L)

Tactic:
simp only [XYIdeal, XClass, YClass, linePolynomial]

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
x y L : R
⊢ span {(mk W) (C (X - C x)), (mk W) (Y - C (C y))} =
    span {(mk W) (C (X - C x)), (mk W) (Y - C (C L * (X - C x) + C y))}

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
x y L : R
⊢ Y - C (C y) + (C X - C (C x)) * -C (C L) = Y - (C (C L) * (C X - C (C x)) + C (C y))

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
x y L : R
⊢ span {(mk W) (C (X - C x)), (mk W) (Y - C (C y) + C (X - C x) * C (C (-L)))} =
    span {(mk W) (C (X - C x)), (mk W) (Y - C (C L * (X - C x) + C y))}

Tactic:
apply congr_arg (_ ∘ _ ∘ _ ∘ _)

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
x y L : R
⊢ Y - C (C y) + C (X - C x) * C (C (-L)) = Y - C (C L * (X - C x) + C y)

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
x y L : R
⊢ span {(mk W) (C (X - C x)), (mk W) (Y - C (C y))} =
    span {(mk W) (C (X - C x)), (mk W) (Y - C (C L * (X - C x) + C y))}

Tactic:
rw [← span_pair_add_mul_right <| mk W <| C <| C <| -L, ← _root_.map_mul, ← map_add]

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
x y L : R
⊢ span {(mk W) (C (X - C x)), (mk W) (Y - C (C y) + C (X - C x) * C (C (-L)))} =
    span {(mk W) (C (X - C x)), (mk W) (Y - C (C L * (X - C x) + C y))}

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
x y L : R
⊢ Y - C (C y) + C (X - C x) * C (C (-L)) = Y - C (C L * (X - C x) + C y)

Tactic:
C_simp

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
x y L : R
⊢ Y - C (C y) + (C X - C (C x)) * -C (C L) = Y - (C (C L) * (C X - C (C x)) + C (C y))
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
lemma tendsto_eapprox {f : α → ℝ≥0∞} (hf_meas : Measurable f) (a : α) :
    Tendsto (fun n ↦ eapprox f n a) atTop (𝓝 (f a))

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf_meas : Measurable f
a : α
⊢ Tendsto (fun n => (eapprox f n) a) atTop (𝓝 (⨆ i, (eapprox f i) a))

Tactic:
exact tendsto_atTop_iSup fun _ _ hnm ↦ monotone_eapprox f hnm a

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf_meas : Measurable f
a : α
⊢ Tendsto (fun n => (eapprox f n) a) atTop (𝓝 (f a))

Tactic:
nth_rw 2 [← iSup_coe_eapprox hf_meas]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf_meas : Measurable f
a : α
⊢ Tendsto (fun n => (eapprox f n) a) atTop (𝓝 ((⨆ n, ⇑(eapprox f n)) a))

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf_meas : Measurable f
a : α
⊢ Tendsto (fun n => (eapprox f n) a) atTop (𝓝 ((⨆ n, ⇑(eapprox f n)) a))

Tactic:
rw [iSup_apply]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ≥0∞
hf_meas : Measurable f
a : α
⊢ Tendsto (fun n => (eapprox f n) a) atTop (𝓝 (⨆ i, (eapprox f i) a))
-- Mathlib/Order/Minimal.lean
theorem minimal_mem_image_monotone (hf : ∀ ⦃x y⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y))
    (hx : Minimal (· ∈ s) x) : Minimal (· ∈ f '' s) (f x)

Proof state:
case intro.intro
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x => x ∈ s) x
y : α
hy : y ∈ s
⊢ f y ≤ f x → f x ≤ f y

Tactic:
rw [hf hx.prop hy, hf hy hx.prop]

Result:
case intro.intro
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x => x ∈ s) x
y : α
hy : y ∈ s
⊢ y ≤ x → x ≤ y

Proof state:
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x => x ∈ s) x
⊢ ∀ ⦃y : β⦄, (fun x => x ∈ f '' s) y → y ≤ f x → f x ≤ y

Tactic:
rintro _ ⟨y, hy, rfl⟩

Result:
case intro.intro
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x => x ∈ s) x
y : α
hy : y ∈ s
⊢ f y ≤ f x → f x ≤ f y

Proof state:
case intro.intro
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x => x ∈ s) x
y : α
hy : y ∈ s
⊢ y ≤ x → x ≤ y

Tactic:
exact hx.le_of_le hy

Result:
no goals

Proof state:
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x => x ∈ s) x
⊢ Minimal (fun x => x ∈ f '' s) (f x)

Tactic:
refine ⟨mem_image_of_mem f hx.prop, ?_⟩

Result:
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
f : α → β
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
hx : Minimal (fun x => x ∈ s) x
⊢ ∀ ⦃y : β⦄, (fun x => x ∈ f '' s) y → y ≤ f x → f x ≤ y
-- Mathlib/Data/Finset/NAry.lean
@[simp (default + 1)] -- otherwise `simp` doesn't use `forall_mem_image₂`
lemma le_inf'_image₂ {g : γ → δ} {a : δ} (h : (image₂ f s t).Nonempty) :
    a ≤ inf' (image₂ f s t) h g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeInf δ
g : γ → δ
a : δ
h : (image₂ f s t).Nonempty
⊢ a ≤ (image₂ f s t).inf' h g ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ g (f x y)

Tactic:
rw [le_inf'_iff, forall_mem_image₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem coordinate_eval_8 :
    (coordinate 8).eval
      (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: t)) = a8

Proof state:
a0 a1 a2 a3 a4 a5 a6 a7 a8 : Int
t : List Int
⊢ (coordinate 8).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: a8 :: t)) = a8

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem red_invRev_iff : Red (invRev L₁) (invRev L₂) ↔ Red L₁ L₂ :=
  ⟨fun h => by simpa only [invRev_invRev] using h.invRev, fun h => h.invRev⟩

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
h : Red (invRev L₁) (invRev L₂)
⊢ Red L₁ L₂

Tactic:
simpa only [invRev_invRev] using h.invRev

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem digits_lt_base {b m d : ℕ} (hb : 1 < b) (hd : d ∈ digits b m) : d < b

Proof state:
b m d : ℕ
hb : 1 < b
hd : d ∈ b.digits m
⊢ d < b

Tactic:
rcases b with (_ | _ | b) <;> try simp_all

Result:
case succ.succ
m d b : ℕ
hd : d ∈ (b + 1 + 1).digits m
⊢ d < b + 1 + 1

Proof state:
case succ.succ
m d b : ℕ
hb : 1 < b + 1 + 1
hd : d ∈ (b + 1 + 1).digits m
⊢ d < b + 1 + 1

Tactic:
simp_all

Result:
case succ.succ
m d b : ℕ
hd : d ∈ (b + 1 + 1).digits m
⊢ d < b + 1 + 1

Proof state:
case succ.succ
m d b : ℕ
hd : d ∈ (b + 1 + 1).digits m
⊢ d < b + 1 + 1

Tactic:
exact digits_lt_base' hd

Result:
no goals
-- Mathlib/Data/PNat/Xgcd.lean
theorem reduce_b {u : XgcdType} (h : u.r ≠ 0) : u.reduce = u.step.reduce.flip

Proof state:
u : XgcdType
h : u.r ≠ 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.step.reduce.flip

Tactic:
exact if_neg h

Result:
no goals

Proof state:
u : XgcdType
h : u.r ≠ 0
⊢ u.reduce = u.step.reduce.flip

Tactic:
rw [reduce]

Result:
u : XgcdType
h : u.r ≠ 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.step.reduce.flip
-- Mathlib/Logic/ExistsUnique.lean
theorem existsUnique_eq {a' : α} : ∃! a, a = a'

Proof state:
α : Sort u_1
a' : α
⊢ ∃! a, a = a'

Tactic:
simp only [eq_comm, ExistsUnique, and_self, forall_eq', exists_eq']

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem exists_nat_eq_of_le_nat {c : Cardinal} {n : ℕ} (h : c ≤ n) : ∃ m, m ≤ n ∧ c = m

Proof state:
c : Cardinal.{u_1}
n : ℕ
h : c ≤ ↑n
⊢ ∃ m ≤ n, c = ↑m

Tactic:
lift c to ℕ using h.trans_lt (nat_lt_aleph0 _)

Result:
case intro
n c : ℕ
h : ↑c ≤ ↑n
⊢ ∃ m ≤ n, ↑c = ↑m

Proof state:
case intro
n c : ℕ
h : ↑c ≤ ↑n
⊢ ∃ m ≤ n, ↑c = ↑m

Tactic:
exact ⟨c, mod_cast h, rfl⟩

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
theorem Asymptotics.IsBigO.trans_tendsto_norm_atTop {α : Type*} {u v : α → 𝕜} {l : Filter α}
    (huv : u =O[l] v) (hu : Tendsto (fun x => ‖u x‖) l atTop) :
    Tendsto (fun x => ‖v x‖) l atTop

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : c > 0
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
⊢ Tendsto (fun x => ‖v x‖) l atTop

Tactic:
convert Tendsto.atTop_div_const hc (tendsto_atTop_mono' l hcuv hu)

Result:
case h.e'_3.h
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : c > 0
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
x✝ : α
⊢ ‖v x✝‖ = c * ‖v x✝‖ / c

Proof state:
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
⊢ Tendsto (fun x => ‖v x‖) l atTop

Tactic:
rcases huv.exists_pos with ⟨c, hc, hcuv⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : c > 0
hcuv : IsBigOWith c l u v
⊢ Tendsto (fun x => ‖v x‖) l atTop

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : c > 0
hcuv : IsBigOWith c l u v
⊢ Tendsto (fun x => ‖v x‖) l atTop

Tactic:
rw [IsBigOWith] at hcuv

Result:
case intro.intro
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : c > 0
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
⊢ Tendsto (fun x => ‖v x‖) l atTop

Proof state:
case h.e'_3.h
𝕜 : Type u_1
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : c > 0
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
x✝ : α
⊢ ‖v x✝‖ = c * ‖v x✝‖ / c

Tactic:
rw [mul_div_cancel_left₀ _ hc.ne.symm]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma even_xor_odd' (n : ℕ) : ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1)

Proof state:
case h
k : ℕ
⊢ Xor' (k + k = 2 * k) (k + k = 2 * k + 1)

Tactic:
simpa only [← two_mul, eq_self_iff_true, xor_true] using (succ_ne_self (2 * k)).symm

Result:
no goals

Proof state:
case h
k : ℕ
⊢ Xor' (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)

Tactic:
simpa only [xor_true, xor_comm] using (succ_ne_self _)

Result:
no goals

Proof state:
n : ℕ
⊢ ∃ k, Xor' (n = 2 * k) (n = 2 * k + 1)

Tactic:
obtain ⟨k, rfl⟩ | ⟨k, rfl⟩ := even_or_odd n <;> use k

Result:
case h
k : ℕ
⊢ Xor' (k + k = 2 * k) (k + k = 2 * k + 1)

case h
k : ℕ
⊢ Xor' (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_norm_eq_lintegral_enorm {P : Type*} [NormedAddCommGroup P] {f : α → P}
    (hf : AEStronglyMeasurable f μ) : ∫ x, ‖f x‖ ∂μ = (∫⁻ x, ‖f x‖ₑ ∂μ).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : α), ‖f x‖ ∂μ = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae _ hf.norm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal

α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ 0 ≤ᶠ[ae μ] fun x => ‖f x‖

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal = (∫⁻ (x : α), ‖f x‖ₑ ∂μ).toReal

Tactic:
simp_rw [ofReal_norm_eq_enorm]

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ ∀ (a : α), 0 a ≤ ‖f a‖

Tactic:
simp_rw [Pi.zero_apply, norm_nonneg, imp_true_iff]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ 0 ≤ᶠ[ae μ] fun x => ‖f x‖

Tactic:
filter_upwards

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
P : Type u_7
inst✝ : NormedAddCommGroup P
f : α → P
hf : AEStronglyMeasurable f μ
⊢ ∀ (a : α), 0 a ≤ ‖f a‖
-- Mathlib/FieldTheory/Perfect.lean
theorem roots_X_pow_char_sub_C_pow {y : R} {m : ℕ} :
    ((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
m : ℕ
H : ((X ^ p ^ 1 - C y) ^ m).roots = (m * p ^ 1) • {(iterateFrobeniusEquiv R p 1).symm y}
⊢ ((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}

Tactic:
rwa [pow_one, iterateFrobeniusEquiv_one] at H

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
m : ℕ
⊢ ((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}

Tactic:
have H := roots_X_pow_char_pow_sub_C_pow (p := p) (n := 1) (y := y) (m := m)

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
m : ℕ
H : ((X ^ p ^ 1 - C y) ^ m).roots = (m * p ^ 1) • {(iterateFrobeniusEquiv R p 1).symm y}
⊢ ((X ^ p - C y) ^ m).roots = (m * p) • {(frobeniusEquiv R p).symm y}