harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem getElem_modifyHead {l : List α} {f : α → α} {n} (h : n < (l.modifyHead f).length) :
    (l.modifyHead f)[n] = if h' : n = 0 then f (l[0]'(by simp at h; omega)) else l[n]'(by simpa using h)

Proof state:
α : Type ?u.1753
l : List α
f : α → α
n : Nat
h : n < (modifyHead f l).length
h' : n = 0
⊢ 0 < l.length

Tactic:
simp at h

Result:
α : Type ?u.1753
l : List α
f : α → α
n : Nat
h' : n = 0
h : n < l.length
⊢ 0 < l.length

Proof state:
case cons
α : Type u_1
f : α → α
n : Nat
hd : α
tl : List α
h : n < (modifyHead f (hd :: tl)).length
⊢ (modifyHead f (hd :: tl))[n] = if h' : n = 0 then f (hd :: tl)[0] else (hd :: tl)[n]

Tactic:
cases n <;> simp

Result:
no goals

Proof state:
α : Type ?u.1753
l : List α
f : α → α
n : Nat
h' : n = 0
h : n < l.length
⊢ 0 < l.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
l : List α
f : α → α
n : Nat
h : n < (modifyHead f l).length
⊢ (modifyHead f l)[n] = if h' : n = 0 then f l[0] else l[n]

Tactic:
cases l with
| nil => simp at h
| cons hd tl => cases n <;> simp

Result:
no goals

Proof state:
case nil
α : Type u_1
f : α → α
n : Nat
h : n < (modifyHead f []).length
⊢ (modifyHead f [])[n] = if h' : n = 0 then f [][0] else [][n]

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type ?u.1753
l : List α
f : α → α
n : Nat
h : n < (modifyHead f l).length
h' : ¬n = 0
⊢ n < l.length

Tactic:
simpa using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem getElem_zipIdx (a : Array α) (k : Nat) (i : Nat) (h : i < (a.zipIdx k).size) :
    (a.zipIdx k)[i] = (a[i]'(by simp_all), k + i)

Proof state:
α : Type ?u.46115
a : Array α
k i : Nat
h : i < (a.zipIdx k).size
⊢ i < a.size

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
a : Array α
k i : Nat
h : i < (a.zipIdx k).size
⊢ (a.zipIdx k)[i] = (a[i], k + i)

Tactic:
simp [zipIdx]

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem ωSup_zip (c₀ : Chain α) (c₁ : Chain β) : ωSup (c₀.zip c₁) = (ωSup c₀, ωSup c₁)

Proof state:
case H
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain α
c₁ : Chain β
⊢ ∀ (c : α × β), ωSup (c₀.zip c₁) ≤ c ↔ (ωSup c₀, ωSup c₁) ≤ c

Tactic:
rintro ⟨z₁, z₂⟩

Result:
case H.mk
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain α
c₁ : Chain β
z₁ : α
z₂ : β
⊢ ωSup (c₀.zip c₁) ≤ (z₁, z₂) ↔ (ωSup c₀, ωSup c₁) ≤ (z₁, z₂)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain α
c₁ : Chain β
⊢ ωSup (c₀.zip c₁) = (ωSup c₀, ωSup c₁)

Tactic:
apply eq_of_forall_ge_iff

Result:
case H
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain α
c₁ : Chain β
⊢ ∀ (c : α × β), ωSup (c₀.zip c₁) ≤ c ↔ (ωSup c₀, ωSup c₁) ≤ c

Proof state:
case H.mk
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain α
c₁ : Chain β
z₁ : α
z₂ : β
⊢ ωSup (c₀.zip c₁) ≤ (z₁, z₂) ↔ (ωSup c₀, ωSup c₁) ≤ (z₁, z₂)

Tactic:
simp [ωSup_le_iff, forall_and]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_smul_le {r : R} {f : MvPolynomial σ R} :
    m.degree (r • f) ≼[m] m.degree f

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (C r) + m.degree f) = m.toSyn (m.degree f)

Tactic:
simp

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (C r * f)) ≤ m.toSyn (m.degree f)

