harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem foldlM_attachWith [Monad m]
    (l : Vector α n) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x} → m β} {b} :
    (l.attachWith q H).foldlM f b = l.attach.foldlM (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
q : α → Prop
f : β → { x // q x } → m β
b : β
l : Array α
H : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → q a
⊢ foldlM f b ({ toArray := l, size_toArray := ⋯ }.attachWith q H) =
    foldlM
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b { toArray := l, size_toArray := ⋯ }.attach

Tactic:
simp [Array.foldlM_map]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝ : Monad m
l : Vector α n
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : β → { x // q x } → m β
b : β
⊢ foldlM f b (l.attachWith q H) =
    foldlM
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b l.attach

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
q : α → Prop
f : β → { x // q x } → m β
b : β
l : Array α
H : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → q a
⊢ foldlM f b ({ toArray := l, size_toArray := ⋯ }.attachWith q H) =
    foldlM
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b { toArray := l, size_toArray := ⋯ }.attach
-- Mathlib/Data/Seq/WSeq.lean
theorem head_nil : head (nil : WSeq α) = Computation.pure none

Proof state:
α : Type u
⊢ nil.head = Computation.pure none

Tactic:
simp [head]

Result:
no goals
-- Mathlib/Data/Multiset/Fold.lean
theorem fold_cons'_left (b a : α) (s : Multiset α) : (a ::ₘ s).fold op b = s.fold op (a * b)

Proof state:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = fold op (op a b) s

Tactic:
rw [fold_cons'_right, hc.comm]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem inner_rightAngleRotation_swap' (x y : E) : ⟪J x, y⟫ = -⟪x, J y⟫

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner (o.rightAngleRotation x) y = -inner x (o.rightAngleRotation y)

Tactic:
simp [o.inner_rightAngleRotation_swap x y]

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem eq_of_vsub_eq_zero {p₁ p₂ : P} (h : p₁ -ᵥ p₂ = (0 : G)) : p₁ = p₂

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p₁ p₂ : P
h : p₁ -ᵥ p₂ = 0
⊢ p₁ = p₂

Tactic:
rw [← vsub_vadd p₁ p₂, h, zero_vadd]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive]
lemma single_le_prod : (∀ x ∈ s, (1 : α) ≤ x) → ∀ x ∈ s, x ≤ s.prod :=
  Quotient.inductionOn s fun l hl x hx => by simpa using List.single_le_prod hl x hx

Proof state:
α : Type u_2
inst✝ : OrderedCommMonoid α
s : Multiset α
l : List α
hl : ∀ x ∈ ⟦l⟧, 1 ≤ x
x : α
hx : x ∈ ⟦l⟧
⊢ x ≤ prod ⟦l⟧

Tactic:
simpa using List.single_le_prod hl x hx

Result:
no goals
-- Mathlib/SetTheory/Nimber/Basic.lean
theorem add_cancel_right (a b : Nimber) : a + b + b = a

Proof state:
a b : Nimber
⊢ a + b + b = a

Tactic:
rw [add_assoc, add_self, add_zero]

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem geom_mean_le_arith_mean3_weighted (w₁ w₂ w₃ p₁ p₂ p₃ : ℝ≥0) :
    w₁ + w₂ + w₃ = 1 →
      p₁ ^ (w₁ : ℝ) * p₂ ^ (w₂ : ℝ) * p₃ ^ (w₃ : ℝ) ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃

Proof state:
w₁ w₂ w₃ p₁ p₂ p₃ : ℝ≥0
⊢ w₁ + w₂ + w₃ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ * p₃ ^ ↑w₃ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃

Tactic:
simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty,
  Finset.univ_eq_empty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one, ← add_assoc,
  mul_assoc] using geom_mean_le_arith_mean_weighted univ ![w₁, w₂, w₃] ![p₁, p₂, p₃]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem ite_eq_false : (if b = false then p else q) ↔ if b then q else p

Proof state:
b : Bool
p q : Prop
⊢ (if b = false then p else q) ↔ if b = true then q else p

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_Ico_mul_neg [Ring α] (x : α) {m n : ℕ} (hmn : m ≤ n) :
    (∑ i ∈ Finset.Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n

Proof state:
α : Type u
inst✝ : Ring α
x : α
m n : ℕ
hmn : m ≤ n
⊢ (∑ i ∈ Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n

Tactic:
rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul_neg, geom_sum_mul_neg, sub_sub_sub_cancel_left]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem expSeries_eq_ofScalars : expSeries 𝕂 𝔸 = ofScalars 𝔸 fun n ↦ (n !⁻¹ : 𝕂)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ expSeries 𝕂 𝔸 = ofScalars 𝔸 fun n => (↑n !)⁻¹

Tactic:
simp_rw [FormalMultilinearSeries.ext_iff, expSeries, ofScalars, implies_true]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
lemma comap_comap (I : TwoSidedIdeal T) (f : R →+* S) (g : S →+* T) :
    (I.comap g).comap f = I.comap (g.comp f)

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
I : TwoSidedIdeal T
f : R →+* S
g : S →+* T
⊢ (comap f) ((comap g) I) = (comap (g.comp f)) I

Tactic:
ext

Result:
case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
I : TwoSidedIdeal T
f : R →+* S
g : S →+* T
x✝ : R
⊢ x✝ ∈ (comap f) ((comap g) I) ↔ x✝ ∈ (comap (g.comp f)) I

Proof state:
case h
R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
I : TwoSidedIdeal T
f : R →+* S
g : S →+* T
x✝ : R
⊢ x✝ ∈ (comap f) ((comap g) I) ↔ x✝ ∈ (comap (g.comp f)) I

Tactic:
simp [mem_comap]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem prime_dvd_of_eq_neg_one {p : ℕ} [Fact p.Prime] {a : ℤ} (h : J(a | p) = -1) {x y : ℤ}
    (hxy : ↑p ∣ (x ^ 2 - a * y ^ 2 : ℤ)) : ↑p ∣ x ∧ ↑p ∣ y

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑p ∣ x ^ 2 - a * y ^ 2
⊢ ↑p ∣ x ∧ ↑p ∣ y

Tactic:
exact legendreSym.prime_dvd_of_eq_neg_one h hxy

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : J(a | p) = -1
x y : ℤ
hxy : ↑p ∣ x ^ 2 - a * y ^ 2
⊢ ↑p ∣ x ∧ ↑p ∣ y

Tactic:
rw [← legendreSym.to_jacobiSym] at h

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑p ∣ x ^ 2 - a * y ^ 2
⊢ ↑p ∣ x ∧ ↑p ∣ y
-- Mathlib/Topology/MetricSpace/Polish.lean
theorem _root_.IsOpen.isClopenable [TopologicalSpace α] [PolishSpace α] {s : Set α}
    (hs : IsOpen s) : IsClopenable s

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsOpen s
⊢ IsClopenable s

Tactic:
simpa using hs.isClosed_compl.isClopenable.compl

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem isOpen_image_iff_of_subset_source {s : Set X} (hs : s ⊆ e.source) :
    IsOpen (e '' s) ↔ IsOpen s

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
hs : s ⊆ e.source
⊢ IsOpen (↑e '' s) ↔ IsOpen s

Tactic:
rw [← e.symm.isOpen_symm_image_iff_of_subset_target hs, e.symm_symm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem takeWhile_append_dropWhile (p : α → Bool) :
    ∀ (l : List α), takeWhile p l ++ dropWhile p l = l
  | [] => rfl
  | x :: xs => by simp [takeWhile, dropWhile]; cases p x <;> simp [takeWhile_append_dropWhile p xs]

Proof state:
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ ((match p x with
      | true => x :: takeWhile p xs
      | false => []) ++
      match p x with
      | true => dropWhile p xs
      | false => x :: xs) =
    x :: xs

Tactic:
cases p x <;> simp [takeWhile_append_dropWhile p xs]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ takeWhile p (x :: xs) ++ dropWhile p (x :: xs) = x :: xs

Tactic:
simp [takeWhile, dropWhile]

Result:
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ ((match p x with
      | true => x :: takeWhile p xs
      | false => []) ++
      match p x with
      | true => dropWhile p xs
      | false => x :: xs) =
    x :: xs
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_add {A : M} (ha : IsUnit A.det) (m n : ℤ) : A ^ (m + n) = A ^ m * A ^ n

Proof state:
case hz
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit A.det
m : ℤ
⊢ A ^ (m + 0) = A ^ m * A ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case hp
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit A.det
m : ℤ
n : ℕ
ihn : A ^ (m + ↑n) = A ^ m * A ^ ↑n
⊢ A ^ (m + (↑n + 1)) = A ^ m * A ^ (↑n + 1)

Tactic:
simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit A.det
m n : ℤ
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
induction n with
| hz => simp
| hp n ihn => simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc]
| hn n ihn => rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]

Result:
no goals

Proof state:
case hn
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
ha : IsUnit A.det
m : ℤ
n : ℕ
ihn : A ^ (m + -↑n) = A ^ m * A ^ (-↑n)
⊢ A ^ (m + (-↑n - 1)) = A ^ m * A ^ (-↑n - 1)

Tactic:
rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc]

Result:
no goals
-- Mathlib/Topology/Constructible.lean
lemma isConstructible_preimage_iff_of_isOpenEmbedding {s : Set Y} (hf : IsOpenEmbedding f)
    (hfcomp : IsRetrocompact (range f)) (hsf : s ⊆ range f) :
    IsConstructible (f ⁻¹' s) ↔ IsConstructible s where
  mp hs

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
hsf : s ⊆ range f
hs : IsConstructible (f ⁻¹' s)
⊢ IsConstructible s

Tactic:
simpa [image_preimage_eq_range_inter, inter_eq_right.2 hsf]
using hs.image_of_isOpenEmbedding hf hfcomp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_insertList_of_mem [BEq α] [EquivBEq α] [Inhabited α]
    {l toInsert : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k')
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ toInsert.map Sigma.fst) :
    getKey! k' (insertList l toInsert) = k

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : k ∈ List.map Sigma.fst toInsert
⊢ getKey! k' (insertList l toInsert) = k

Tactic:
rw [getKey!_eq_getKey?, getKey?_insertList_of_mem k_beq distinct_l distinct_toInsert mem,
  Option.get!_some]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem logMap_zero : logMap (0 : mixedSpace K) = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ logMap 0 = 0

Tactic:
ext

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ logMap 0 x✝ = 0 x✝

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : { w // w ≠ w₀ }
⊢ logMap 0 x✝ = 0 x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem semiconj_conj (f : α₁ → α₁) : Semiconj e f (e.conj f) := fun x => by simp

Proof state:
α₁ : Type u_9
β₁ : Type u_10
e : α₁ ≃ β₁
f : α₁ → α₁
x : α₁
⊢ e (f x) = e.conj f (e x)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem multichoose_neg_add (n k : ℕ) : multichoose (-n : ℤ) (n + k + 1) = 0

Proof state:
n k : ℕ
⊢ multichoose (-↑n) (n + k + 1) = 0

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero (n + k + 1)),
  factorial_nsmul_multichoose_eq_ascPochhammer, smeval_ascPochhammer_neg_add, smul_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_le : |a| ≤ b ↔ -b ≤ a ∧ a ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ |a| ≤ b ↔ -b ≤ a ∧ a ≤ b

Tactic:
rw [abs_le', and_comm, neg_le]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem cycleGraph_degree_two_le {n : ℕ} {v : Fin (n + 2)} :
    (cycleGraph (n + 2)).degree v = Finset.card {v - 1, v + 1}

Proof state:
n : ℕ
v : Fin (n + 2)
⊢ (cycleGraph (n + 2)).degree v = {v - 1, v + 1}.card

Tactic:
rw [SimpleGraph.degree, cycleGraph_neighborFinset]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_inv_eq_of_eq_mul (h : a = c * b) : a * b⁻¹ = c

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : a = c * b
⊢ a * b⁻¹ = c

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_eq_symm (hy : y ≤ x) (h : x \ y = z) : x \ z = y

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hy : y ≤ x
h : x \ y = z
⊢ x \ z = y

Tactic:
rw [← h, sdiff_sdiff_eq_self hy]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem integral_radius_zero (f : ℂ → E) (c : ℂ) : (∮ z in C(c, 0), f z) = 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
⊢ (∮ (z : ℂ) in C(c, 0), f z) = 0

Tactic:
simp (config := { unfoldPartialApp := true }) [circleIntegral, const]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem and_self_left  : a ∧ (a ∧ b) ↔ a ∧ b

Proof state:
a b : Prop
⊢ a ∧ a ∧ b ↔ a ∧ b

Tactic:
rw [←propext and_assoc, and_self]

Result:
no goals
-- Mathlib/Data/Finsupp/MonomialOrder.lean
lemma toSyn_strictMono : StrictMono (m.toSyn)

Proof state:
σ : Type u_1
m : MonomialOrder σ
⊢ StrictMono ⇑m.toSyn

Tactic:
apply m.toSyn_monotone.strictMono_of_injective m.toSyn.injective

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem Reachable.pos_dist_of_ne (h : G.Reachable u v) (hne : u ≠ v) :
    0 < G.dist u v :=
  Nat.pos_of_ne_zero (by simp [h, hne])

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
h : G.Reachable u v
hne : u ≠ v
⊢ G.dist u v ≠ 0

Tactic:
simp [h, hne]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.self_eq_add_left (a b : BitVec w) : (a == b + a) = (b == 0#w)

Proof state:
w : Nat
a b : BitVec w
⊢ (a == b + a) = (b == 0#w)

Tactic:
rw [Bool.eq_iff_iff]

Result:
w : Nat
a b : BitVec w
⊢ (a == b + a) = true ↔ (b == 0#w) = true

Proof state:
w : Nat
a b : BitVec w
⊢ (a == b + a) = true ↔ (b == 0#w) = true

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_C_mul (p : R[X]) (ha : a ≠ 0) : (C a * p).roots = p.roots

Proof state:
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
ha : a ≠ 0
⊢ (C a * p).roots = p.roots

Tactic:
by_cases hp : p = 0 <;>
  simp only [roots_mul, *, Ne, mul_eq_zero, C_eq_zero, or_self_iff, not_false_iff, roots_C,
    zero_add, mul_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem monic_of_injective (hf : Injective f) {p : R[X]} (hp : (p.map f).Monic) : p.Monic

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
hp : (map f p).Monic
⊢ p.Monic

Tactic:
apply hf

Result:
case a
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
hp : (map f p).Monic
⊢ f p.leadingCoeff = f 1

Proof state:
case a
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
hp : (map f p).Monic
⊢ f p.leadingCoeff = f 1

Tactic:
rw [← leadingCoeff_of_injective hf, hp.leadingCoeff, f.map_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
    (m.insert k v).isEmpty = false

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ (m.insert k v).isEmpty = false

Tactic:
simp_to_raw using Raw₀.isEmpty_insert

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_has_biproduct₁ [HasBinaryBiproduct X Y] :
    BicartesianSq biprod.fst biprod.snd (0 : X ⟶ 0) (0 : Y ⟶ 0)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproduct X Y
⊢ BicartesianSq biprod.fst biprod.snd 0 0

Tactic:
convert of_is_biproduct₁ (BinaryBiproduct.isBilimit X Y)

Result:
no goals
-- Mathlib/RingTheory/Derivation/Basic.lean
theorem map_algebraMap : D (algebraMap R A r) = 0

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
r : R
⊢ D ((algebraMap R A) r) = 0

Tactic:
rw [← mul_one r, RingHom.map_mul, RingHom.map_one, ← smul_def, map_smul, map_one_eq_zero,
  smul_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem measure_eq (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) :
    μ s = μ t

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
⊢ μ s = μ t

Tactic:
simpa only [setLIntegral_one] using hs.setLIntegral_eq ht (fun _ => 1) fun _ _ => rfl

Result:
no goals
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Ioo_succ_right_eq_Ioc_of_not_isMax (hb : ¬ IsMax b) (a : α) : Ioo a (succ b) = Ioc a b

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ x ∈ Ioo a (succ b) ↔ x ∈ Ioc a b

Tactic:
rw [mem_Ioo, mem_Ioc, lt_succ_iff_of_not_isMax hb]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ioo a (succ b) = Ioc a b

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ x ∈ Ioo a (succ b) ↔ x ∈ Ioc a b
-- Mathlib/Analysis/NormedSpace/ConformalLinearMap.lean
theorem isConformalMap_of_subsingleton [Subsingleton M] (f' : M →L[R] N) : IsConformalMap f' :=
  ⟨1, one_ne_zero, ⟨0, fun x => by simp [Subsingleton.elim x 0]⟩, Subsingleton.elim _ _⟩

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : NormedField R
inst✝⁴ : SeminormedAddCommGroup M
inst✝³ : SeminormedAddCommGroup N
inst✝² : NormedSpace R M
inst✝¹ : NormedSpace R N
inst✝ : Subsingleton M
f' : M →L[R] N
x : M
⊢ ‖0 x‖ = ‖x‖

Tactic:
simp [Subsingleton.elim x 0]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lt_mul_div_add (a) {b : Ordinal} (h : b ≠ 0) : a < b * (a / b) + b

Proof state:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * (a / b) + b

Tactic:
simpa only [mul_succ] using lt_mul_succ_div a h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Iso.lean
@[reassoc (attr := simp)]
lemma pushout_inl_inv_inr_of_right_isIso :
    pushout.inl f g ≫ inv (pushout.inr f g) = inv f ≫ g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ pushout.inl f g ≫ inv (pushout.inr f g) = inv f ≫ g

Tactic:
rw [IsIso.eq_inv_comp, pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem eq_zero_iff_ae_eq_zero {f : Lp E p μ} : f = 0 ↔ f =ᵐ[μ] 0

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
⊢ f = 0 ↔ ↑↑f =ᶠ[ae μ] 0

Tactic:
rw [← (Lp.memLp f).toLp_eq_toLp_iff MemLp.zero, MemLp.toLp_zero, toLp_coeFn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem allOnes_and {x : BitVec w} : allOnes w &&& x = x

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (allOnes w &&& x).getLsbD i = x.getLsbD i

Tactic:
simp [h]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ allOnes w &&& x = x

Tactic:
ext i h

Result:
case pred
w : Nat
x : BitVec w
i : Nat
h : i < w
⊢ (allOnes w &&& x).getLsbD i = x.getLsbD i
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma hom_inv_apply {R S : CommRingCat} (e : R ≅ S) (s : S) : e.hom (e.inv s) = s

Proof state:
R S : CommRingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_sin' {x : ℝ} (hx : x ∈ Icc (-(π / 2)) (π / 2)) : arcsin (sin x) = x :=
  injOn_sin (arcsin_mem_Icc _) hx <| by rw [sin_arcsin (neg_one_le_sin _) (sin_le_one _)]

Proof state:
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ sin (arcsin (sin x)) = sin x

Tactic:
rw [sin_arcsin (neg_one_le_sin _) (sin_le_one _)]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Inversion/ImageHyperplane.lean
theorem image_inversion_sphere_dist_center (hR : R ≠ 0) (hy : y ≠ c) :
    inversion c R '' sphere y (dist y c) = insert c (perpBisector c (inversion c R y) : Set P)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R '' sphere y (dist y c) = insert c ↑(perpBisector c (inversion c R y))

Tactic:
rw [image_eq_preimage_of_inverse (inversion_involutive _ hR) (inversion_involutive _ hR),
  preimage_inversion_sphere_dist_center hR hy]

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
@[simp] lemma mem_Ici : x ∈ Ici a ↔ a ≤ x

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ici a ↔ a ≤ x

Tactic:
rw [Ici, ← Finset.mem_def, Finset.mem_Ici]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {i : Nat} :
    xs.findIdx? p = some i ↔
      ∃ h : i < xs.size, p xs[i] ∧ ∀ j (hji : j < i), ¬p (xs[j]'(Nat.lt_trans hji h))

Proof state:
case mk
α : Type u_1
p : α → Bool
i : Nat
xs : List α
⊢ findIdx? p { toList := xs } = some i ↔
    ∃ h, p { toList := xs }[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p { toList := xs }[j] = true

Tactic:
simp [List.findIdx?_eq_some_iff_getElem]

Result:
no goals

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
i : Nat
⊢ findIdx? p xs = some i ↔ ∃ h, p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
i : Nat
xs : List α
⊢ findIdx? p { toList := xs } = some i ↔
    ∃ h, p { toList := xs }[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p { toList := xs }[j] = true
-- Mathlib/SetTheory/Nimber/Field.lean
theorem add_mul (a b c : Nimber) : (a + b) * c = a * c + b * c

Proof state:
a b c : Nimber
⊢ (a + b) * c = a * c + b * c

Tactic:
rw [Nimber.mul_comm, Nimber.mul_add, Nimber.mul_comm, Nimber.mul_comm b]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Span.lean
theorem span_zero : span (0 : Set α) = ⊥

Proof state:
α : Type u
inst✝ : Semiring α
⊢ span 0 = ⊥

Tactic:
rw [← Set.singleton_zero, span_singleton_eq_bot]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem le_refl (a : Fin n) : a ≤ a

Proof state:
n : Nat
a : Fin n
⊢ a ≤ a

Tactic:
simp [le_def]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive (attr := simp)] lemma inv_mul_cancel_comm (a b : G) : a⁻¹ * b * a = b

Proof state:
G : Type u_1
inst✝ : CommGroup G
a b : G
⊢ a⁻¹ * b * a = b

Tactic:
rw [mul_comm, mul_inv_cancel_left]

Result:
no goals