harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Game/PGame.lean
theorem leftMoves_add_cases {x y : PGame} (k) {P : (x + y).LeftMoves → Prop}
    (hl : ∀ i, P <| toLeftMovesAdd (Sum.inl i)) (hr : ∀ i, P <| toLeftMovesAdd (Sum.inr i)) :
    P k

Proof state:
case inr
x y : PGame
k : (x + y).LeftMoves
P : (x + y).LeftMoves → Prop
hl : ∀ (i : x.LeftMoves), P (toLeftMovesAdd (Sum.inl i))
hr : ∀ (i : y.LeftMoves), P (toLeftMovesAdd (Sum.inr i))
i : y.LeftMoves
⊢ P (toLeftMovesAdd (Sum.inr i))

Tactic:
exact hr i

Result:
no goals

Proof state:
x y : PGame
k : (x + y).LeftMoves
P : (x + y).LeftMoves → Prop
hl : ∀ (i : x.LeftMoves), P (toLeftMovesAdd (Sum.inl i))
hr : ∀ (i : y.LeftMoves), P (toLeftMovesAdd (Sum.inr i))
⊢ P k

Tactic:
rw [← toLeftMovesAdd.apply_symm_apply k]

Result:
x y : PGame
k : (x + y).LeftMoves
P : (x + y).LeftMoves → Prop
hl : ∀ (i : x.LeftMoves), P (toLeftMovesAdd (Sum.inl i))
hr : ∀ (i : y.LeftMoves), P (toLeftMovesAdd (Sum.inr i))
⊢ P (toLeftMovesAdd (toLeftMovesAdd.symm k))

Proof state:
x y : PGame
k : (x + y).LeftMoves
P : (x + y).LeftMoves → Prop
hl : ∀ (i : x.LeftMoves), P (toLeftMovesAdd (Sum.inl i))
hr : ∀ (i : y.LeftMoves), P (toLeftMovesAdd (Sum.inr i))
⊢ P (toLeftMovesAdd (toLeftMovesAdd.symm k))

Tactic:
rcases toLeftMovesAdd.symm k with i | i

Result:
case inl
x y : PGame
k : (x + y).LeftMoves
P : (x + y).LeftMoves → Prop
hl : ∀ (i : x.LeftMoves), P (toLeftMovesAdd (Sum.inl i))
hr : ∀ (i : y.LeftMoves), P (toLeftMovesAdd (Sum.inr i))
i : x.LeftMoves
⊢ P (toLeftMovesAdd (Sum.inl i))

case inr
x y : PGame
k : (x + y).LeftMoves
P : (x + y).LeftMoves → Prop
hl : ∀ (i : x.LeftMoves), P (toLeftMovesAdd (Sum.inl i))
hr : ∀ (i : y.LeftMoves), P (toLeftMovesAdd (Sum.inr i))
i : y.LeftMoves
⊢ P (toLeftMovesAdd (Sum.inr i))

Proof state:
case inl
x y : PGame
k : (x + y).LeftMoves
P : (x + y).LeftMoves → Prop
hl : ∀ (i : x.LeftMoves), P (toLeftMovesAdd (Sum.inl i))
hr : ∀ (i : y.LeftMoves), P (toLeftMovesAdd (Sum.inr i))
i : x.LeftMoves
⊢ P (toLeftMovesAdd (Sum.inl i))

Tactic:
exact hl i

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
theorem norm_def (x : tsze R M) : ‖x‖ = ‖fst x‖ + ‖snd x‖

Proof state:
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ ‖x.1‖ + ‖x.2‖ = ‖x.fst‖ + ‖x.snd‖

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ 0 < ENNReal.toReal 1

Tactic:
norm_num

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ (‖x.1‖ ^ ENNReal.toReal 1 + ‖x.2‖ ^ ENNReal.toReal 1) ^ (1 / ENNReal.toReal 1) = ‖x.fst‖ + ‖x.snd‖

Tactic:
simp only [ENNReal.one_toReal, Real.rpow_one, div_one]

Result:
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ ‖x.1‖ + ‖x.2‖ = ‖x.fst‖ + ‖x.snd‖