Tactic:
apply le_of_le_of_eq degree_mul_le

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (C r) + m.degree f) = m.toSyn (m.degree f)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (r • f)) ≤ m.toSyn (m.degree f)

Tactic:
rw [smul_eq_C_mul]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
r : R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (C r * f)) ≤ m.toSyn (m.degree f)
-- Mathlib/Topology/Maps/Basic.lean
theorem id : IsOpenMap (@id X) := fun s hs => by rwa [image_id]

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ IsOpen (id '' s)

Tactic:
rwa [image_id]

Result:
no goals
-- Mathlib/Data/Finset/Piecewise.lean
lemma update_piecewise [DecidableEq ι] (i : ι) (v : π i) :
    update (s.piecewise f g) i v = s.piecewise (update f i v) (update g i v)

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
⊢ update (s.piecewise f g) i v = s.piecewise (update f i v) (update g i v)

Tactic:
ext j

Result:
case h
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
j : ι
⊢ update (s.piecewise f g) i v j = s.piecewise (update f i v) (update g i v) j

Proof state:
case h
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : (j : ι) → Decidable (j ∈ s)
inst✝ : DecidableEq ι
i : ι
v : π i
j : ι
⊢ update (s.piecewise f g) i v j = s.piecewise (update f i v) (update g i v) j

Tactic:
rcases em (j = i) with (rfl | hj) <;> by_cases hs : j ∈ s <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem decide_eq_decide {p q : Prop} {_ : Decidable p} {_ : Decidable q} :
    decide p = decide q ↔ (p ↔ q) :=
  ⟨fun h => by rw [← decide_eq_true_iff (p := p), h, decide_eq_true_iff], fun h => by simp [h]⟩

Proof state:
p q : Prop
x✝¹ : Decidable p
x✝ : Decidable q
h : decide p = decide q
⊢ p ↔ q

Tactic:
rw [← decide_eq_true_iff (p := p), h, decide_eq_true_iff]

Result:
no goals

Proof state:
p q : Prop
x✝¹ : Decidable p
x✝ : Decidable q
h : p ↔ q
⊢ decide p = decide q

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Tactic/Abel.lean
lemma subst_into_addg {α} [AddCommGroup α] (l r tl tr t)
    (prl : (l : α) = tl) (prr : r = tr) (prt : tl + tr = t) : l + r = t

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
l r tl tr t : α
prl : l = tl
prr : r = tr
prt : tl + tr = t
⊢ l + r = t

Tactic:
rw [prl, prr, prt]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
lemma measurable_of_real_prod {f : EReal × β → γ}
    (h_real : Measurable fun p : ℝ × β ↦ f (p.1, p.2))
    (h_bot : Measurable fun x ↦ f (⊥, x)) (h_top : Measurable fun x ↦ f (⊤, x)) : Measurable f :=
  .of_union₃_range_cover (measurableEmbedding_prod_mk_left _) (measurableEmbedding_prod_mk_left _)
    (measurableEmbedding_coe.prodMap .id) (by simp [-univ_subset_iff, subset_def, EReal.forall])
    h_bot h_top h_real

Proof state:
β : Type u_6
γ : Type u_7
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : EReal × β → γ
h_real : Measurable fun p => f (↑p.1, p.2)
h_bot : Measurable fun x => f (⊥, x)
h_top : Measurable fun x => f (⊤, x)
⊢ univ ⊆ range (Prod.mk ⊥) ∪ range (Prod.mk ⊤) ∪ range (Prod.map Real.toEReal id)

Tactic:
simp [-univ_subset_iff, subset_def, EReal.forall]

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

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

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

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

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

