harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/DFinsupp/Defs.lean
theorem mk_injective (s : Finset ι) : Function.Injective (@mk ι β _ _ s)

Proof state:
case h.mk
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
i : ι
hi : i ∈ s
h1 : (mk s x) ↑⟨i, hi⟩ = (mk s y) ↑⟨i, hi⟩
⊢ x ⟨i, hi⟩ = y ⟨i, hi⟩

Tactic:
dsimp only [mk_apply, Subtype.coe_mk] at h1

Result:
case h.mk
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
i : ι
hi : i ∈ s
h1 : (if H : i ∈ s then x ⟨i, H⟩ else 0) = if H : i ∈ s then y ⟨i, H⟩ else 0
⊢ x ⟨i, hi⟩ = y ⟨i, hi⟩

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
⊢ x = y

Tactic:
ext i

Result:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
i : ↑↑s
⊢ x i = y i

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
i : ↑↑s
⊢ (mk s x) ↑i = (mk s y) ↑i

Tactic:
rw [H]

Result:
no goals

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
i : ↑↑s
⊢ x i = y i

Tactic:
have h1 : (mk s x : ∀ i, β i) i = (mk s y : ∀ i, β i) i := by rw [H]

Result:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
i : ↑↑s
h1 : (mk s x) ↑i = (mk s y) ↑i
⊢ x i = y i

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
i : ↑↑s
h1 : (mk s x) ↑i = (mk s y) ↑i
⊢ x i = y i

Tactic:
obtain ⟨i, hi : i ∈ s⟩ := i

Result:
case h.mk
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
i : ι
hi : i ∈ s
h1 : (mk s x) ↑⟨i, hi⟩ = (mk s y) ↑⟨i, hi⟩
⊢ x ⟨i, hi⟩ = y ⟨i, hi⟩

Proof state:
case h.mk
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
i : ι
hi : i ∈ s
h1 : (if H : i ∈ s then x ⟨i, H⟩ else 0) = if H : i ∈ s then y ⟨i, H⟩ else 0
⊢ x ⟨i, hi⟩ = y ⟨i, hi⟩

Tactic:
simpa only [dif_pos hi] using h1

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
⊢ Function.Injective (mk s)

Tactic:
intro x y H

Result:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
⊢ x = y
-- Mathlib/Topology/Path.lean
theorem truncate_range {a b : X} (γ : Path a b) {t₀ t₁ : ℝ} :
    range (γ.truncate t₀ t₁) ⊆ range γ

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ range ⇑(γ.truncate t₀ t₁) ⊆ range γ.extend

Tactic:
simp only [range_subset_iff, SetCoe.exists, SetCoe.forall]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ ∀ (x : ℝ) (h : x ∈ I), (γ.truncate t₀ t₁) ⟨x, h⟩ ∈ range γ.extend

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ x : ℝ
_hx : x ∈ I
⊢ (γ.truncate t₀ t₁) ⟨x, _hx⟩ ∈ range γ.extend

Tactic:
simp only [DFunLike.coe, Path.truncate, mem_range_self]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ ∀ (x : ℝ) (h : x ∈ I), (γ.truncate t₀ t₁) ⟨x, h⟩ ∈ range γ.extend

Tactic:
intro x _hx

Result:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ x : ℝ
_hx : x ∈ I
⊢ (γ.truncate t₀ t₁) ⟨x, _hx⟩ ∈ range γ.extend

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ range ⇑(γ.truncate t₀ t₁) ⊆ range ⇑γ

Tactic:
rw [← γ.extend_range]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
t₀ t₁ : ℝ
⊢ range ⇑(γ.truncate t₀ t₁) ⊆ range γ.extend
-- Mathlib/Analysis/Convex/Segment.lean
theorem image_mk_segment_right (x : E) (y₁ y₂ : F) :
    (fun y => (x, y)) '' [y₁ -[𝕜] y₂] = [(x, y₁) -[𝕜] (x, y₂)]

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun y => (x, y)) '' [y₁-[𝕜]y₂] = [(x, y₁)-[𝕜](x, y₂)]