Proof state:
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ ‖x‖ = ‖x.fst‖ + ‖x.snd‖

Tactic:
rw [WithLp.prod_norm_eq_add (by norm_num)]

Result:
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
x : tsze R M
⊢ (‖x.1‖ ^ ENNReal.toReal 1 + ‖x.2‖ ^ ENNReal.toReal 1) ^ (1 / ENNReal.toReal 1) = ‖x.fst‖ + ‖x.snd‖
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem equiv_empty : Equiv empty a b ↔ a = b

Proof state:
a b : Nat
⊢ empty.Equiv a b ↔ a = b

Tactic:
simp [Equiv]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
/-- See `ENNReal.mul_inv_cancel_right` for a simpler version assuming `b ≠ 0`, `b ≠ ∞`. -/
protected lemma mul_inv_cancel_right' (hb₀ : b = 0 → a = 0) (hb : b = ∞ → a = 0) :
    a * b * b⁻¹ = a

Proof state:
case inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb : b = ⊤ → a = 0
hb₀ : b ≠ 0
⊢ a * b * b⁻¹ = a

Tactic:
obtain rfl | hb := eq_or_ne b ⊤

Result:
case inr.inl
a : ℝ≥0∞
hb₀✝ : ⊤ = 0 → a = 0
hb : ⊤ = ⊤ → a = 0
hb₀ : ⊤ ≠ 0
⊢ a * ⊤ * ⊤⁻¹ = a

case inr.inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb✝ : b = ⊤ → a = 0
hb₀ : b ≠ 0
hb : b ≠ ⊤
⊢ a * b * b⁻¹ = a

Proof state:
a b : ℝ≥0∞
hb₀ : b = 0 → a = 0
hb : b = ⊤ → a = 0
⊢ a * b * b⁻¹ = a

Tactic:
obtain rfl | hb₀ := eq_or_ne b 0

Result:
case inl
a : ℝ≥0∞
hb₀ : 0 = 0 → a = 0
hb : 0 = ⊤ → a = 0
⊢ a * 0 * 0⁻¹ = a

case inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb : b = ⊤ → a = 0
hb₀ : b ≠ 0
⊢ a * b * b⁻¹ = a

Proof state:
case inr.inr
a b : ℝ≥0∞
hb₀✝ : b = 0 → a = 0
hb✝ : b = ⊤ → a = 0
hb₀ : b ≠ 0
hb : b ≠ ⊤
⊢ a * b * b⁻¹ = a

Tactic:
simp [mul_assoc, ENNReal.mul_inv_cancel, *]

Result:
no goals

Proof state:
case inl
a : ℝ≥0∞
hb₀ : 0 = 0 → a = 0
hb : 0 = ⊤ → a = 0
⊢ a * 0 * 0⁻¹ = a

Tactic:
simp_all

Result:
no goals

Proof state:
case inr.inl
a : ℝ≥0∞
hb₀✝ : ⊤ = 0 → a = 0
hb : ⊤ = ⊤ → a = 0
hb₀ : ⊤ ≠ 0
⊢ a * ⊤ * ⊤⁻¹ = a

Tactic:
simp_all

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_erase_bot [DecidableEq α] (s : Finset α) : (s.erase ⊥).sup id = s.sup id

Proof state:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
⊢ (s.erase ⊥).sup id = s.sup id

Tactic:
refine (sup_mono (s.erase_subset _)).antisymm (Finset.sup_le_iff.2 fun a ha => ?_)

Result:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ id a ≤ (s.erase ⊥).sup id

Proof state:
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ id a ≤ (s.erase ⊥).sup id

Tactic:
obtain rfl | ha' := eq_or_ne a ⊥

Result:
case inl
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
ha : ⊥ ∈ s
⊢ id ⊥ ≤ (s.erase ⊥).sup id

case inr
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
ha' : a ≠ ⊥
⊢ id a ≤ (s.erase ⊥).sup id

Proof state:
case inr
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
ha' : a ≠ ⊥
⊢ id a ≤ (s.erase ⊥).sup id

