harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem map_srange (g : S →ₙ+* T) (f : R →ₙ+* S) : map g (srange f) = srange (g.comp f)

Proof state:
R : Type u
S : Type v
T : Type w
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
g : S →ₙ+* T
f : R →ₙ+* S
⊢ map g (srange f) = srange (g.comp f)

Tactic:
simpa only [srange_eq_map] using (⊤ : NonUnitalSubsemiring R).map_map g f

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_mul_I : cosh (x * I) = cos x

Proof state:
x : ℂ
⊢ cosh (x * I) = cos x

Tactic:
rw [← mul_right_inj' (two_ne_zero' ℂ), two_cosh, two_cos, neg_mul_eq_neg_mul]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem isUnit_iff_singleton : IsUnit s ↔ ∃ a, s = {a}

Proof state:
α : Type u_2
inst✝ : Group α
s : Set α
⊢ IsUnit s ↔ ∃ a, s = {a}

Tactic:
simp only [isUnit_iff, Group.isUnit, and_true]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get?_range {m n : Nat} (h : m < n) : get? (range n) m = some m

Proof state:
m n : Nat
h : m < n
⊢ (range n).get? m = some m

Tactic:
simp [getElem?_range, h]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem image_seq {f : β → γ} {s : Set (α → β)} {t : Set α} :
    f '' seq s t = seq ((f ∘ ·) '' s) t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
s : Set (α → β)
t : Set α
⊢ f '' s.seq t = ((fun x => f ∘ x) '' s).seq t

Tactic:
simp only [seq, image_image2, image2_image_left, comp_apply]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
@[simp] lemma coprod_add (f₁ g₁ : M₁ →L[R] M) (f₂ g₂ : M₂ →L[R] M) :
    (f₁ + g₁).coprod (f₂ + g₂) = f₁.coprod f₂ + g₁.coprod g₂

Proof state:
R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst✝¹⁰ : Semiring R
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f₁ g₁ : M₁ →L[R] M
f₂ g₂ : M₂ →L[R] M
⊢ (f₁ + g₁).coprod (f₂ + g₂) = f₁.coprod f₂ + g₁.coprod g₂

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedSeries_baseChange {A : Type*} [CommRing A] [Algebra R A] (k : ℕ) :
    derivedSeries A (A ⊗[R] L) k = (derivedSeries R L k).baseChange A

Proof state:
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
k : ℕ
⊢ derivedSeries A (A ⊗[R] L) k = LieSubmodule.baseChange A (derivedSeries R L k)