Tactic:
rw [segment_eq_image₂, segment_eq_image₂, image_image]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun x_1 => (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} =
    (fun p => p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
a : 𝕜 × 𝕜
ha : a ∈ {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
⊢ (x, a.1 • y₁ + a.2 • y₂) = a.1 • (x, y₁) + a.2 • (x, y₂)

Tactic:
simp [Convex.combo_self ha.2.2]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun x_1 => (x, x_1.1 • y₁ + x_1.2 • y₂)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1} =
    (fun p => p.1 • (x, y₁) + p.2 • (x, y₂)) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}

Tactic:
refine EqOn.image_eq fun a ha ↦ ?_

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
a : 𝕜 × 𝕜
ha : a ∈ {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}
⊢ (x, a.1 • y₁ + a.2 • y₂) = a.1 • (x, y₁) + a.2 • (x, y₂)
-- Mathlib/Analysis/Calculus/FDeriv/WithLp.lean
theorem hasStrictFDerivAt_piLp :
    HasStrictFDerivAt f f' y ↔
      ∀ i, HasStrictFDerivAt (fun x => f x i) (PiLp.proj _ _ i ∘L f') y

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
y : H
⊢ HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun x => f x i) ((PiLp.proj p E i).comp f') y

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_hasStrictFDerivAt_iff, hasStrictFDerivAt_pi']

Result:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
y : H
⊢ (∀ (i : ι),
      HasStrictFDerivAt (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i)
        ((proj i).comp ((↑(PiLp.continuousLinearEquiv p 𝕜 E)).comp f')) y) ↔
    ∀ (i : ι), HasStrictFDerivAt (fun x => f x i) ((PiLp.proj p E i).comp f') y

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
y : H
⊢ (∀ (i : ι),
      HasStrictFDerivAt (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i)
        ((proj i).comp ((↑(PiLp.continuousLinearEquiv p 𝕜 E)).comp f')) y) ↔
    ∀ (i : ι), HasStrictFDerivAt (fun x => f x i) ((PiLp.proj p E i).comp f') y

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Sups.lean
lemma sep_sups_le (s t : Set α) (a : α) :
    {b ∈ s ⊻ t | b ≤ a} = {b ∈ s | b ≤ a} ⊻ {b ∈ t | b ≤ a}

Proof state:
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ {b | b ∈ s ⊻ t ∧ b ≤ a} = {b | b ∈ s ∧ b ≤ a} ⊻ {b | b ∈ t ∧ b ≤ a}

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a x✝ : α
⊢ x✝ ∈ {b | b ∈ s ⊻ t ∧ b ≤ a} ↔ x✝ ∈ {b | b ∈ s ∧ b ≤ a} ⊻ {b | b ∈ t ∧ b ≤ a}

Proof state:
case h
α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a x✝ : α
⊢ x✝ ∈ {b | b ∈ s ⊻ t ∧ b ≤ a} ↔ x✝ ∈ {b | b ∈ s ∧ b ≤ a} ⊻ {b | b ∈ t ∧ b ≤ a}

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem back?_map {f : α → β} {l : Array α} : (l.map f).back? = l.back?.map f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ (map f l).back? = Option.map f l.back?

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
toList✝ : List α
⊢ (map f { toList := toList✝ }).back? = Option.map f { toList := toList✝ }.back?

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
toList✝ : List α
⊢ (map f { toList := toList✝ }).back? = Option.map f { toList := toList✝ }.back?

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem is_left_invariant_haarContent {K₀ : PositiveCompacts G} (g : G) (K : Compacts G) :
    haarContent K₀ (K.map _ <| continuous_mul_left g) = haarContent K₀ K

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
g : G
K : Compacts G
⊢ (haarContent K₀) (Compacts.map (fun b => g * b) ⋯ K) = (haarContent K₀) K

Tactic:
simpa only [ENNReal.coe_inj, ← NNReal.coe_inj, haarContent_apply] using
  is_left_invariant_chaar g K

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublists_cons_perm_append (a : α) (l : List α) :
    sublists (a :: l) ~ sublists l ++ map (cons a) (sublists l) :=
  Perm.trans (sublists_perm_sublists' _) <| by
  rw [sublists'_cons]
  exact Perm.append (sublists_perm_sublists' _).symm (Perm.map _ (sublists_perm_sublists' _).symm)

Proof state:
α : Type u
a : α
l : List α
⊢ (a :: l).sublists' ~ l.sublists ++ map (cons a) l.sublists

Tactic:
rw [sublists'_cons]

Result:
α : Type u
a : α
l : List α
⊢ l.sublists' ++ map (cons a) l.sublists' ~ l.sublists ++ map (cons a) l.sublists

Proof state:
α : Type u
a : α
l : List α
⊢ l.sublists' ++ map (cons a) l.sublists' ~ l.sublists ++ map (cons a) l.sublists

Tactic:
exact Perm.append (sublists_perm_sublists' _).symm (Perm.map _ (sublists_perm_sublists' _).symm)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem eraseIdx_modify_of_eq (f : α → α) (n) (l : List α) :
    (modify f n l).eraseIdx n = l.eraseIdx n

Proof state:
case h
α : Type u_1
f : α → α
n : Nat
l : List α
⊢ ∀ (i : Nat) (h₁ : i < ((modify f n l).eraseIdx n).length) (h₂ : i < (l.eraseIdx n).length),
    ((modify f n l).eraseIdx n)[i] = (l.eraseIdx n)[i]

Tactic:
intro m h₁ h₂

Result:
case h
α : Type u_1
f : α → α
n : Nat
l : List α
m : Nat
h₁ : m < ((modify f n l).eraseIdx n).length
h₂ : m < (l.eraseIdx n).length
⊢ ((modify f n l).eraseIdx n)[m] = (l.eraseIdx n)[m]

Proof state:
case h
α : Type u_1
f : α → α
n : Nat
l : List α
m : Nat
h₁ : m < ((modify f n l).eraseIdx n).length
h₂ : m < (l.eraseIdx n).length
⊢ ((modify f n l).eraseIdx n)[m] = (l.eraseIdx n)[m]

Tactic:
simp only [getElem_eraseIdx, getElem_modify]

Result:
case h
α : Type u_1
f : α → α
n : Nat
l : List α
m : Nat
h₁ : m < ((modify f n l).eraseIdx n).length
h₂ : m < (l.eraseIdx n).length
⊢ (if h : m < n then if n = m then f l[m] else l[m] else if n = m + 1 then f l[m + 1] else l[m + 1]) =
    if h' : m < n then l[m] else l[m + 1]

Proof state:
case h.isFalse.isFalse
α : Type u_1
f : α → α
n : Nat
l : List α
m : Nat
h₁ : m < ((modify f n l).eraseIdx n).length
h₂ : m < (l.eraseIdx n).length
h✝¹ : ¬m < n
h✝ : ¬n = m + 1
⊢ l[m + 1] = l[m + 1]

Tactic:
rfl

Result:
no goals

Proof state:
case h.isFalse.isTrue
α : Type u_1
f : α → α
n : Nat
l : List α
m : Nat
h₁ : m < ((modify f n l).eraseIdx n).length
h₂ : m < (l.eraseIdx n).length
h✝¹ : ¬m < n
h✝ : n = m + 1
⊢ f l[m + 1] = l[m + 1]

Tactic:
omega

Result:
no goals

Proof state:
case hl
α : Type u_1
f : α → α
n : Nat
l : List α
⊢ ((modify f n l).eraseIdx n).length = (l.eraseIdx n).length

Tactic:
simp [length_eraseIdx]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
⊢ (modify f n l).eraseIdx n = l.eraseIdx n

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
f : α → α
n : Nat
l : List α
⊢ ((modify f n l).eraseIdx n).length = (l.eraseIdx n).length

case h
α : Type u_1
f : α → α
n : Nat
l : List α
⊢ ∀ (i : Nat) (h₁ : i < ((modify f n l).eraseIdx n).length) (h₂ : i < (l.eraseIdx n).length),
    ((modify f n l).eraseIdx n)[i] = (l.eraseIdx n)[i]

Proof state:
case h
α : Type u_1
f : α → α
n : Nat
l : List α
m : Nat
h₁ : m < ((modify f n l).eraseIdx n).length
h₂ : m < (l.eraseIdx n).length
⊢ (if h : m < n then if n = m then f l[m] else l[m] else if n = m + 1 then f l[m + 1] else l[m + 1]) =
    if h' : m < n then l[m] else l[m + 1]

Tactic:
split <;> split <;> first | rfl | omega

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ico_eq_Ico_iff (h : a₁ < b₁ ∨ a₂ < b₂) : Ico a₁ b₁ = Ico a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ :=
  ⟨fun e => by
      simp only [Subset.antisymm_iff] at e
      simp only [le_antisymm_iff]
      rcases h with h | h <;>
      simp only [gt_iff_lt, not_lt, Ico_subset_Ico_iff h] at e <;>
      [ rcases e with ⟨⟨h₁, h₂⟩, e'⟩; rcases e with ⟨e', ⟨h₁, h₂⟩⟩ ] <;>
      -- Porting note: restore `tauto`
      have hab := (Ico_subset_Ico_iff <| h₁.trans_lt <| h.trans_le h₂).1 e' <;>
      [ exact ⟨⟨hab.left, h₁⟩, ⟨h₂, hab.right⟩⟩; exact ⟨⟨h₁, hab.left⟩, ⟨hab.right, h₂⟩⟩ ],
    fun ⟨h₁, h₂⟩ => by rw [h₁, h₂]⟩

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ = Ico a₂ b₂
⊢ a₁ = a₂ ∧ b₁ = b₂

Tactic:
simp only [Subset.antisymm_iff] at e

Result:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
⊢ a₁ = a₂ ∧ b₁ = b₂

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁

Tactic:
rcases h with h | h <;>
simp only [gt_iff_lt, not_lt, Ico_subset_Ico_iff h] at e <;>
[ rcases e with ⟨⟨h₁, h₂⟩, e'⟩; rcases e with ⟨e', ⟨h₁, h₂⟩⟩ ] <;>
have hab := (Ico_subset_Ico_iff <| h₁.trans_lt <| h.trans_le h₂).1 e' <;>
[ exact ⟨⟨hab.left, h₁⟩, ⟨h₂, hab.right⟩⟩; exact ⟨⟨h₁, hab.left⟩, ⟨hab.right, h₂⟩⟩ ]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : a₁ < b₁ ∨ a₂ < b₂
x✝ : a₁ = a₂ ∧ b₁ = b₂
h₁ : a₁ = a₂
h₂ : b₁ = b₂
⊢ Ico a₁ b₁ = Ico a₂ b₂

Tactic:
rw [h₁, h₂]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
⊢ a₁ = a₂ ∧ b₁ = b₂

Tactic:
simp only [le_antisymm_iff]

Result:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : a₁ < b₁ ∨ a₂ < b₂
e : Ico a₁ b₁ ⊆ Ico a₂ b₂ ∧ Ico a₂ b₂ ⊆ Ico a₁ b₁
⊢ (a₁ ≤ a₂ ∧ a₂ ≤ a₁) ∧ b₁ ≤ b₂ ∧ b₂ ≤ b₁
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem lintegral_coe_eq_integral (f : α → ℝ≥0) (hfi : Integrable (fun x => (f x : ℝ)) μ) :
    ∫⁻ a, f a ∂μ = ENNReal.ofReal (∫ a, f a ∂μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (fun x => ↑(f x)) μ
⊢ ∫⁻ (a : α), ↑(f a) ∂μ ≠ ⊤

Tactic:
simpa [← lt_top_iff_ne_top, hasFiniteIntegral_iff_enorm, NNReal.enorm_eq] using
  hfi.hasFiniteIntegral

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (fun x => ↑(f x)) μ
⊢ ∫⁻ (a : α), ↑(f a) ∂μ = ENNReal.ofReal (∫ (a : α), ↑(f a) ∂μ)

Tactic:
simp_rw [integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall fun x => (f x).coe_nonneg)
    hfi.aestronglyMeasurable, ← ENNReal.coe_nnreal_eq]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (fun x => ↑(f x)) μ
⊢ ∫⁻ (a : α), ↑(f a) ∂μ = ENNReal.ofReal (∫⁻ (a : α), ↑(f a) ∂μ).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (fun x => ↑(f x)) μ
⊢ ∫⁻ (a : α), ↑(f a) ∂μ = ENNReal.ofReal (∫⁻ (a : α), ↑(f a) ∂μ).toReal

Tactic:
rw [ENNReal.ofReal_toReal]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (fun x => ↑(f x)) μ
⊢ ∫⁻ (a : α), ↑(f a) ∂μ ≠ ⊤
-- Mathlib/NumberTheory/Modular.lean
theorem abs_c_le_one (hz : z ∈ 𝒟ᵒ) (hg : g • z ∈ 𝒟ᵒ) : |g 1 0| ≤ 1

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : ℝ := normSq (denom (↑g) z)
⊢ c ^ 4 * z.im ^ 2 * (z.im ^ 2 / normSq (denom (↑g) z) ^ 2) * 16 = c ^ 4 * z.im ^ 4 / nsq ^ 2 * 16

Tactic:
ring

Result:
no goals

Proof state:
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
this : 9 * c ^ 4 < 16
⊢ (3 * c ^ 2) ^ 2 < 4 ^ 2

Tactic:
linarith

Result:
no goals

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
⊢ 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4

Tactic:
gcongr <;> apply three_lt_four_mul_im_sq_of_mem_fdo <;> assumption

Result:
no goals

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c' ^ 2 ≤ 1 ^ 2
⊢ |↑g 1 0| ≤ 1

Tactic:
rwa [sq_le_sq, abs_one] at this

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem range_exp_mul_I : (Set.range fun x : ℝ => exp (x * I)) = Metric.sphere 0 1

Proof state:
⊢ (range fun x => cexp (↑x * I)) = sphere 0 1

Tactic:
ext x

Result:
case h
x : ℂ
⊢ (x ∈ range fun x => cexp (↑x * I)) ↔ x ∈ sphere 0 1

Proof state:
case h
x : ℂ
⊢ (x ∈ range fun x => cexp (↑x * I)) ↔ x ∈ sphere 0 1

Tactic:
simp only [mem_sphere_zero_iff_norm, norm_eq_one_iff, Set.mem_range]

Result:
no goals
-- Mathlib/Algebra/Lie/Sl2.lean
/-- Given a representation of a Lie algebra with distinguished `sl₂` triple, a simultaneous
eigenvector for the action of both `h` and `e` necessarily has eigenvalue zero for `e`. -/
lemma HasPrimitiveVectorWith.mk' [NoZeroSMulDivisors ℤ M] (t : IsSl2Triple h e f) (m : M) (μ ρ : R)
    (hm : m ≠ 0) (hm' : ⁅h, m⁆ = μ • m) (he : ⁅e, m⁆ = ρ • m) :
    HasPrimitiveVectorWith t m μ  where
  ne_zero := hm
  lie_h := hm'
  lie_e

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
h e f : L
inst✝ : NoZeroSMulDivisors ℤ M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
⊢ ⁅e, m⁆ = 0

Tactic:
suffices 2 • ⁅e, m⁆ = 0 by simpa using this

Result:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
h e f : L
inst✝ : NoZeroSMulDivisors ℤ M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
⊢ 2 • ⁅e, m⁆ = 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
h e f : L
inst✝ : NoZeroSMulDivisors ℤ M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
this : 2 • ⁅e, m⁆ = 0
⊢ ⁅e, m⁆ = 0

Tactic:
simpa using this

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
h e f : L
inst✝ : NoZeroSMulDivisors ℤ M
t : IsSl2Triple h e f
m : M
μ ρ : R
hm : m ≠ 0
hm' : ⁅h, m⁆ = μ • m
he : ⁅e, m⁆ = ρ • m
⊢ 2 • ⁅e, m⁆ = 0

Tactic:
rw [← nsmul_lie, ← t.lie_h_e_nsmul, lie_lie, hm', lie_smul, he, lie_smul, hm',
  smul_smul, smul_smul, mul_comm ρ μ, sub_self]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem affineIndependent_iff {ι} {p : ι → V} :
    AffineIndependent k p ↔
      ∀ (s : Finset ι) (w : ι → k), s.sum w = 0 → ∑ e ∈ s, w e • p e = 0 → ∀ e ∈ s, w e = 0 :=
  forall₃_congr fun s w hw => by simp [s.weightedVSub_eq_linear_combination hw]

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ι : Type u_5
p : ι → V
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
⊢ ((s.weightedVSub p) w = 0 → ∀ i ∈ s, w i = 0) ↔ ∑ e ∈ s, w e • p e = 0 → ∀ e ∈ s, w e = 0

Tactic:
simp [s.weightedVSub_eq_linear_combination hw]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
theorem hurwitzZetaEven_neg_two_mul_nat_add_one (a : UnitAddCircle) (n : ℕ) :
    hurwitzZetaEven a (-2 * (n + 1)) = 0

Proof state:
a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ -2 * (↑n + 1) = -(2 * ↑(n + 1))

Tactic:
simp

Result:
no goals

Proof state:
a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ hurwitzZetaEven a (-2 * (↑n + 1)) = 0

Tactic:
rw [hurwitzZetaEven, Function.update_of_ne this, Gammaℝ_eq_zero_iff.mpr ⟨n + 1, by simp⟩,
  div_zero]

Result:
no goals

Proof state:
a : UnitAddCircle
n : ℕ
⊢ hurwitzZetaEven a (-2 * (↑n + 1)) = 0

Tactic:
have : (-2 : ℂ) * (n + 1) ≠ 0 :=
  mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (Nat.cast_add_one_ne_zero n)

Result:
a : UnitAddCircle
n : ℕ
this : -2 * (↑n + 1) ≠ 0
⊢ hurwitzZetaEven a (-2 * (↑n + 1)) = 0
-- Mathlib/LinearAlgebra/Pi.lean
theorem biInf_comap_proj :
    ⨅ i ∈ I, comap (proj i : ((i : ι) → φ i) →ₗ[R] φ i) (p i) = pi I p

Proof state:
case h
R : Type u
ι : Type x
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
I : Set ι
p : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
⊢ x ∈ ⨅ i ∈ I, comap (proj i) (p i) ↔ x ∈ pi I p

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
ι : Type x
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
I : Set ι
p : (i : ι) → Submodule R (φ i)
⊢ ⨅ i ∈ I, comap (proj i) (p i) = pi I p

Tactic:
ext x

Result:
case h
R : Type u
ι : Type x
inst✝² : Semiring R
φ : ι → Type u_1
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
I : Set ι
p : (i : ι) → Submodule R (φ i)
x : (i : ι) → φ i
⊢ x ∈ ⨅ i ∈ I, comap (proj i) (p i) ↔ x ∈ pi I p
-- Mathlib/Data/Rat/Floor.lean
theorem isInt_intFloor {R} [LinearOrderedRing R] [FloorRing R] (r : R) (m : ℤ) :
    IsInt r m → IsInt ⌊r⌋ m

Proof state:
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
r : R
m : ℤ
⊢ IsInt r m → IsInt ⌊r⌋ m

Tactic:
rintro ⟨⟨⟩⟩

Result:
case mk.refl
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt ⌊↑m⌋ m

Proof state:
case mk.refl
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt ⌊↑m⌋ m

Tactic:
exact ⟨by simp⟩

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ ⌊↑m⌋ = ↑m

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean
lemma pi_norm (x : C⋆ᵐᵒᵈ (Π i, E i)) : ‖x‖ = √‖∑ i, ⟪x i, x i⟫_A‖

Proof state:
A : Type u_1
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → Module ℂ (E i)
inst✝¹ : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝ : (i : ι) → CStarModule A (E i)
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
⊢ ‖x‖ = √‖∑ i : ι, ⟪x i, x i⟫_A‖

Tactic:
rfl

Result:
no goals

Proof state:
A : Type u_1
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → Module ℂ (E i)
inst✝¹ : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝ : (i : ι) → CStarModule A (E i)
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
⊢ ‖x‖ = √‖∑ i : ι, ⟪x i, x i⟫_A‖

Tactic:
with_reducible_and_instances rfl

Result:
no goals