Tactic:
exact le_sup (mem_erase.2 ⟨ha', ha⟩)

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
ha : ⊥ ∈ s
⊢ id ⊥ ≤ (s.erase ⊥).sup id

Tactic:
exact bot_le

Result:
no goals
-- Mathlib/Algebra/Lie/Basic.lean
lemma lie_swap_lie [Bracket L₂ L₁] [AddCommGroup M] [IsLieTower L₁ L₂ M] [IsLieTower L₂ L₁ M]
    (x : L₁) (y : L₂) (m : M) : ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆

Proof state:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
⊢ ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆

Tactic:
have h1 := leibniz_lie x y m

Result:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆

Proof state:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆

Tactic:
convert congr($h1.symm - $h2) using 1 <;> simp only [add_sub_cancel_right, sub_add_cancel_right]

Result:
no goals

Proof state:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆

Tactic:
have h2 := leibniz_lie y x m

Result:
L₁ : Type u_1
L₂ : Type u_2
M : Type u_3
inst✝⁶ : Bracket L₁ L₂
inst✝⁵ : Bracket L₁ M
inst✝⁴ : Bracket L₂ M
inst✝³ : Bracket L₂ L₁
inst✝² : AddCommGroup M
inst✝¹ : IsLieTower L₁ L₂ M
inst✝ : IsLieTower L₂ L₁ M
x : L₁
y : L₂
m : M
h1 : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
h2 : ⁅y, ⁅x, m⁆⁆ = ⁅⁅y, x⁆, m⁆ + ⁅x, ⁅y, m⁆⁆
⊢ ⁅⁅x, y⁆, m⁆ = -⁅⁅y, x⁆, m⁆
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem proj_eq_self {x : I → Bool} (h : ∀ i, x i ≠ false → J i) : Proj J x = x

Proof state:
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
⊢ Proj J x = x

Tactic:
ext i

Result:
case h
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
i : I
⊢ Proj J x i = x i

Proof state:
case h
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
i : I
⊢ false ≠ x i → J i

Tactic:
simpa only [ne_comm] using h i

Result:
no goals

Proof state:
case h
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
i : I
⊢ Proj J x i = x i

Tactic:
simp only [Proj, ite_eq_left_iff]

Result:
case h
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
i : I
⊢ ¬J i → false = x i

Proof state:
case h
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
i : I
⊢ ¬J i → false = x i

Tactic:
contrapose!

Result:
case h
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
i : I
⊢ false ≠ x i → J i
-- Mathlib/Data/Multiset/UnionInter.lean
lemma inter_add_distrib (s t u : Multiset α) : s ∩ t + u = (s + u) ∩ (t + u)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : s ∩ t + u ≠ (s + u) ∩ (t + u)
⊢ False

Tactic:
obtain ⟨a, ha⟩ := lt_iff_cons_le.1 <| h.lt_of_le <| le_inter
  (Multiset.add_le_add_right inter_le_left) (Multiset.add_le_add_right inter_le_right)

Result:
case intro
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : s ∩ t + u ≠ (s + u) ∩ (t + u)
a : α
ha : a ::ₘ (s ∩ t + u) ≤ (s + u) ∩ (t + u)
⊢ False

Proof state:
case intro
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : s ∩ t + u ≠ (s + u) ∩ (t + u)
a : α
ha : a ::ₘ (s ∩ t + u) ≤ (s + u) ∩ (t + u)
⊢ False

Tactic:
rw [← cons_add] at ha

Result:
case intro
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : s ∩ t + u ≠ (s + u) ∩ (t + u)
a : α
ha : a ::ₘ s ∩ t + u ≤ (s + u) ∩ (t + u)
⊢ False

Proof state:
case intro
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : s ∩ t + u ≠ (s + u) ∩ (t + u)
a : α
ha : a ::ₘ s ∩ t + u ≤ (s + u) ∩ (t + u)
⊢ False

Tactic:
exact (lt_cons_self (s ∩ t) a).not_le <| le_inter
  (Multiset.le_of_add_le_add_right (ha.trans inter_le_left))
  (Multiset.le_of_add_le_add_right (ha.trans inter_le_right))

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ∩ t + u = (s + u) ∩ (t + u)

Tactic:
by_contra! h

Result:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : s ∩ t + u ≠ (s + u) ∩ (t + u)
⊢ False
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive] lemma eq_iff_eq_of_mul_eq_mul (h : a * b = c * d) : a = c ↔ b = d

