harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem xor_append {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
    (x₁ ++ y₁) ^^^ (x₂ ++ y₂) = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂)

Proof state:
case pred
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
i : Nat
a✝ : i < w + v
⊢ (x₁ ++ y₁ ^^^ x₂ ++ y₂).getLsbD i = if i < v then (y₁ ^^^ y₂).getLsbD i else (x₁ ^^^ x₂).getLsbD (i - v)

Tactic:
split <;> simp [getLsbD_append, *]

Result:
no goals

Proof state:
case pred
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
i : Nat
a✝ : i < w + v
⊢ (x₁ ++ y₁ ^^^ x₂ ++ y₂).getLsbD i = ((x₁ ^^^ x₂) ++ (y₁ ^^^ y₂)).getLsbD i

Tactic:
simp only [getLsbD_append, cond_eq_if]

Result:
case pred
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
i : Nat
a✝ : i < w + v
⊢ (x₁ ++ y₁ ^^^ x₂ ++ y₂).getLsbD i = if i < v then (y₁ ^^^ y₂).getLsbD i else (x₁ ^^^ x₂).getLsbD (i - v)

Proof state:
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
⊢ x₁ ++ y₁ ^^^ x₂ ++ y₂ = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂)

Tactic:
ext i

Result:
case pred
w v : Nat
x₁ x₂ : BitVec w
y₁ y₂ : BitVec v
i : Nat
a✝ : i < w + v
⊢ (x₁ ++ y₁ ^^^ x₂ ++ y₂).getLsbD i = ((x₁ ^^^ x₂) ++ (y₁ ^^^ y₂)).getLsbD i
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem map_comap (μ : Measure β) : (comap f μ).map f = μ.restrict (range f)

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
⊢ Measure.map f (Measure.comap f μ) = μ.restrict (range f)

Tactic:
ext1 t ht

Result:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
t : Set β
ht : MeasurableSet t
⊢ (Measure.map f (Measure.comap f μ)) t = (μ.restrict (range f)) t

Proof state:
case h
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
t : Set β
ht : MeasurableSet t
⊢ (Measure.map f (Measure.comap f μ)) t = (μ.restrict (range f)) t

Tactic:
rw [hf.map_apply, comap_apply f hf.injective hf.measurableSet_image' _ (hf.measurable ht),
  image_preimage_eq_inter_range, Measure.restrict_apply ht]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_congr_ae {f g : α → ℝ≥0∞} (h : f =ᵐ[μ] g) :
    μ.withDensity f = μ.withDensity g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity f) s = (μ.withDensity g) s

Tactic:
rw [withDensity_apply _ hs, withDensity_apply _ hs]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
⊢ μ.withDensity f = μ.withDensity g

Tactic:
refine Measure.ext fun s hs => ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity f) s = (μ.withDensity g) s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ

Tactic:
exact lintegral_congr_ae (ae_restrict_of_ae h)

Result:
no goals
-- Mathlib/Data/List/TakeDrop.lean
theorem span_eq_takeWhile_dropWhile (l : List α) : span p l = (takeWhile p l, dropWhile p l)

Proof state:
α : Type u
p : α → Bool
l : List α
⊢ span p l = (takeWhile p l, dropWhile p l)

Tactic:
simpa using span.loop_eq_take_drop p l []

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem exists_mem_iff_getElem {l : List α} {p : α → Prop} :
    (∃ x ∈ l, p x) ↔ ∃ (i : ℕ) (_ : i < l.length), p l[i]

Proof state:
α : Type u
l : List α
p : α → Prop
⊢ (∃ x, (∃ i h, l[i] = x) ∧ p x) ↔ ∃ i x, p l[i]

Tactic:
exact ⟨fun ⟨_x, ⟨i, hi, hix⟩, hxp⟩ ↦ ⟨i, hi, hix ▸ hxp⟩, fun ⟨i, hi, hp⟩ ↦ ⟨_, ⟨i, hi, rfl⟩, hp⟩⟩

Result:
no goals

Proof state:
α : Type u
l : List α
p : α → Prop
⊢ (∃ x, x ∈ l ∧ p x) ↔ ∃ i x, p l[i]

Tactic:
simp only [mem_iff_getElem]