Tactic:
rw [derivedSeries_def, derivedSeries_def, ← derivedSeriesOfIdeal_baseChange,
  LieSubmodule.baseChange_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast!_insertList_of_contains_eq_false [BEq α] [LawfulBEq α]
    {l toInsert : List ((a : α) × β a)} {k : α} [Inhabited (β k)]
    (not_contains : (toInsert.map Sigma.fst).contains k = false) :
    getValueCast! k (insertList l toInsert) = getValueCast! k l

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k : α
inst✝ : Inhabited (β k)
not_contains : (List.map Sigma.fst toInsert).contains k = false
⊢ getValueCast! k (insertList l toInsert) = getValueCast! k l

Tactic:
rw [getValueCast!_eq_getValueCast?, getValueCast!_eq_getValueCast?,
  getValueCast?_insertList_of_contains_eq_false not_contains]

Result:
no goals
-- Mathlib/LinearAlgebra/Contraction.lean
theorem dualTensorHomEquivOfBasis_symm_cancel_right (x : M →ₗ[R] N) :
    dualTensorHom R M N ((dualTensorHomEquivOfBasis b).symm x) = x

Proof state:
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
x : M →ₗ[R] N
⊢ (dualTensorHom R M N) ((dualTensorHomEquivOfBasis b).symm x) = x

Tactic:
rw [← dualTensorHomEquivOfBasis_apply b, LinearEquiv.apply_symm_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem bnot_isLeft (x : α ⊕ β) : !x.isLeft = x.isRight

Proof state:
α : Type u_1
β : Type u_2
x : α ⊕ β
⊢ (!decide (x.isLeft = x.isRight)) = true

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Basic.lean
theorem of_left_adjoint {L : C ⥤ D} {R : D ⥤ C} (h : L ⊣ R) : IsCofilteredOrEmpty D :=
  { cone_objs := fun X Y =>
      ⟨L.obj (min (R.obj X) (R.obj Y)), (h.homEquiv _ X).symm (minToLeft _ _),
        (h.homEquiv _ Y).symm (minToRight _ _), ⟨⟩⟩
    cone_maps := fun X Y f g =>
      ⟨L.obj (eq (R.map f) (R.map g)), (h.homEquiv _ _).symm (eqHom _ _), by
        rw [← h.homEquiv_naturality_right_symm, ← h.homEquiv_naturality_right_symm, eq_condition]⟩ }

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsCofilteredOrEmpty C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ (h.homEquiv (eq (R.map f) (R.map g)) X).symm (eqHom (R.map f) (R.map g)) ≫ f =
    (h.homEquiv (eq (R.map f) (R.map g)) X).symm (eqHom (R.map f) (R.map g)) ≫ g

Tactic:
rw [← h.homEquiv_naturality_right_symm, ← h.homEquiv_naturality_right_symm, eq_condition]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Sequence.lean
/-- `S i` has strictly monotone degree. -/
lemma degree_strictMono : StrictMono <| degree ∘ S := fun _ _  ↦ by simp

Proof state:
R : Type u_1
inst✝ : Semiring R
S : Sequence R
x✝¹ x✝ : ℕ
⊢ x✝¹ < x✝ → (degree ∘ ↑S) x✝¹ < (degree ∘ ↑S) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_eq_self (h : s ⊆ t) : μ.restrict t s = μ s :=
  (le_iff'.1 restrict_le_self s).antisymm <|
    calc
      μ s ≤ μ (toMeasurable (μ.restrict t) s ∩ t) :=
        measure_mono (subset_inter (subset_toMeasurable _ _) h)
      _ = μ.restrict t s

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ⊆ t
⊢ μ (toMeasurable (μ.restrict t) s ∩ t) = (μ.restrict t) s

Tactic:
rw [← restrict_apply (measurableSet_toMeasurable _ _), measure_toMeasurable]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
@[simp] lemma map_nnratCast [DivisionSemiring α] [DivisionSemiring β] [RingHomClass F α β] (f : F)
    (q : ℚ≥0) : f q = q

Proof state:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionSemiring α
inst✝¹ : DivisionSemiring β
inst✝ : RingHomClass F α β
f : F
q : ℚ≥0
⊢ f ↑q = ↑q

Tactic:
simp_rw [NNRat.cast_def, map_div₀, map_natCast]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem tendsto_iff_dist_tendsto_zero {f : β → α} {x : Filter β} {a : α} :
    Tendsto f x (𝓝 a) ↔ Tendsto (fun b => dist (f b) a) x (𝓝 0)

Proof state:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
x : Filter β
a : α
⊢ Tendsto f x (𝓝 a) ↔ Tendsto (fun b => dist (f b) a) x (𝓝 0)

Tactic:
rw [← nhds_comap_dist a, tendsto_comap_iff, Function.comp_def]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
lemma Topology.isEmbedding_sigmaMap {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)}
    (h : Injective f₁) : IsEmbedding (Sigma.map f₁ f₂) ↔ ∀ i, IsEmbedding (f₂ i)

Proof state:
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h : Injective f₁
⊢ IsEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsEmbedding (f₂ i)

Tactic:
simp only [isEmbedding_iff, Injective.sigma_map, isInducing_sigmaMap h, forall_and,
  h.sigma_map_iff]

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem erase_erase {a a' : α} {s : Finmap β} : erase a (erase a' s) = erase a' (erase a s) :=
  induction_on s fun s => ext (by simp only [AList.erase_erase, erase_toFinmap])

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s✝ : Finmap β
s : AList β
⊢ (erase a (erase a' ⟦s⟧)).entries = (erase a' (erase a ⟦s⟧)).entries

Tactic:
simp only [AList.erase_erase, erase_toFinmap]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_eq_iInf_iSup_of_nat' {u : ℕ → α} : limsup u atTop = ⨅ n : ℕ, ⨆ i : ℕ, u (i + n)

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ limsup u atTop = ⨅ n, ⨆ i, u (i + n)

Tactic:
simp only [limsup_eq_iInf_iSup_of_nat, iSup_ge_eq_iSup_nat_add]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp] lemma sectL_zero (b : β) : sectL (0 : Kernel (α × β) γ) b = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
b : β
⊢ sectL 0 b = 0

Tactic:
simp [sectL]

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem toReal_natCast (n : ℕ) : (n : ℝ≥0∞).toReal = n

Proof state:
n : ℕ
⊢ (↑n).toReal = ↑n

Tactic:
rw [← ENNReal.ofReal_natCast n, ENNReal.toReal_ofReal (Nat.cast_nonneg _)]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem integrable_iff_mem_L1 {f : α →ₘ[μ] β} : Integrable f ↔ f ∈ (α →₁[μ] β)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α →ₘ[μ] β
⊢ f.Integrable ↔ f ∈ Lp β 1 μ

Tactic:
rw [← integrable_coeFn, ← memLp_one_iff_integrable, Lp.mem_Lp_iff_memLp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_ofList [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} {k : α} :
    k ∈ ofList l ↔ (l.map Prod.fst).contains k

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k : α
⊢ k ∈ ofList l ↔ (List.map Prod.fst l).contains k = true

Tactic:
simp [mem_iff_contains]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma nonsingular_of_Z_eq_zero {P : Fin 3 → R} (hPz : P z = 0) :
    W'.Nonsingular P ↔ W'.Equation P ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W'.a₁ * P x * P y ≠ 0)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.Nonsingular P ↔ W'.Equation P ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W'.a₁ * P x * P y ≠ 0)

Tactic:
simp only [nonsingular_iff, hPz, add_zero, sub_zero, zero_sub, mul_zero,
  zero_pow <| OfNat.ofNat_ne_zero _, neg_ne_zero]

Result:
no goals
-- Mathlib/Algebra/Regular/Basic.lean
theorem IsLeftRegular.of_mul (ab : IsLeftRegular (a * b)) : IsLeftRegular b :=
  Function.Injective.of_comp (f := (a * ·)) (by rwa [comp_mul_left a b])

Proof state:
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsLeftRegular (a * b)
⊢ Function.Injective ((fun x => a * x) ∘ fun x => b * x)

Tactic:
rwa [comp_mul_left a b]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem push_eq_append_iff {a b c : Array α} {x : α} :
    c.push x = a ++ b ↔ (b = #[] ∧ a = c.push x) ∨ (∃ b', b = b'.push x ∧ c = a ++ b')

Proof state:
α : Type u_1
a b c : Array α
x : α
⊢ c.push x = a ++ b ↔ b = #[] ∧ a = c.push x ∨ ∃ b', b = b'.push x ∧ c = a ++ b'

Tactic:
rw [eq_comm, append_eq_push_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.map_comp_id {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryProduct X W]
    [HasBinaryProduct Z W] [HasBinaryProduct Y W] :
    prod.map (f ≫ g) (𝟙 W) = prod.map f (𝟙 W) ≫ prod.map g (𝟙 W)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝² : HasBinaryProduct X W
inst✝¹ : HasBinaryProduct Z W
inst✝ : HasBinaryProduct Y W
⊢ map (f ≫ g) (𝟙 W) = map f (𝟙 W) ≫ map g (𝟙 W)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
lemma dens_union_add_dens_inter (s t : Finset α) :
    dens (s ∪ t) + dens (s ∩ t) = dens s + dens t

Proof state:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∪ t).dens + (s ∩ t).dens = s.dens + t.dens

Tactic:
simp_rw [dens, ← add_div, ← Nat.cast_add, card_union_add_card_inter]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
@[simp]
lemma dist_bot : (⊥ : SimpleGraph V).dist u v = 0

Proof state:
V : Type u_1
u v : V
⊢ ⊥.dist u v = 0

Tactic:
by_cases h : u = v <;> simp [h]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem cons_rev {α n} (a : α) (f : Fin n → α) (i : Fin <| n + 1) :
    cons (α := fun _ => α) a f i.rev = snoc (α := fun _ => α) (f ∘ Fin.rev : Fin _ → α) a i

Proof state:
α : Sort u_3
n : ℕ
a : α
f : Fin n → α
i : Fin (n + 1)
⊢ cons a f i.rev = snoc (f ∘ rev) a i

Tactic:
simpa using insertNth_rev 0 a f i

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem right_unitality_hom (X : C) :
    δ F X (𝟙_ C) ≫ F.obj X ◁ η F ≫ (ρ_ (F.obj X)).hom = F.map (ρ_ X).hom

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ δ F X (𝟙_ C) ≫ F.obj X ◁ η F ≫ (ρ_ (F.obj X)).hom = F.map (ρ_ X).hom

Tactic:
rw [← Category.assoc, ← Iso.eq_comp_inv, right_unitality, ← Category.assoc,
  ← F.map_comp, Iso.hom_inv_id, F.map_id, id_comp]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Defs.lean
theorem finsuppProdLEquiv_symm_apply {α β R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
    (f : α →₀ β →₀ M) (xy) : (finsuppProdLEquiv R).symm f xy = f xy.1 xy.2

Proof state:
α : Type u_7
β : Type u_8
R : Type u_9
M : Type u_10
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α →₀ β →₀ M
xy : α × β
⊢ ((finsuppProdLEquiv R).symm f) xy = (f xy.1) xy.2

Tactic:
conv_rhs =>
  rw [← (finsuppProdLEquiv R).apply_symm_apply f, finsuppProdLEquiv_apply]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma max_neg_neg (x y : EReal) : max (-x) (-y) = -min x y

Proof state:
x y : EReal
⊢ -x ⊔ -y = -(x ⊓ y)

Tactic:
rcases le_total x y with (h | h) <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_alter [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} (h : m.WF) :
    (m.alter k f).contains k' = if k == k' then (f (m.get? k)).isSome else m.contains k'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).contains k' = if (k == k') = true then (f (m.get? k)).isSome else m.contains k'

Tactic:
simp_to_raw using Raw₀.contains_alter

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
theorem posLog_add {a b : ℝ} : log⁺ (a + b) ≤ log 2 + log⁺ a + log⁺ b

Proof state:
a b : ℝ
⊢ log⁺ (a + b) ≤ log 2 + log⁺ a + log⁺ b

Tactic:
convert posLog_sum Finset.univ ![a, b] using 1 <;> simp [add_assoc]

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
@[simp] lemma indepFun_zero_left {β γ} [MeasurableSpace β] [MeasurableSpace γ]
    {f : Ω → β} {g : Ω → γ} : IndepFun f g (0 : Kernel α Ω) μ

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
μ : Measure α
β : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
⊢ IndepFun f g 0 μ

Tactic:
simp [IndepFun]

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
lemma inv_apply' (ψ : AddChar A M) (a : A) : ψ⁻¹ a = (ψ a)⁻¹

Proof state:
A : Type u_1
M : Type u_2
inst✝¹ : AddCommGroup A
inst✝ : DivisionCommMonoid M
ψ : AddChar A M
a : A
⊢ ψ⁻¹ a = (ψ a)⁻¹

Tactic:
rw [inv_apply, map_neg_eq_inv]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_concat : (l.concat a).prod = l.prod * a

Proof state:
M : Type u_4
inst✝ : Monoid M
l : List M
a : M
⊢ (l.concat a).prod = l.prod * a

Tactic:
rw [concat_eq_append, prod_append, prod_singleton]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem mem_aroots' [CommRing S] [IsDomain S] [Algebra T S] {p : T[X]} {a : S} :
    a ∈ p.aroots S ↔ p.map (algebraMap T S) ≠ 0 ∧ aeval a p = 0

Proof state:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
p : T[X]
a : S
⊢ a ∈ p.aroots S ↔ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0

Tactic:
rw [mem_roots', IsRoot.def, ← eval₂_eq_eval_map, aeval_def]

Result:
no goals
-- Mathlib/Computability/TMConfig.lean
theorem comp_eval (f g) : (comp f g).eval = fun v => g.eval v >>= f.eval

Proof state:
f g : Code
⊢ (f.comp g).eval = fun v => g.eval v >>= f.eval

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem flip_bijective_iff₁ [FiniteDimensional K V₁] : Bijective B.flip ↔ Bijective B

Proof state:
K : Type uK
inst✝⁵ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : FiniteDimensional K V₁
⊢ Bijective ⇑B.flip ↔ Bijective ⇑B

Tactic:
simp_rw [Bijective, flip_injective_iff₁, flip_surjective_iff₁, and_comm]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem restrictScalars_sup :
    L.restrictScalars K ⊔ L'.restrictScalars K = (L ⊔ L').restrictScalars K :=
  toSubfield_injective (by simp)

Proof state:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra K E
inst✝¹ : Algebra K F
inst✝ : IsScalarTower K F E
L L' : IntermediateField F E
⊢ (restrictScalars K L ⊔ restrictScalars K L').toSubfield = (restrictScalars K (L ⊔ L')).toSubfield

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insertManyIfNewUnit_list_of_contains [EquivBEq α] [LawfulHashable α]
    [Inhabited α] (h : m.1.WF) {l : List α} {k : α} :
    m.contains k → getKey! (insertManyIfNewUnit m l).1 k = getKey! m k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw₀ α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
l : List α
k : α
⊢ m.contains k = true → (insertManyIfNewUnit m l).val.getKey! k = m.getKey! k

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.getKey!_insertListIfNewUnit_of_contains

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_eq_toFinset_card (s : Set α) (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
⊢ s.ncard = (Finite.toFinset hs).card

Tactic:
rw [← Nat.card_coe_set_eq, @Nat.card_eq_fintype_card _ hs.fintype,
  @Finite.card_toFinset _ _ hs.fintype hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_cons_head [LawfulBEq α] (a : α) (l : List α) : (a :: l).erase a = l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ (a :: l).erase a = l

Tactic:
simp [erase_cons]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem findSome?_succ_of_isNone {f : Fin (n+1) → Option α} (h : (f 0).isNone) :
    findSome? f = findSome? fun i => f i.succ

Proof state:
n : Nat
α : Type u_1
f : Fin (n + 1) → Option α
h : (f 0).isNone = true
⊢ findSome? f = findSome? fun i => f i.succ

Tactic:
simp_all [findSome?_succ_of_none]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem algebraMap_eval_U [Algebra R R'] (x : R) (n : ℤ) :
    algebraMap R R' ((U R n).eval x) = (U R' n).eval (algebraMap R R' x)

Proof state:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R
n : ℤ
⊢ (algebraMap R R') (eval x (U R n)) = eval ((algebraMap R R') x) (U R' n)

Tactic:
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_U]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem IsRotated.trans : ∀ {l l' l'' : List α}, l ~r l' → l' ~r l'' → l ~r l''
  | _, _, _, ⟨n, rfl⟩, ⟨m, rfl⟩ => ⟨n + m, by rw [rotate_rotate]⟩

Proof state:
α : Type u
l✝ : List α
n m : ℕ
⊢ l✝.rotate (n + m) = (l✝.rotate n).rotate m

Tactic:
rw [rotate_rotate]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lt_limit {o} (h : IsLimit o) {a} : a < o ↔ ∃ x < o, a < x

Proof state:
o : Ordinal.{u_4}
h : o.IsLimit
a : Ordinal.{u_4}
⊢ a < o ↔ ∃ x < o, a < x

Tactic:
simpa only [not_forall₂, not_le, bex_def] using not_congr (@limit_le _ h a)

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem IsAlgebraic.algebraMap {a : S} :
    IsAlgebraic R a → IsAlgebraic R (algebraMap S A a) := fun ⟨f, hf₁, hf₂⟩ =>
  ⟨f, hf₁, by rw [aeval_algebraMap_apply, hf₂, map_zero]⟩

Proof state:
R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
a : S
x✝ : IsAlgebraic R a
f : R[X]
hf₁ : f ≠ 0
hf₂ : (aeval a) f = 0
⊢ (aeval ((algebraMap S A) a)) f = 0

Tactic:
rw [aeval_algebraMap_apply, hf₂, map_zero]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma div_div_div_cancel_left' (a b : G₀) (hc : c ≠ 0) : c / a / (c / b) = b / a

Proof state:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
c a b : G₀
hc : c ≠ 0
⊢ c / a / (c / b) = b / a

Tactic:
rw [div_div_div_eq, mul_comm, mul_div_mul_right _ _ hc]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalComplement_eq_orthogonalComplement {L : Submodule 𝕜 E} [HasOrthogonalProjection K]
    [HasOrthogonalProjection L] : Kᗮ = Lᗮ ↔ K = L :=
  ⟨fun h ↦ by simpa using congr(Submodule.orthogonal $(h)),
    fun h ↦ congr(Submodule.orthogonal $(h))⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
K L : Submodule 𝕜 E
inst✝¹ : HasOrthogonalProjection K
inst✝ : HasOrthogonalProjection L
h : Kᗮ = Lᗮ
⊢ K = L

Tactic:
simpa using congr(Submodule.orthogonal $(h))

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem restrictScalars_injective :
    Function.Injective (restrictScalars K : IntermediateField L' L → IntermediateField K L) :=
  fun U V H => ext fun x => by rw [← mem_restrictScalars K, H, mem_restrictScalars]

Proof state:
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field L'
inst✝³ : Algebra K L
inst✝² : Algebra K L'
inst✝¹ : Algebra L' L
inst✝ : IsScalarTower K L' L
U V : IntermediateField L' L
H : restrictScalars K U = restrictScalars K V
x : L
⊢ x ∈ U ↔ x ∈ V

Tactic:
rw [← mem_restrictScalars K, H, mem_restrictScalars]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Real.lean
theorem frontier_closedBall' (x : E) (r : ℝ) : frontier (closedBall x r) = sphere x r

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ frontier (closedBall x r) = sphere x r

Tactic:
rw [frontier, closure_closedBall, interior_closedBall' x r, closedBall_diff_ball]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean
theorem ordinaryHypergeometricSeries_apply_eq (x : 𝔸) (n : ℕ) :
    (ordinaryHypergeometricSeries 𝔸 a b c n fun _ => x) =
      ((n !⁻¹ : 𝕂) * (ascPochhammer 𝕂 n).eval a * (ascPochhammer 𝕂 n).eval b *
        ((ascPochhammer 𝕂 n).eval c)⁻¹ ) • x ^ n

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
x : 𝔸
n : ℕ
⊢ ((ordinaryHypergeometricSeries 𝔸 a b c n) fun x_1 => x) =
    ((↑n !)⁻¹ * Polynomial.eval a (ascPochhammer 𝕂 n) * Polynomial.eval b (ascPochhammer 𝕂 n) *
        (Polynomial.eval c (ascPochhammer 𝕂 n))⁻¹) •
      x ^ n

Tactic:
rw [ordinaryHypergeometricSeries, ofScalars_apply_eq]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ResidueField.lean
lemma evaluation_ne_zero_iff_mem_basicOpen (x : X) (hx : x ∈ U) (f : Γ(X, U)) :
    X.evaluation U x hx f ≠ 0 ↔ x ∈ X.basicOpen f

Proof state:
X : Scheme
U : X.Opens
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
⊢ (ConcreteCategory.hom (X.evaluation U x hx)) f ≠ 0 ↔ x ∈ X.basicOpen f

Tactic:
simp

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_eq_sup_sdiff_inf : a ∆ b = (a ⊔ b) \ (a ⊓ b)

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ a ∆ b = (a ⊔ b) \ (a ⊓ b)

Tactic:
simp [sup_sdiff, symmDiff]

Result:
no goals