Proof state:
α : Type u_1
inst✝ : CancelCommMonoid α
a b c d : α
h : a * b = c * d
⊢ a = c ↔ b = d

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem derivWithin_sub_const (c : F) :
    derivWithin (fun y => f y - c) s x = derivWithin f s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
c : F
⊢ derivWithin (fun y => f y - c) s x = derivWithin f s x

Tactic:
simp only [derivWithin, fderivWithin_sub_const]

Result:
no goals
-- Mathlib/Probability/Kernel/Defs.lean
theorem sum_zero [Countable ι] : (Kernel.sum fun _ : ι => (0 : Kernel α β)) = 0

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
⊢ (Kernel.sum fun x => 0) = 0

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum fun x => 0) a) s = (0 a) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum fun x => 0) a) s = (0 a) s

Tactic:
rw [sum_apply' _ a hs]

Result:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
a : α
s : Set β
hs : MeasurableSet s
⊢ ∑' (n : ι), (0 a) s = (0 a) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
a : α
s : Set β
hs : MeasurableSet s
⊢ ∑' (n : ι), (0 a) s = (0 a) s

Tactic:
simp only [zero_apply, Measure.coe_zero, Pi.zero_apply, tsum_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modify_eq_take_cons_drop {f : α → α} {n} {l : List α} (h : n < l.length) :
    modify f n l = take n l ++ f l[n] :: drop (n + 1) l

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
h : n < l.length
⊢ take n l ++ modifyHead f (l[n] :: drop (n + 1) l) = take n l ++ f l[n] :: drop (n + 1) l

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
h : n < l.length
⊢ modify f n l = take n l ++ f l[n] :: drop (n + 1) l

Tactic:
rw [modify_eq_take_drop, drop_eq_getElem_cons h]

Result:
α : Type u_1
f : α → α
n : Nat
l : List α
h : n < l.length
⊢ take n l ++ modifyHead f (l[n] :: drop (n + 1) l) = take n l ++ f l[n] :: drop (n + 1) l
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem mem_roots' : a ∈ p.roots ↔ p ≠ 0 ∧ IsRoot p a

Proof state:
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ a ∈ p.roots ↔ p ≠ 0 ∧ p.IsRoot a

Tactic:
classical
rw [← count_pos, count_roots p, rootMultiplicity_pos']

Result:
no goals

Proof state:
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ a ∈ p.roots ↔ p ≠ 0 ∧ p.IsRoot a

Tactic:
rw [← count_pos, count_roots p, rootMultiplicity_pos']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modifyTailIdx_modifyTailIdx_le {f g : List α → List α} (m n : Nat) (l : List α)
    (h : n ≤ m) :
    (l.modifyTailIdx f n).modifyTailIdx g m =
      l.modifyTailIdx (fun l => (f l).modifyTailIdx g (m - n)) n

Proof state:
case intro
α : Type u_1
f g : List α → List α
n : Nat
l : List α
m : Nat
h : n ≤ n + m
⊢ modifyTailIdx g (n + m) (modifyTailIdx f n l) = modifyTailIdx (fun l => modifyTailIdx g (n + m - n) (f l)) n l

Tactic:
rw [Nat.add_comm, modifyTailIdx_modifyTailIdx, Nat.add_sub_cancel]

Result:
no goals

Proof state:
α : Type u_1
f g : List α → List α
m n : Nat
l : List α
h : n ≤ m
⊢ modifyTailIdx g m (modifyTailIdx f n l) = modifyTailIdx (fun l => modifyTailIdx g (m - n) (f l)) n l

Tactic:
rcases Nat.exists_eq_add_of_le h with ⟨m, rfl⟩

Result:
case intro
α : Type u_1
f g : List α → List α
n : Nat
l : List α
m : Nat
h : n ≤ n + m
⊢ modifyTailIdx g (n + m) (modifyTailIdx f n l) = modifyTailIdx (fun l => modifyTailIdx g (n + m - n) (f l)) n l
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem smul_inter_ne_empty_iff' {s t : Set α} {x : α} :
    x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x

Proof state:
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x

Tactic:
simp_rw [smul_inter_ne_empty_iff, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
lemma normedSpaceCore: NormedSpace.Core ℂ (CStarMatrix m n A) where
  norm_nonneg M := (toCLM M).opNorm_nonneg
  norm_smul c M

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
⊢ ∀ (x : CStarMatrix m n A), ‖x‖ = 0 ↔ x = 0

Tactic:
simpa only [norm_def, norm_eq_zero, ← injective_iff_map_eq_zero'] using toCLM_injective

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
h✝ : Function.Injective ⇑toCLM
⊢ ∀ (x : CStarMatrix m n A), ‖toCLM x‖ = 0 ↔ x = 0

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
c : ℂ
M : CStarMatrix m n A
⊢ ‖c • M‖ = ‖c‖ * ‖M‖

Tactic:
rw [norm_def, norm_def, map_smul, norm_smul _ (toCLM M)]

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
c : ℂ
M : CStarMatrix m n A
⊢ BoundedSMul ℂ (C⋆ᵐᵒᵈ (n → A) →L[ℂ] C⋆ᵐᵒᵈ (m → A))

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M₁ M₂ : CStarMatrix m n A
⊢ ‖M₁ + M₂‖ ≤ ‖M₁‖ + ‖M₂‖

Tactic:
simpa [← map_add] using norm_add_le (toCLM M₁) (toCLM M₂)

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderEmbedding.lean
theorem preimage_Ioc : e ⁻¹' Ioc (e x) (e y) = Ioc x y

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' Ioc (e x) (e y) = Ioc x y

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ioc (e x) (e y) ↔ x✝ ∈ Ioc x y

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ioc (e x) (e y) ↔ x✝ ∈ Ioc x y

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/RingedSpace/PresheafedSpace.lean
theorem hext {X Y : PresheafedSpace C} (α β : Hom X Y) (w : α.base = β.base) (h : HEq α.c β.c) :
    α = β

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
α β : X.Hom Y
w : α.base = β.base
h : HEq α.c β.c
⊢ α = β

Tactic:
cases α

Result:
case mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
β : X.Hom Y
base✝ : ↑X ⟶ ↑Y
c✝ : Y.presheaf ⟶ (Presheaf.pushforward C base✝).obj X.presheaf
w : { base := base✝, c := c✝ }.base = β.base
h : HEq { base := base✝, c := c✝ }.c β.c
⊢ { base := base✝, c := c✝ } = β

Proof state:
case mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
β : X.Hom Y
base✝ : ↑X ⟶ ↑Y
c✝ : Y.presheaf ⟶ (Presheaf.pushforward C base✝).obj X.presheaf
w : { base := base✝, c := c✝ }.base = β.base
h : HEq { base := base✝, c := c✝ }.c β.c
⊢ { base := base✝, c := c✝ } = β

Tactic:
cases β

Result:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base✝¹ : ↑X ⟶ ↑Y
c✝¹ : Y.presheaf ⟶ (Presheaf.pushforward C base✝¹).obj X.presheaf
base✝ : ↑X ⟶ ↑Y
c✝ : Y.presheaf ⟶ (Presheaf.pushforward C base✝).obj X.presheaf
w : { base := base✝¹, c := c✝¹ }.base = { base := base✝, c := c✝ }.base
h : HEq { base := base✝¹, c := c✝¹ }.c { base := base✝, c := c✝ }.c
⊢ { base := base✝¹, c := c✝¹ } = { base := base✝, c := c✝ }

Proof state:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base✝¹ : ↑X ⟶ ↑Y
c✝¹ : Y.presheaf ⟶ (Presheaf.pushforward C base✝¹).obj X.presheaf
base✝ : ↑X ⟶ ↑Y
c✝ : Y.presheaf ⟶ (Presheaf.pushforward C base✝).obj X.presheaf
w : { base := base✝¹, c := c✝¹ }.base = { base := base✝, c := c✝ }.base
h : HEq { base := base✝¹, c := c✝¹ }.c { base := base✝, c := c✝ }.c
⊢ { base := base✝¹, c := c✝¹ } = { base := base✝, c := c✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma completedHurwitzZetaEven_eq (a : UnitAddCircle) (s : ℂ) :
    completedHurwitzZetaEven a s =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)

Proof state:
case e_a
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a s - ((1 / (s / 2)) • if a = 0 then 1 else 0) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s

Tactic:
rw [smul_eq_mul, mul_comm, mul_div_assoc, div_div, div_mul_cancel₀ _ two_ne_zero, mul_one_div]

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven a s = completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)

Tactic:
rw [completedHurwitzZetaEven, WeakFEPair.Λ, sub_div, sub_div]

Result:
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 -
      ((hurwitzEvenFEPair a).ε / (↑(hurwitzEvenFEPair a).k - s / 2)) • (hurwitzEvenFEPair a).g₀ / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)

Proof state:
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 -
      ((hurwitzEvenFEPair a).ε / (↑(hurwitzEvenFEPair a).k - s / 2)) • (hurwitzEvenFEPair a).g₀ / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s - 1 / (1 - s)

Tactic:
congr 1

Result:
case e_a
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s

case e_a
a : UnitAddCircle
s : ℂ
⊢ ((hurwitzEvenFEPair a).ε / (↑(hurwitzEvenFEPair a).k - s / 2)) • (hurwitzEvenFEPair a).g₀ / 2 = 1 / (1 - s)

Proof state:
case e_a
a : UnitAddCircle
s : ℂ
⊢ ((hurwitzEvenFEPair a).ε / (↑(hurwitzEvenFEPair a).k - s / 2)) • (hurwitzEvenFEPair a).g₀ / 2 = 1 / (1 - s)

Tactic:
change (1 / (↑(1 / 2 : ℝ) - s / 2)) • 1 / 2 = 1 / (1 - s)

Result:
case e_a
a : UnitAddCircle
s : ℂ
⊢ (1 / (↑(1 / 2) - s / 2)) • 1 / 2 = 1 / (1 - s)

Proof state:
case e_a
a : UnitAddCircle
s : ℂ
⊢ (1 / (1 / 2 - s / 2)) • 1 / 2 = 1 / (1 - s)

Tactic:
rw [smul_eq_mul, mul_one, ← sub_div, div_div, div_mul_cancel₀ _ two_ne_zero]

Result:
no goals

Proof state:
case e_a
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).f₀ / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s

Tactic:
change completedHurwitzZetaEven₀ a s - (1 / (s / 2)) • (if a = 0 then 1 else 0) / 2 =
  completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s

Result:
case e_a
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a s - ((1 / (s / 2)) • if a = 0 then 1 else 0) / 2 =
    completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s

Proof state:
case e_a
a : UnitAddCircle
s : ℂ
⊢ (1 / (↑(1 / 2) - s / 2)) • 1 / 2 = 1 / (1 - s)

Tactic:
push_cast

Result:
case e_a
a : UnitAddCircle
s : ℂ
⊢ (1 / (1 / 2 - s / 2)) • 1 / 2 = 1 / (1 - s)
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffOn_succ_of_fderivWithin (hf : DifferentiableOn 𝕜 f s)
    (h' : n = ω → AnalyticOn 𝕜 f s)
    (h : ContDiffOn 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) : ContDiffOn 𝕜 (n + 1) f s

Proof state:
case inr
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
hf : DifferentiableOn 𝕜 f s
h' : n = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 n (fun y => fderivWithin 𝕜 f s y) s
hn : n ≠ ∞
x : E
hx : x ∈ s
⊢ ∃ u ∈ 𝓝[s] x,
    (n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 n f' u x

Tactic:
exact ⟨s, self_mem_nhdsWithin, h', fderivWithin 𝕜 f s,
  fun y hy => (hf y hy).hasFDerivWithinAt, h x hx⟩

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
hf : DifferentiableOn 𝕜 f s
h' : ∞ = ω → AnalyticOn 𝕜 f s
h : ContDiffOn 𝕜 ∞ (fun y => fderivWithin 𝕜 f s y) s
m : ℕ
x : E
hx : x ∈ s
⊢ ↑m = ω → AnalyticOn 𝕜 f s

Tactic:
simp

Result:
no goals