Result:
α : Type u
l : List α
p : α → Prop
⊢ (∃ x, (∃ i h, l[i] = x) ∧ p x) ↔ ∃ i x, p l[i]
-- Mathlib/Algebra/Module/SpanRank.lean
/-- For a finitely generated submodule, its spanRank is less than or equal to a cardinal `a`
  if and only if there is a generating subset with cardinality less than or equal to `a`. -/
lemma FG.spanRank_le_iff_exists_span_set_card_le (p : Submodule R M) {a : Cardinal} :
    p.spanRank ≤ a ↔ ∃ s : Set M, #s ≤ a ∧ span R s = p

Proof state:
case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{u}
⊢ (∃ s, #↑s ≤ a ∧ span R s = p) → p.spanRank ≤ a

Tactic:
exact (fun ⟨s, ⟨hs₁, hs₂⟩⟩ ↦ hs₂.symm ▸ (le_trans (spanRank_span_le_card s) hs₁))

Result:
no goals

Proof state:
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{u}
⊢ p.spanRank ≤ a ↔ ∃ s, #↑s ≤ a ∧ span R s = p

Tactic:
constructor

Result:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{u}
⊢ p.spanRank ≤ a → ∃ s, #↑s ≤ a ∧ span R s = p

case mpr
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{u}
⊢ (∃ s, #↑s ≤ a ∧ span R s = p) → p.spanRank ≤ a

Proof state:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{u}
⊢ p.spanRank ≤ a → ∃ s, #↑s ≤ a ∧ span R s = p

Tactic:
intro h

Result:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{u}
h : p.spanRank ≤ a
⊢ ∃ s, #↑s ≤ a ∧ span R s = p

Proof state:
case mp.intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{u}
h : p.spanRank ≤ a
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
⊢ ∃ s, #↑s ≤ a ∧ span R s = p

Tactic:
exact ⟨s, ⟨hs₁ ▸ h, hs₂⟩⟩

Result:
no goals

Proof state:
case mp
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{u}
h : p.spanRank ≤ a
⊢ ∃ s, #↑s ≤ a ∧ span R s = p

Tactic:
obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p

Result:
case mp.intro.intro
R : Type u_1
M : Type u
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
a : Cardinal.{u}
h : p.spanRank ≤ a
s : Set M
hs₁ : #↑s = p.spanRank
hs₂ : span R s = p
⊢ ∃ s, #↑s ≤ a ∧ span R s = p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem ite_val {n : Nat} {c : Prop} [Decidable c] {x : c → Fin n} (y : ¬c → Fin n) :
    (if h : c then x h else y h).val = if h : c then (x h).val else (y h).val

Proof state:
n : Nat
c : Prop
inst✝ : Decidable c
x : c → Fin n
y : ¬c → Fin n
⊢ ↑(if h : c then x h else y h) = if h : c then ↑(x h) else ↑(y h)

Tactic:
by_cases c <;> simp [*]

Result:
no goals
-- Mathlib/Data/ZMod/ValMinAbs.lean
lemma valMinAbs_mul_two_eq_iff (a : ZMod n) : a.valMinAbs * 2 = n ↔ 2 * a.val = n

Proof state:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ ¬a.valMinAbs * 2 = ↑(n + 1)

Tactic:
intro he

Result:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
he : a.valMinAbs * 2 = ↑(n + 1)
⊢ False

Proof state:
case neg
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ a.valMinAbs * 2 = ↑(n + 1) ↔ 2 * a.val = n + 1

Tactic:
apply iff_of_false _ (mt _ h)

Result:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ ¬a.valMinAbs * 2 = ↑(n + 1)

n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ 2 * a.val = n + 1 → a.val ≤ n.succ / 2

Proof state:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ a.val * 2 = n + 1 → a.val ≤ n.succ / 2

Tactic:
exact fun h => (Nat.le_div_iff_mul_le zero_lt_two).2 h.le

Result:
no goals

Proof state:
case zero
a : ZMod 0
⊢ a.valMinAbs * 2 = ↑0 ↔ 2 * a.val = 0

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
a : ZMod n
⊢ a.valMinAbs * 2 = ↑n ↔ 2 * a.val = n

Tactic:
rcases n with - | n

Result:
case zero
a : ZMod 0
⊢ a.valMinAbs * 2 = ↑0 ↔ 2 * a.val = 0

case succ
n : ℕ
a : ZMod (n + 1)
⊢ a.valMinAbs * 2 = ↑(n + 1) ↔ 2 * a.val = n + 1

Proof state:
n : ℕ
a : ZMod (n + 1)
h✝ : ¬0 ≤ a.valMinAbs
h : ¬0 ≤ ↑(n + 1)
he : a.valMinAbs * 2 = ↑(n + 1)
⊢ False

n : ℕ
a : ZMod (n + 1)
h : ¬0 ≤ a.valMinAbs
he : a.valMinAbs * 2 = ↑(n + 1)
⊢ 0 < 2

Tactic:
exacts [h (Nat.cast_nonneg _), zero_lt_two]

Result:
no goals

Proof state:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ 2 * a.val = n + 1 → a.val ≤ n.succ / 2

Tactic:
rw [mul_comm]

Result:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ a.val * 2 = n + 1 → a.val ≤ n.succ / 2

Proof state:
case succ
n : ℕ
a : ZMod (n + 1)
⊢ a.valMinAbs * 2 = ↑(n + 1) ↔ 2 * a.val = n + 1

Tactic:
by_cases h : a.val ≤ n.succ / 2

Result:
case pos
n : ℕ
a : ZMod (n + 1)
h : a.val ≤ n.succ / 2
⊢ a.valMinAbs * 2 = ↑(n + 1) ↔ 2 * a.val = n + 1

case neg
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ a.valMinAbs * 2 = ↑(n + 1) ↔ 2 * a.val = n + 1

Proof state:
case pos
n : ℕ
a : ZMod (n + 1)
h : a.val ≤ n.succ / 2
⊢ (if a.val ≤ (n + 1) / 2 then ↑a.val else ↑a.val - ↑(n + 1)) * 2 = ↑(n + 1) ↔ 2 * a.val = n + 1

Tactic:
rw [if_pos h, ← Int.natCast_inj, Nat.cast_mul, Nat.cast_two, mul_comm]

Result:
no goals

Proof state:
case pos
n : ℕ
a : ZMod (n + 1)
h : a.val ≤ n.succ / 2
⊢ a.valMinAbs * 2 = ↑(n + 1) ↔ 2 * a.val = n + 1

Tactic:
dsimp [valMinAbs]

Result:
case pos
n : ℕ
a : ZMod (n + 1)
h : a.val ≤ n.succ / 2
⊢ (if a.val ≤ (n + 1) / 2 then ↑a.val else ↑a.val - ↑(n + 1)) * 2 = ↑(n + 1) ↔ 2 * a.val = n + 1

Proof state:
n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
he : a.valMinAbs * 2 = ↑(n + 1)
⊢ False

Tactic:
rw [← a.valMinAbs_nonneg_iff, ← mul_nonneg_iff_left_nonneg_of_pos, he] at h

Result:
n : ℕ
a : ZMod (n + 1)
h✝ : ¬0 ≤ a.valMinAbs
h : ¬0 ≤ ↑(n + 1)
he : a.valMinAbs * 2 = ↑(n + 1)
⊢ False

n : ℕ
a : ZMod (n + 1)
h : ¬0 ≤ a.valMinAbs
he : a.valMinAbs * 2 = ↑(n + 1)
⊢ 0 < 2
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem IsLindelof.compl_mem_sets_of_nhdsWithin (hs : IsLindelof s) {f : Filter X}
    [CountableInterFilter f] (hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f) : sᶜ ∈ f

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
⊢ sᶜ ∈ f

Tactic:
refine hs.compl_mem_sets fun x hx ↦ ?_

Result:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
⊢ sᶜ ∈ 𝓝 x ⊓ f

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
⊢ ∃ i ∈ 𝓝 x ⊓ 𝓟 s, (id i)ᶜ ∈ f

Tactic:
exact hf x hx

Result:
no goals

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
⊢ sᶜ ∈ 𝓝 x ⊓ f

Tactic:
rw [← disjoint_principal_right, disjoint_right_comm, (basis_sets _).disjoint_iff_left]

Result:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
hs : IsLindelof s
f : Filter X
inst✝ : CountableInterFilter f
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
⊢ ∃ i ∈ 𝓝 x ⊓ 𝓟 s, (id i)ᶜ ∈ f
-- Mathlib/Data/Fin/Basic.lean
theorem coe_of_injective_castSucc_symm {n : ℕ} (i : Fin n.succ) (hi) :
    ((Equiv.ofInjective castSucc (castSucc_injective _)).symm ⟨i, hi⟩ : ℕ) = i

Proof state:
n : ℕ
i : Fin n.succ
hi : i ∈ Set.range castSucc
⊢ ↑((Equiv.ofInjective castSucc ⋯).symm ⟨i, hi⟩).castSucc = ↑i

Tactic:
exact congr_arg val (Equiv.apply_ofInjective_symm _ _)

Result:
no goals

Proof state:
n : ℕ
i : Fin n.succ
hi : i ∈ Set.range castSucc
⊢ ↑((Equiv.ofInjective castSucc ⋯).symm ⟨i, hi⟩) = ↑i

Tactic:
rw [← coe_castSucc]

Result:
n : ℕ
i : Fin n.succ
hi : i ∈ Set.range castSucc
⊢ ↑((Equiv.ofInjective castSucc ⋯).symm ⟨i, hi⟩).castSucc = ↑i
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem isoPullback_inv_fst (h : IsPullback fst snd f g) [HasPullback f g] :
    h.isoPullback.inv ≫ fst = pullback.fst _ _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ h.isoPullback.inv ≫ fst = pullback.fst f g

Tactic:
simp [Iso.inv_comp_eq]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem natDegree_iterate_derivative (p : R[X]) (k : ℕ) :
    (derivative^[k] p).natDegree ≤ p.natDegree - k

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
d : ℕ
hd : ((⇑derivative)^[d] p).natDegree ≤ p.natDegree - d
⊢ (derivative ((⇑derivative)^[d] p)).natDegree ≤ p.natDegree - d - 1

Tactic:
exact (natDegree_derivative_le _).trans <| Nat.sub_le_sub_right hd 1

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ((⇑derivative)^[0] p).natDegree ≤ p.natDegree - 0

Tactic:
rw [Function.iterate_zero_apply, Nat.sub_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ((⇑derivative)^[k] p).natDegree ≤ p.natDegree - k

Tactic:
induction k with
| zero => rw [Function.iterate_zero_apply, Nat.sub_zero]
| succ d hd =>
    rw [Function.iterate_succ_apply', Nat.sub_succ']
    exact (natDegree_derivative_le _).trans <| Nat.sub_le_sub_right hd 1

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
d : ℕ
hd : ((⇑derivative)^[d] p).natDegree ≤ p.natDegree - d
⊢ ((⇑derivative)^[d + 1] p).natDegree ≤ p.natDegree - (d + 1)

Tactic:
rw [Function.iterate_succ_apply', Nat.sub_succ']

Result:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
d : ℕ
hd : ((⇑derivative)^[d] p).natDegree ≤ p.natDegree - d
⊢ (derivative ((⇑derivative)^[d] p)).natDegree ≤ p.natDegree - d - 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem getElem_attachWith {xs : List α} {P : α → Prop} {H : ∀ a ∈ xs, P a}
    {i : Nat} (h : i < (xs.attachWith P H).length) :
    (xs.attachWith P H)[i] = ⟨xs[i]'(by simpa using h), H _ (getElem_mem (by simpa using h))⟩ :=
  getElem_pmap ..

Proof state:
α : Type ?u.40686
xs : List α
P : α → Prop
H : ∀ (a : α), a ∈ xs → P a
i : Nat
h : i < (xs.attachWith P H).length
⊢ i < xs.length

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Unitization.lean
theorem splitMul_apply (x : Unitization 𝕜 A) :
    splitMul 𝕜 A x = (x.fst, algebraMap 𝕜 (A →L[𝕜] A) x.fst + mul 𝕜 A x.snd) :=
  show (x.fst + 0, _) = (x.fst, _) by rw [add_zero]; rfl

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x : Unitization 𝕜 A
⊢ (x.fst + 0, (lift (NonUnitalAlgHom.Lmul 𝕜 A)).toRingHom x) =
    (x.fst, (algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (mul 𝕜 A) x.snd)

Tactic:
rw [add_zero]

Result:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x : Unitization 𝕜 A
⊢ (x.fst, (lift (NonUnitalAlgHom.Lmul 𝕜 A)).toRingHom x) = (x.fst, (algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (mul 𝕜 A) x.snd)

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : SMulCommClass 𝕜 A A
x : Unitization 𝕜 A
⊢ (x.fst, (lift (NonUnitalAlgHom.Lmul 𝕜 A)).toRingHom x) = (x.fst, (algebraMap 𝕜 (A →L[𝕜] A)) x.fst + (mul 𝕜 A) x.snd)

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean
lemma pairwise_disjoint_gammaSet : Pairwise (Disjoint on gammaSet N)

Proof state:
N : ℕ
u v : Fin 2 → ZMod N
huv : ¬(Disjoint on gammaSet N) u v
⊢ u = v

Tactic:
obtain ⟨f, hf⟩ := Set.not_disjoint_iff.mp huv

Result:
case intro
N : ℕ
u v : Fin 2 → ZMod N
huv : ¬(Disjoint on gammaSet N) u v
f : Fin 2 → ℤ
hf : f ∈ gammaSet N u ∧ f ∈ gammaSet N v
⊢ u = v

Proof state:
N : ℕ
u v : Fin 2 → ZMod N
huv : u ≠ v
⊢ (Disjoint on gammaSet N) u v

Tactic:
contrapose! huv

Result:
N : ℕ
u v : Fin 2 → ZMod N
huv : ¬(Disjoint on gammaSet N) u v
⊢ u = v

Proof state:
case intro
N : ℕ
u v : Fin 2 → ZMod N
huv : ¬(Disjoint on gammaSet N) u v
f : Fin 2 → ℤ
hf : f ∈ gammaSet N u ∧ f ∈ gammaSet N v
⊢ u = v

Tactic:
exact hf.1.1.symm.trans hf.2.1

Result:
no goals

Proof state:
N : ℕ
⊢ Pairwise (Disjoint on gammaSet N)

Tactic:
refine fun u v huv ↦ ?_

Result:
N : ℕ
u v : Fin 2 → ZMod N
huv : u ≠ v
⊢ (Disjoint on gammaSet N) u v
-- Mathlib/Data/Set/Basic.lean
theorem not_monotoneOn_not_antitoneOn_iff_exists_le_le :
    ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
      ∃ᵉ (a ∈ s) (b ∈ s) (c ∈ s), a ≤ b ∧ b ≤ c ∧
        (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Proof state:
α : Type u
β : Type v
s : Set α
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
    ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, and_assoc, exists_and_left,
  not_monotone_not_antitone_iff_exists_le_le, @and_left_comm (_ ∈ s)]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_le_nonneg {s : Set X} (hs : MeasurableSet s) (hf : StronglyMeasurable f)
    (hfi : Integrable f μ) : ∫ x in s, f x ∂μ ≤ ∫ x in {y | 0 ≤ f y}, f x ∂μ

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in {y | 0 ≤ f y}, f x ∂μ

Tactic:
rw [← integral_indicator hs, ←
  integral_indicator (stronglyMeasurable_const.measurableSet_le hf)]

Result:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ ∫ (x : X), s.indicator f x ∂μ ≤ ∫ (x : X), {a | 0 ≤ f a}.indicator f x ∂μ

Proof state:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ ∫ (x : X), s.indicator f x ∂μ ≤ ∫ (x : X), {a | 0 ≤ f a}.indicator f x ∂μ

Tactic:
exact
  integral_mono (hfi.indicator hs)
    (hfi.indicator (stronglyMeasurable_const.measurableSet_le hf))
    (indicator_le_indicator_nonneg s f)

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Basic.lean
lemma IsIdempotentElem.eq_zero_of_isNilpotent [MonoidWithZero R] {e : R}
    (idem : IsIdempotentElem e) (nilp : IsNilpotent e) : e = 0

Proof state:
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
nilp : IsNilpotent e
⊢ e = 0

Tactic:
obtain ⟨rfl | n, hn⟩ := nilp

Result:
case intro.zero
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : e ^ 0 = 0
⊢ e = 0

case intro.succ
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
n : ℕ
hn : e ^ (n + 1) = 0
⊢ e = 0

Proof state:
case intro.zero
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : 1 = 0
⊢ e = 0

Tactic:
rw [← one_mul e, hn, zero_mul]

Result:
no goals

Proof state:
case intro.zero
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : e ^ 0 = 0
⊢ e = 0

Tactic:
rw [pow_zero] at hn

Result:
case intro.zero
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
hn : 1 = 0
⊢ e = 0

Proof state:
case intro.succ
R : Type u_1
inst✝ : MonoidWithZero R
e : R
idem : IsIdempotentElem e
n : ℕ
hn : e ^ (n + 1) = 0
⊢ e = 0

Tactic:
rw [← hn, idem.pow_succ_eq]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
lemma abs_sub_lt_of_lt_lt {m a b : ℕ} (ha : a < m) (hb : b < m) : |(b : ℤ) - a| < m

Proof state:
m a b : ℕ
ha : a < m
hb : b < m
⊢ -↑m < ↑b - ↑a ∧ ↑b - ↑a < ↑m

Tactic:
omega

Result:
no goals

Proof state:
m a b : ℕ
ha : a < m
hb : b < m
⊢ |↑b - ↑a| < ↑m

Tactic:
rw [abs_lt]

Result:
m a b : ℕ
ha : a < m
hb : b < m
⊢ -↑m < ↑b - ↑a ∧ ↑b - ↑a < ↑m
-- Mathlib/GroupTheory/Perm/List.lean
theorem support_formPerm_of_nodup [Fintype α] (l : List α) (h : Nodup l) (h' : ∀ x : α, l ≠ [x]) :
    support (formPerm l) = l.toFinset

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ ↑l.formPerm.support = ↑l.toFinset

Tactic:
convert support_formPerm_of_nodup' _ h h'

Result:
case h.e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ ↑l.formPerm.support = {x | l.formPerm x ≠ x}

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ l.formPerm.support = l.toFinset

Tactic:
rw [← Finset.coe_inj]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ ↑l.formPerm.support = ↑l.toFinset

Proof state:
case h.e'_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ ↑l.formPerm.support = {x | l.formPerm x ≠ x}

Tactic:
simp [Set.ext_iff]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem Equiv.isUniformEmbedding {α β : Type*} [UniformSpace α] [UniformSpace β] (f : α ≃ β)
    (h₁ : UniformContinuous f) (h₂ : UniformContinuous f.symm) : IsUniformEmbedding f :=
  isUniformEmbedding_iff'.2 ⟨f.injective, h₁, by rwa [← Equiv.prodCongr_apply, ← map_equiv_symm]⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α ≃ β
h₁ : UniformContinuous ⇑f
h₂ : UniformContinuous ⇑f.symm
⊢ comap (Prod.map ⇑f ⇑f) (𝓤 β) ≤ 𝓤 α

Tactic:
rwa [← Equiv.prodCongr_apply, ← map_equiv_symm]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem nat_add_aleph0 (n : ℕ) : ↑n + ℵ₀ = ℵ₀

Proof state:
n : ℕ
⊢ ↑n + ℵ₀ = ℵ₀

Tactic:
rw [add_comm, aleph0_add_nat]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem congrArg_cast_hom_left {X Y Z : C} (p : X = Y) (q : Y ⟶ Z) :
    cast (congrArg (fun W : C => W ⟶ Z) p.symm) q = eqToHom p ≫ q

Proof state:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
q : X ⟶ Z
⊢ cast ⋯ q = eqToHom ⋯ ≫ q

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y ⟶ Z
⊢ cast ⋯ q = eqToHom p ≫ q

Tactic:
cases p

Result:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
q : X ⟶ Z
⊢ cast ⋯ q = eqToHom ⋯ ≫ q
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_add_sq_real (x y : F) : ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2

Tactic:
have h := @norm_add_sq ℝ _ _ _ _ x y

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫_ℝ + ‖y‖ ^ 2
⊢ ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
h : ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫_ℝ + ‖y‖ ^ 2
⊢ ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuous_iff_continuousOn_univ {f : α → β} : Continuous f ↔ ContinuousOn f univ

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
⊢ Continuous f ↔ ContinuousOn f univ

Tactic:
simp [continuous_iff_continuousAt, ContinuousOn, ContinuousAt, ContinuousWithinAt,
  nhdsWithin_univ]

Result:
no goals