Tactic:
simp_rw [WeakFEPair.symm, hurwitzEvenFEPair, push_cast, inv_one, smul_eq_mul,
  mul_comm _ (if _ then _ else _), mul_div_assoc, div_div, ← sub_div,
  div_mul_cancel₀ _ (two_ne_zero' ℂ), mul_one_div]

Result:
no goals

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

Tactic:
congr 1

Result:
case e_a
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 =
    completedCosZeta₀ a s - 1 / s

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

Proof state:
case e_a
a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).symm.Λ₀ (s / 2) / 2 - (1 / (s / 2)) • (hurwitzEvenFEPair a).symm.f₀ / 2 =
    completedCosZeta₀ a s - 1 / s

Tactic:
rw [completedCosZeta₀, WeakFEPair.symm, hurwitzEvenFEPair, smul_eq_mul, mul_one, div_div,
  div_mul_cancel₀ _ (two_ne_zero' ℂ)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range_succ_eq_map (n : Nat) : range (n + 1) = 0 :: map succ (range n)

Proof state:
case e_tail.e_f
n : Nat
⊢ (fun x => 1 + x) = succ

Tactic:
exact funext (Nat.add_comm 1)

Result:
no goals

Proof state:
n : Nat
⊢ range (n + 1) = 0 :: map succ (range n)

Tactic:
rw [range_eq_range', range_eq_range', range', Nat.add_comm, ← map_add_range']

Result:
n : Nat
⊢ 0 :: map (fun x => 1 + x) (range' 0 n) = 0 :: map succ (range' 0 n)

Proof state:
n : Nat
⊢ 0 :: map (fun x => 1 + x) (range' 0 n) = 0 :: map succ (range' 0 n)

Tactic:
congr

Result:
case e_tail.e_f
n : Nat
⊢ (fun x => 1 + x) = succ
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem insertNew_toList {p : Path α} : (p.insertNew v).toList = p.withList [v]

Proof state:
α : Type u_1
v : α
p : Path α
⊢ (p.insertNew v).toList = p.withList [v]

Tactic:
simp [insertNew]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem flatten_equiv {c : Computation (WSeq α)} {s} (h : s ∈ c) : flatten c ~ʷ s

Proof state:
case h2
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
s' : Computation (WSeq α)
⊢ flatten s' ~ʷ s → flatten s'.think ~ʷ s

Tactic:
apply Equiv.trans

Result:
case h2.a
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
s' : Computation (WSeq α)
⊢ flatten s'.think ~ʷ flatten s'

Proof state:
case h2
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ ∀ (s_1 : Computation (WSeq α)), flatten s_1 ~ʷ s → flatten s_1.think ~ʷ s

Tactic:
intro s'

Result:
case h2
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
s' : Computation (WSeq α)
⊢ flatten s' ~ʷ s → flatten s'.think ~ʷ s

Proof state:
case h1
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ flatten (Computation.pure s) ~ʷ s

Tactic:
simp [Equiv.refl]

Result:
no goals

Proof state:
case h2.a
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
s' : Computation (WSeq α)
⊢ flatten s'.think ~ʷ flatten s'

Tactic:
simp [think_equiv]

Result:
no goals

Proof state:
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ flatten c ~ʷ s

Tactic:
apply Computation.memRecOn h

Result:
case h1
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ flatten (Computation.pure s) ~ʷ s

case h2
α : Type u
c : Computation (WSeq α)
s : WSeq α
h : s ∈ c
⊢ ∀ (s_1 : Computation (WSeq α)), flatten s_1 ~ʷ s → flatten s_1.think ~ʷ s
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Ioo {a b : α} : ((↑) : ℤ → α) ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋ ⌈b⌉

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ Int.cast ⁻¹' Ioo a b = Ioo ⌊a⌋ ⌈b⌉

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ioo a b ↔ x✝ ∈ Ioo ⌊a⌋ ⌈b⌉

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ioo a b ↔ x✝ ∈ Ioo ⌊a⌋ ⌈b⌉

Tactic:
simp [floor_lt, lt_ceil]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem tail_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
    (H : ∀ (a : α), a ∈ xs → P a) :
    (xs.pmap f H).tail = xs.tail.pmap f (fun a h => H a (mem_of_mem_tail h))

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ (pmap f xs H).tail = pmap f xs.tail ⋯

Tactic:
cases xs <;> simp

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Diam.lean
theorem diam_union' {t : Set α} (h : (s ∩ t).Nonempty) : diam (s ∪ t) ≤ diam s + diam t

Proof state:
α : Type u_1
s : Set α
inst✝ : PseudoEMetricSpace α
t : Set α
h : (s ∩ t).Nonempty
⊢ diam (s ∪ t) ≤ diam s + diam t

Tactic:
let ⟨x, ⟨xs, xt⟩⟩ := h

Result:
α : Type u_1
s : Set α
inst✝ : PseudoEMetricSpace α
t : Set α
h : (s ∩ t).Nonempty
x : α
xs : x ∈ s
xt : x ∈ t
⊢ diam (s ∪ t) ≤ diam s + diam t

Proof state:
α : Type u_1
s : Set α
inst✝ : PseudoEMetricSpace α
t : Set α
h : (s ∩ t).Nonempty
x : α
xs : x ∈ s
xt : x ∈ t
⊢ diam (s ∪ t) ≤ diam s + diam t

Tactic:
simpa using diam_union xs xt

Result:
no goals
-- Mathlib/Data/Finset/NatDivisors.lean
/-- The divisors of a product of natural numbers are the pointwise product of the divisors of the
factors. -/
lemma Nat.divisors_mul (m n : ℕ) : divisors (m * n) = divisors m * divisors n

Proof state:
case h
m n k : ℕ
⊢ (∃ x x_1, (x ∣ m ∧ x_1 ∣ n ∧ x * x_1 = k) ∧ m ≠ 0 ∧ n ≠ 0) ↔ ∃ y x, (y ∣ m ∧ m ≠ 0) ∧ (x ∣ n ∧ n ≠ 0) ∧ y * x = k

Tactic:
simp only [and_assoc, and_comm, and_left_comm]

Result:
no goals

Proof state:
m n : ℕ
⊢ (m * n).divisors = m.divisors * n.divisors

Tactic:
ext k

Result:
case h
m n k : ℕ
⊢ k ∈ (m * n).divisors ↔ k ∈ m.divisors * n.divisors

Proof state:
case h
m n k : ℕ
⊢ k ∈ (m * n).divisors ↔ k ∈ m.divisors * n.divisors

Tactic:
simp_rw [mem_mul, mem_divisors, dvd_mul, mul_ne_zero_iff, ← exists_and_left, ← exists_and_right]

Result:
case h
m n k : ℕ
⊢ (∃ x x_1, (x ∣ m ∧ x_1 ∣ n ∧ x * x_1 = k) ∧ m ≠ 0 ∧ n ≠ 0) ↔ ∃ y x, (y ∣ m ∧ m ≠ 0) ∧ (x ∣ n ∧ n ≠ 0) ∧ y * x = k
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_lt_one_iff (hx : 0 ≤ x) :
    x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Proof state:
case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Tactic:
simp [rpow_lt_one_iff_of_pos hx, hx.ne.symm]

Result:
no goals

Proof state:
x y : ℝ
hx : 0 ≤ x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Tactic:
rcases hx.eq_or_lt with (rfl | hx)

Result:
case inl
y : ℝ
hx : 0 ≤ 0
⊢ 0 ^ y < 1 ↔ 0 = 0 ∧ y ≠ 0 ∨ 1 < 0 ∧ y < 0 ∨ 0 < 1 ∧ 0 < y

case inr
x y : ℝ
hx✝ : 0 ≤ x
hx : 0 < x
⊢ x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

Proof state:
case inl
y : ℝ
hx : 0 ≤ 0
⊢ 0 ^ y < 1 ↔ 0 = 0 ∧ y ≠ 0 ∨ 1 < 0 ∧ y < 0 ∨ 0 < 1 ∧ 0 < y

Tactic:
rcases _root_.em (y = 0) with (rfl | hy) <;> simp [*, lt_irrefl, zero_lt_one]

Result:
no goals
-- Mathlib/Topology/UnitInterval.lean
theorem symm_symm (x : I) : σ (σ x) = x :=
  Subtype.ext <| by simp [symm]

Proof state:
x : ↑I
⊢ ↑(σ (σ x)) = ↑x

Tactic:
simp [symm]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/PDeriv.lean
theorem pderiv_X_self (i : σ) : pderiv i (X i : MvPolynomial σ R) = 1

Proof state:
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
⊢ (pderiv i) (X i) = 1

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
⊢ (pderiv i) (X i) = 1

Tactic:
classical simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem differentiableAt_comp_sub (a : E) :
    DifferentiableAt 𝕜 (fun x ↦ f (x - a)) x ↔ DifferentiableAt 𝕜 f (x - a)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x a : E
⊢ DifferentiableAt 𝕜 (fun x => f (x - a)) x ↔ DifferentiableAt 𝕜 f (x - a)

Tactic:
simp [DifferentiableAt, hasFDerivAt_comp_sub]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem sup_eq_closure_mul (H K : Submonoid M) : H ⊔ K = closure ((H : Set M) * (K : Set M)) :=
  le_antisymm
    (sup_le (fun h hh => subset_closure ⟨h, hh, 1, K.one_mem, mul_one h⟩) fun k hk =>
      subset_closure ⟨1, H.one_mem, k, hk, one_mul k⟩)
    ((closure_mul_le _ _).trans <| by rw [closure_eq, closure_eq])

Proof state:
M : Type u_3
inst✝ : Monoid M
H K : Submonoid M
⊢ closure ↑H ⊔ closure ↑K ≤ H ⊔ K

Tactic:
rw [closure_eq, closure_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem subset_replicate {n : Nat} {a : α} {l : List α} (h : n ≠ 0) : l ⊆ replicate n a ↔ ∀ x ∈ l, x = a

Proof state:
case cons
α : Type u_1
n : Nat
a : α
h : n ≠ 0
x : α
xs : List α
ih : xs ⊆ replicate n a ↔ ∀ (x : α), x ∈ xs → x = a
⊢ (∀ (x : α), x ∈ xs → x = a) → x = a → ¬n = 0

Tactic:
solve_by_elim

Result:
no goals

Proof state:
case nil
α : Type u_1
n : Nat
a : α
h : n ≠ 0
⊢ [] ⊆ replicate n a ↔ ∀ (x : α), x ∈ [] → x = a

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
n : Nat
a : α
h : n ≠ 0
x : α
xs : List α
ih : xs ⊆ replicate n a ↔ ∀ (x : α), x ∈ xs → x = a
⊢ x :: xs ⊆ replicate n a ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → x_1 = a

Tactic:
simp only [cons_subset, mem_replicate, ne_eq, ih, mem_cons, forall_eq_or_imp,
  and_congr_left_iff, and_iff_right_iff_imp]

Result:
case cons
α : Type u_1
n : Nat
a : α
h : n ≠ 0
x : α
xs : List α
ih : xs ⊆ replicate n a ↔ ∀ (x : α), x ∈ xs → x = a
⊢ (∀ (x : α), x ∈ xs → x = a) → x = a → ¬n = 0

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
h : n ≠ 0
⊢ l ⊆ replicate n a ↔ ∀ (x : α), x ∈ l → x = a

Tactic:
induction l with
| nil => simp
| cons x xs ih =>
  simp only [cons_subset, mem_replicate, ne_eq, ih, mem_cons, forall_eq_or_imp,
    and_congr_left_iff, and_iff_right_iff_imp]
  solve_by_elim

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/Monoid.lean
theorem ContMDiffWithinAt.div_const (hf : ContMDiffWithinAt I' I n f s x) :
    ContMDiffWithinAt I' I n (fun x ↦ f x / c) s x

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_2
inst✝¹¹ : TopologicalSpace H
E : Type u_3
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁸ : DivInvMonoid G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : ChartedSpace H G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f : M → G
s : Set M
x : M
c : G
hf : ContMDiffWithinAt I' I n f s x
⊢ ContMDiffWithinAt I' I n (fun x => f x / c) s x

Tactic:
simpa only [div_eq_mul_inv] using hf.mul contMDiffWithinAt_const

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Hom.lean
theorem toMulActionHom_injective {f g : A →ₑ+[φ] B} (h : (f : A →ₑ[φ] B) = (g : A →ₑ[φ] B)) :
    f = g

Proof state:
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : DistribMulAction M A
B : Type u_5
inst✝¹ : AddMonoid B
inst✝ : DistribMulAction N B
f g : A →ₑ+[φ] B
h : ↑f = ↑g
⊢ f = g

Tactic:
ext a

Result:
case a
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : DistribMulAction M A
B : Type u_5
inst✝¹ : AddMonoid B
inst✝ : DistribMulAction N B
f g : A →ₑ+[φ] B
h : ↑f = ↑g
a : A
⊢ f a = g a

Proof state:
case a
M : Type u_1
inst✝⁵ : Monoid M
N : Type u_2
inst✝⁴ : Monoid N
φ : M →* N
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : DistribMulAction M A
B : Type u_5
inst✝¹ : AddMonoid B
inst✝ : DistribMulAction N B
f g : A →ₑ+[φ] B
h : ↑f = ↑g
a : A
⊢ f a = g a

Tactic:
exact MulActionHom.congr_fun h a

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.sameRay_vsub_left {x y z : P} (h : Wbtw R x y z) : SameRay R (y -ᵥ x) (z -ᵥ x)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Wbtw R x y z
⊢ SameRay R (y -ᵥ x) (z -ᵥ x)

Tactic:
rcases h with ⟨t, ⟨ht0, _⟩, rfl⟩

Result:
case intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
right✝ : t ≤ 1
⊢ SameRay R ((lineMap x z) t -ᵥ x) (z -ᵥ x)

Proof state:
case intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x z : P
t : R
ht0 : 0 ≤ t
right✝ : t ≤ 1
⊢ SameRay R ((lineMap x z) t -ᵥ x) (z -ᵥ x)

Tactic:
simpa [lineMap_apply] using SameRay.sameRay_nonneg_smul_left (z -ᵥ x) ht0

Result:
no goals
-- Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean
theorem CharZero.of_module (M) [AddCommMonoidWithOne M] [CharZero M] [Module R M] : CharZero R

Proof state:
R : Type u_1
inst✝³ : Semiring R
M : Type u_3
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
⊢ CharZero R

Tactic:
refine ⟨fun m n h => @Nat.cast_injective M _ _ _ _ ?_⟩

Result:
R : Type u_1
inst✝³ : Semiring R
M : Type u_3
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ ↑m = ↑n

Proof state:
R : Type u_1
inst✝³ : Semiring R
M : Type u_3
inst✝² : AddCommMonoidWithOne M
inst✝¹ : CharZero M
inst✝ : Module R M
m n : ℕ
h : ↑m = ↑n
⊢ ↑m = ↑n

Tactic:
rw [← nsmul_one, ← nsmul_one, ← Nat.cast_smul_eq_nsmul R, ← Nat.cast_smul_eq_nsmul R, h]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Constructions.lean
theorem orthogonal_cross_left {v w : ℙ F (Fin 3 → F)} (h : v ≠ w) :
    v.orthogonal (cross v w)

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal v

Tactic:
exact cross_orthogonal_left h

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ v.orthogonal (v.cross w)

Tactic:
rw [orthogonal_comm]

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : ℙ F (Fin 3 → F)
h : v ≠ w
⊢ (v.cross w).orthogonal v
-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem locally_zero_iff (hp : HasFPowerSeriesAt f p z₀) : (∀ᶠ z in 𝓝 z₀, f z = 0) ↔ p = 0 :=
  ⟨fun hf => hp.eq_zero_of_eventually hf, fun h => eventually_eq_zero (𝕜 := 𝕜) (by rwa [h] at hp)⟩

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p = 0
⊢ HasFPowerSeriesAt f 0 z₀

Tactic:
rwa [h] at hp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_one_ne (n : Nat) : n + 1 ≠ n := fun h => by cases h

Proof state:
n : Nat
h : n + 1 = n
⊢ False

Tactic:
cases h

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem differentiableAt_neg_iff : DifferentiableAt 𝕜 (fun y => -f y) x ↔ DifferentiableAt 𝕜 f x :=
  ⟨fun h => by simpa only [neg_neg] using h.neg, fun h => h.neg⟩

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
h : DifferentiableAt 𝕜 (fun y => -f y) x
⊢ DifferentiableAt 𝕜 f x

Tactic:
simpa only [neg_neg] using h.neg

Result:
no goals