harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/Deriv/Shift.lean
/-- Translation in the domain does not change the derivative. -/
lemma HasDerivAt.comp_sub_const (x a : 𝕜) (hf : HasDerivAt f f' (x - a)) :
    HasDerivAt (fun x ↦ f (x - a)) f' x

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x a : 𝕜
hf : HasDerivAt f f' (x - a)
⊢ HasDerivAt (fun x => f (x - a)) f' x

Tactic:
simpa [Function.comp_def] using HasDerivAt.scomp (𝕜 := 𝕜) x hf <| hasDerivAt_id' x |>.sub_const a

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma neg_sub {x y : EReal} (h1 : x ≠ ⊥ ∨ y ≠ ⊥) (h2 : x ≠ ⊤ ∨ y ≠ ⊤) :
    - (x - y) = - x + y

Proof state:
x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ -(x - y) = -x + y

Tactic:
rw [sub_eq_add_neg, neg_add _ _, sub_eq_add_neg, neg_neg] <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_X_sub_pow_self (n : ℕ) (c : R) :
    derivative^[n] ((X - C c) ^ n) = n.factorial

Proof state:
R : Type u
inst✝ : CommRing R
n : ℕ
c : R
⊢ (⇑derivative)^[n] ((X - C c) ^ n) = ↑n !

Tactic:
rw [iterate_derivative_X_sub_pow, n.sub_self, pow_zero, nsmul_one, n.descFactorial_self]

Result:
no goals
-- Mathlib/CategoryTheory/IsConnected.lean
theorem nonempty_hom_of_preconnected_groupoid {G} [Groupoid G] [IsPreconnected G] :
    ∀ x y : G, Nonempty (x ⟶ y)

Proof state:
G : Type u_1
inst✝¹ : Groupoid G
inst✝ : IsPreconnected G
⊢ ∀ (x y : G), Nonempty (x ⟶ y)

Tactic:
refine equiv_relation _ ?_ fun {j₁ j₂} => Nonempty.intro

Result:
G : Type u_1
inst✝¹ : Groupoid G
inst✝ : IsPreconnected G
⊢ _root_.Equivalence fun x y => Nonempty (x ⟶ y)
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem map_inl (n : N₁) : map fn fg h (inl n) = inl (fn n)

Proof state:
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ →* N₂
fg : G₁ →* G₂
h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
n : N₁
⊢ (map fn fg h) (inl n) = inl (fn n)

Tactic:
simp [map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_cons_none {f : α → Option β} {a : α} {l : List α} (h : f a = none) :
    filterMap f (a :: l) = filterMap f l

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
a : α
l : List α
h : f a = none
⊢ filterMap f (a :: l) = filterMap f l

Tactic:
simp only [filterMap, h]

Result:
no goals
-- Mathlib/LinearAlgebra/Trace.lean
lemma trace_mul_cycle (f g h : M →ₗ[R] M) :
    trace R M (f * g * h) = trace R M (h * f * g)

Proof state:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (f * g * h) = (trace R M) (h * f * g)

Tactic:
rw [LinearMap.trace_mul_comm, ← mul_assoc]

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
lemma iteratedDeriv_sub (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
    iteratedDeriv n (f - g) x = iteratedDeriv n f x - iteratedDeriv n g x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
f g : 𝕜 → F
hf : ContDiffAt 𝕜 (↑n) f x
hg : ContDiffAt 𝕜 (↑n) g x
⊢ iteratedDeriv n (f - g) x = iteratedDeriv n f x - iteratedDeriv n g x

Tactic:
simpa only [iteratedDerivWithin_univ] using
  iteratedDerivWithin_sub (Set.mem_univ _) uniqueDiffOn_univ hf hg

Result:
no goals
-- Mathlib/Computability/EpsilonNFA.lean
theorem evalFrom_append_singleton (S : Set σ) (x : List α) (a : α) :
    M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
x : List α
a : α
⊢ M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a

Tactic:
rw [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem diag_singleton : ({a} : Finset α).diag = {(a, a)}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ {a}.diag = {(a, a)}

Tactic:
rw [← product_sdiff_offDiag, offDiag_singleton, sdiff_empty, singleton_product_singleton]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
lemma isCompl_comap_subtype_of_isCompl_of_le {p q r : Submodule R M}
    (h₁ : IsCompl q r) (h₂ : q ≤ p) :
    IsCompl (q.comap p.subtype) (r.comap p.subtype)

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q r : Submodule R M
h₁ : IsCompl q r
h₂ : q ≤ p
⊢ IsCompl (comap p.subtype q) (comap p.subtype r)

Tactic:
simpa [p.mapIic.isCompl_iff, Iic.isCompl_iff] using Iic.isCompl_inf_inf_of_isCompl_of_le h₁ h₂

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
theorem inr_comp_pushoutSymmetry_inv [HasPushout f g] :
    pushout.inr _ _ ≫ (pushoutSymmetry f g).inv = pushout.inl _ _

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

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/Data/Matrix/Basic.lean
lemma entryLinearMap_eq_comp {i : m} {j : n} :
    entryLinearMap R α i j =
      LinearMap.proj j ∘ₗ LinearMap.proj i ∘ₗ (ofLinearEquiv R).symm.toLinearMap

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
i : m
j : n
⊢ entryLinearMap R α i j = LinearMap.proj j ∘ₗ LinearMap.proj i ∘ₗ ↑(ofLinearEquiv R).symm

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_C_mul_eq_of_mul_eq_one {ai : R} (au : ai * a = 1) :
    (C a * p).natDegree = p.natDegree :=
  le_antisymm (natDegree_C_mul_le a p)
    (calc
      p.natDegree = (1 * p).natDegree

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : ai * a = 1
⊢ (1 * p).natDegree = (C ai * (C a * p)).natDegree

Tactic:
rw [← C_1, ← au, RingHom.map_mul, ← mul_assoc]

Result:
no goals

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
ai : R
au : ai * a = 1
⊢ p.natDegree = (1 * p).natDegree

Tactic:
nth_rw 1 [← one_mul p]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
@[simp 1100, norm_cast]
lemma nnnorm_natCast (n : ℕ) : ‖(n : ℂ)‖₊ = n := Subtype.ext <| by simp

Proof state:
n : ℕ
⊢ ↑‖↑n‖₊ = ↑↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Homotopy/Basic.lean
theorem trans_apply {f₀ f₁ f₂ : C(X, Y)} (F : Homotopy f₀ f₁) (G : Homotopy f₁ f₂) (x : I × X) :
    (F.trans G) x =
      if h : (x.1 : ℝ) ≤ 1 / 2 then
        F (⟨2 * x.1, (unitInterval.mul_pos_mem_iff zero_lt_two).2 ⟨x.1.2.1, h⟩⟩, x.2)
      else
        G (⟨2 * x.1 - 1, unitInterval.two_mul_sub_one_mem_iff.2 ⟨(not_le.1 h).le, x.1.2.2⟩⟩, x.2) :=
  show ite _ _ _ = _ by
    split_ifs <;>
      · rw [extend, ContinuousMap.coe_IccExtend, Set.IccExtend_of_mem]
        rfl

Proof state:
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ¬↑x.1 ≤ 1 / 2
⊢ (G.curry ⟨2 * ↑x.1 - 1, ?neg.hx✝⟩) x.2 = G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)

case neg.hx
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ¬↑x.1 ≤ 1 / 2
⊢ 2 * ↑x.1 - 1 ∈ Set.Icc 0 1

Tactic:
rfl

Result:
no goals

Proof state:
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ¬↑x.1 ≤ 1 / 2
⊢ (G.extend (2 * ↑x.1 - 1)) x.2 = G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)

Tactic:
rw [extend, ContinuousMap.coe_IccExtend, Set.IccExtend_of_mem]

Result:
case neg
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ¬↑x.1 ≤ 1 / 2
⊢ (G.curry ⟨2 * ↑x.1 - 1, ?neg.hx✝⟩) x.2 = G (⟨2 * ↑x.1 - 1, ⋯⟩, x.2)

case neg.hx
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
h✝ : ¬↑x.1 ≤ 1 / 2
⊢ 2 * ↑x.1 - 1 ∈ Set.Icc 0 1
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem mem_nonMemberSubfamily : s ∈ 𝒜.nonMemberSubfamily a ↔ s ∈ 𝒜 ∧ a ∉ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ nonMemberSubfamily a 𝒜 ↔ s ∈ 𝒜 ∧ a ∉ s

Tactic:
simp [nonMemberSubfamily]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldlM_loop_eq [Monad m] (f : α → Fin n → m α) (x) : foldlM.loop n f x n = pure x

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝ : Monad m
f : α → Fin n → m α
x : α
⊢ foldlM.loop n f x n = pure x

Tactic:
rw [foldlM.loop, dif_neg (Nat.lt_irrefl _)]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem const_max (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => max a (f x)

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
Kf : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith Kf fun x => a ⊔ f x

Tactic:
simpa only [max_comm] using hf.max_const a

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem mk_preimage_prod_left_eq_if [DecidablePred (· ∈ t)] :
    (fun a => (a, b)) ⁻¹' s ×ˢ t = if b ∈ t then s else ∅

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
inst✝ : DecidablePred fun x => x ∈ t
⊢ (fun a => (a, b)) ⁻¹' s ×ˢ t = if b ∈ t then s else ∅

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem update_inl_apply_inl [DecidableEq α] [DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i j : α}
    {x : γ} : update f (inl i) x (inl j) = update (f ∘ inl) i x j

Proof state:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : α
x : γ
⊢ update f (inl i) x (inl j) = update (f ∘ inl) i x j

Tactic:
rw [← update_inl_comp_inl, Function.comp_apply]

Result:
no goals
-- Mathlib/Topology/Order/MonotoneConvergence.lean
theorem tendsto_atBot_ciInf (h_mono : Monotone f) (hbdd : BddBelow <| range f) :
    Tendsto f atBot (𝓝 (⨅ i, f i))

Proof state:
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : InfConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddBelow (range f)
⊢ Tendsto f atBot (𝓝 (⨅ i, f i))

Tactic:
convert tendsto_atTop_ciSup h_mono.dual hbdd.dual using 1

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem mono {p : α → α → Prop} (hp : ∀ a b, r a b → p a b) : ∀ {a b}, ReflGen r a b → ReflGen p a b
  | a, _, ReflGen.refl => by rfl
  | a, b, single h => single (hp a b h)

Proof state:
α : Type u_1
r p : α → α → Prop
hp : ∀ (a b : α), r a b → p a b
a : α
⊢ ReflGen p a a

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem comp_eq_mk (g : β → γ) (hg : Continuous g) (f : α →ₘ[μ] β) :
    comp g hg f = mk (g ∘ f) (hg.comp_aestronglyMeasurable f.aestronglyMeasurable)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ
hg : Continuous g
f : α →ₘ[μ] β
⊢ comp g hg f = mk (g ∘ ↑f) ⋯

Tactic:
rw [← comp_mk g hg f f.aestronglyMeasurable, mk_coeFn]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean
theorem center_eq_infi' (S : Set G) (hS : closure S = ⊤) :
    center G = ⨅ g : S, centralizer (zpowers (g : G))

Proof state:
G : Type u_1
inst✝ : Group G
S : Set G
hS : closure S = ⊤
⊢ center G = ⨅ g, centralizer ↑(zpowers ↑g)

Tactic:
rw [center_eq_iInf S hS, ← iInf_subtype'']

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem isSt_symm_real {r s : ℝ} : IsSt r s ↔ IsSt s r

Proof state:
r s : ℝ
⊢ (↑r).IsSt s ↔ (↑s).IsSt r

Tactic:
rw [isSt_real_iff_eq, isSt_real_iff_eq, eq_comm]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem SuperpolynomialDecay.mul_const [ContinuousMul β] (hf : SuperpolynomialDecay l k f) (c : β) :
    SuperpolynomialDecay l k fun n => f n * c := fun z => by
  simpa only [← mul_assoc, zero_mul] using Tendsto.mul_const c (hf z)

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
c : β
z : ℕ
⊢ Tendsto (fun a => k a ^ z * (fun n => f n * c) a) l (𝓝 0)

Tactic:
simpa only [← mul_assoc, zero_mul] using Tendsto.mul_const c (hf z)

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem bit_to_nat (b n) : (bit b n : ℕ) = Nat.bit b n

Proof state:
b : Bool
n : PosNum
⊢ ↑(bit b n) = Nat.bit b ↑n

Tactic:
cases b <;> simp [bit, two_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem separatingLeft_toLinearMap₂'_iff_det_ne_zero {M : Matrix ι ι R₁} :
    (Matrix.toLinearMap₂' R₁ M).SeparatingLeft (R := R₁) ↔ M.det ≠ 0

Proof state:
R₁ : Type u_2
ι : Type u_15
inst✝³ : CommRing R₁
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : IsDomain R₁
M : Matrix ι ι R₁
⊢ ((toLinearMap₂' R₁) M).SeparatingLeft ↔ M.det ≠ 0

Tactic:
rw [Matrix.separatingLeft_toLinearMap₂'_iff, Matrix.nondegenerate_iff_det_ne_zero]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem mem_comap_iff_compl : s ∈ comap f l ↔ (f '' sᶜ)ᶜ ∈ l

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
⊢ s ∈ comap f l ↔ (f '' sᶜ)ᶜ ∈ l

Tactic:
simp only [mem_comap'', kernImage_eq_compl]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompMap.lean
@[simp]
lemma id_comp (κ : Kernel α β) : Kernel.id ∘ₖ κ = κ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ Kernel.id ∘ₖ κ = κ

Tactic:
rw [Kernel.id, deterministic_comp_eq_map, map_id]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
@[simp]
lemma associated_sq [Invertible (2 : R)] : associated (R := R) sq = mul R R :=
  (associated_linMulLin (id) (id)).trans <|
    by simp only [smul_add, invOf_two_smul_add_invOf_two_smul]; rfl

Proof state:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ (mul R R).compl₁₂ LinearMap.id LinearMap.id = mul R R

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ ⅟2 • ((mul R R).compl₁₂ LinearMap.id LinearMap.id + (mul R R).compl₁₂ LinearMap.id LinearMap.id) = mul R R

Tactic:
simp only [smul_add, invOf_two_smul_add_invOf_two_smul]

Result:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ (mul R R).compl₁₂ LinearMap.id LinearMap.id = mul R R
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_def (n : ℕ) {p : ℕ} (pp : p.Prime) : n.factorization p = padicValNat p n

Proof state:
n p : ℕ
pp : Prime p
⊢ n.factorization p = padicValNat p n

Tactic:
simpa [factorization] using absurd pp

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma truncatedInf_sups_of_not_mem (ha : a ∉ upperClosure s ⊔ upperClosure t) :
    truncatedInf (s ⊻ t) a = ⊥ :=
  truncatedInf_of_not_mem <| by rwa [coe_sups, upperClosure_sups]

Proof state:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
ha : a ∉ upperClosure ↑s ⊔ upperClosure ↑t
⊢ a ∉ upperClosure ↑(s ⊻ t)

Tactic:
rwa [coe_sups, upperClosure_sups]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_polynomialZ : (W'.baseChange B).toJacobian.polynomialZ =
    MvPolynomial.map f (W'.baseChange A).toJacobian.polynomialZ

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (baseChange W' B).toJacobian.polynomialZ = (MvPolynomial.map ↑f) (baseChange W' A).toJacobian.polynomialZ

Tactic:
rw [← map_polynomialZ, map_baseChange]

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem length_sublists' : ∀ l : List α, length (sublists' l) = 2 ^ length l
  | [] => rfl
  | a :: l => by
    simp_arith only [sublists'_cons, length_append, length_sublists' l,
      length_map, length, Nat.pow_succ']

Proof state:
α : Type u
a : α
l : List α
⊢ (a :: l).sublists'.length = 2 ^ (a :: l).length

Tactic:
simp_arith only [sublists'_cons, length_append, length_sublists' l,
  length_map, length, Nat.pow_succ']

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem lt_emultiplicity_of_lt_multiplicity {n : ℕ} (h : n < multiplicity a b) :
    n < emultiplicity a b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : n < multiplicity a b
⊢ ↑n < emultiplicity a b

Tactic:
exact_mod_cast (WithTop.coe_strictMono h).trans_le multiplicity_le_emultiplicity

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem place_conjugate (φ : K →+* ℂ) : place (conjugate φ) = place φ

Proof state:
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
⊢ place (conjugate φ) = place φ

Tactic:
ext

Result:
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
x✝ : K
⊢ (place (conjugate φ)) x✝ = (place φ) x✝

Proof state:
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
x✝ : K
⊢ (place (conjugate φ)) x✝ = (place φ) x✝

Tactic:
simp only [place_apply, norm_conj, conjugate_coe_eq]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma lieBracket_add_right (hW : DifferentiableAt 𝕜 W x) (hW₁ : DifferentiableAt 𝕜 W₁ x) :
    lieBracket 𝕜 V (W + W₁) x =
      lieBracket 𝕜 V W x + lieBracket 𝕜 V W₁ x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
⊢ (fderiv 𝕜 W x) (V x) + (fderiv 𝕜 W₁ x) (V x) - ((fderiv 𝕜 V x) (W x) + (fderiv 𝕜 V x) (W₁ x)) =
    (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x) + ((fderiv 𝕜 W₁ x) (V x) - (fderiv 𝕜 V x) (W₁ x))

Tactic:
abel

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
⊢ lieBracket 𝕜 V (W + W₁) x = lieBracket 𝕜 V W x + lieBracket 𝕜 V W₁ x

Tactic:
simp only [lieBracket, Pi.add_apply, map_add]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
⊢ (fderiv 𝕜 (W + W₁) x) (V x) - ((fderiv 𝕜 V x) (W x) + (fderiv 𝕜 V x) (W₁ x)) =
    (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x) + ((fderiv 𝕜 W₁ x) (V x) - (fderiv 𝕜 V x) (W₁ x))

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
⊢ (fderiv 𝕜 (W + W₁) x) (V x) - ((fderiv 𝕜 V x) (W x) + (fderiv 𝕜 V x) (W₁ x)) =
    (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x) + ((fderiv 𝕜 W₁ x) (V x) - (fderiv 𝕜 V x) (W₁ x))

Tactic:
rw [fderiv_add' hW hW₁, ContinuousLinearMap.add_apply]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W W₁ : E → E
x : E
hW : DifferentiableAt 𝕜 W x
hW₁ : DifferentiableAt 𝕜 W₁ x
⊢ (fderiv 𝕜 W x) (V x) + (fderiv 𝕜 W₁ x) (V x) - ((fderiv 𝕜 V x) (W x) + (fderiv 𝕜 V x) (W₁ x)) =
    (fderiv 𝕜 W x) (V x) - (fderiv 𝕜 V x) (W x) + ((fderiv 𝕜 W₁ x) (V x) - (fderiv 𝕜 V x) (W₁ x))
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive sub_nsmul_nsmul_add]
lemma pow_sub_mul_pow (a : M) (h : m ≤ n) : a ^ (n - m) * a ^ m = a ^ n

Proof state:
M : Type u_4
inst✝ : Monoid M
m n : ℕ
a : M
h : m ≤ n
⊢ a ^ (n - m) * a ^ m = a ^ n

Tactic:
rw [← pow_add, Nat.sub_add_cancel h]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem isOpen_iff : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ball x ε ⊆ s

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ball x ε ⊆ s

Tactic:
simp only [isOpen_iff_mem_nhds, mem_nhds_iff]

Result:
no goals
-- Mathlib/Order/Sublattice.lean
@[simp, norm_cast] lemma coe_eq_empty : L = (∅ : Set α) ↔ L = ⊥

Proof state:
α : Type u_2
inst✝ : Lattice α
L : Sublattice α
⊢ ↑L = ∅ ↔ L = ⊥

Tactic:
rw [← coe_bot, coe_inj]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
@[reassoc (attr := simp)]
lemma inj_iso_hom (i : I) (hi : p i = j) :
    c.inj ⟨i, hi⟩ ≫ (c.iso hc).hom = X.ιMapObj p i j hi

Proof state:
I : Type u_1
J : Type u_2
C : Type u_4
inst✝¹ : Category.{u_5, u_4} C
X : GradedObject I C
p : I → J
j : J
inst✝ : X.HasMap p
c : X.CofanMapObjFun p j
hc : IsColimit c
i : I
hi : p i = j
⊢ Cofan.inj c ⟨i, hi⟩ ≫ (iso hc).hom = X.ιMapObj p i j hi

Tactic:
apply IsColimit.comp_coconePointUniqueUpToIso_hom

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem deriv_const_add (c : F) : deriv (c + f ·) x = deriv f x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
c : F
⊢ deriv (fun x => c + f x) x = deriv f x

Tactic:
simp only [deriv, fderiv_const_add]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem lt_csSup_iff (hb : BddAbove s) (hs : s.Nonempty) : a < sSup s ↔ ∃ b ∈ s, a < b

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
a : α
hb : BddAbove s
hs : s.Nonempty
⊢ a < sSup s ↔ ∃ b ∈ s, a < b

Tactic:
simpa only [not_le, not_forall₂, exists_prop] using (csSup_le_iff hb hs (a := a)).not

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
lemma coe_mem_spectrum_real_of_nonneg [Algebra ℝ A] [NonnegSpectrumClass ℝ A] {a : A} {x : ℝ≥0}
    (ha : 0 ≤ a

Proof state:
A : Type u_3
inst✝³ : Ring A
inst✝² : PartialOrder A
inst✝¹ : Algebra ℝ A
inst✝ : NonnegSpectrumClass ℝ A
a : A
x : ℝ≥0
ha : autoParam (0 ≤ a) _auto✝
⊢ ↑x ∈ spectrum ℝ a ↔ x ∈ spectrum ℝ≥0 a

Tactic:
simp [← (SpectrumRestricts.nnreal_of_nonneg ha).algebraMap_image, Set.mem_image,
  NNReal.algebraMap_eq_coe]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem smulTower_leftMulMatrix (x) (ik jk) :
    leftMulMatrix (b.smulTower c) x ik jk =
      leftMulMatrix b (leftMulMatrix c x ik.2 jk.2) ik.1 jk.1

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
m : Type u_4
n : Type u_5
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
b : Basis m R S
c : Basis n S T
x : T
ik jk : m × n
⊢ (leftMulMatrix (b.smulTower c)) x ik jk = (leftMulMatrix b) ((leftMulMatrix c) x ik.2 jk.2) ik.1 jk.1

Tactic:
simp only [leftMulMatrix_apply, LinearMap.toMatrix_apply, mul_comm, Basis.smulTower_apply,
  Basis.smulTower_repr, Finsupp.smul_apply, id.smul_eq_mul, LinearEquiv.map_smul, mul_smul_comm,
  coe_lmul_eq_mul, LinearMap.mul_apply']

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_eq_pi_iff_oangle_rev_eq_pi {x y : V} : o.oangle x y = π ↔ o.oangle y x = π

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle x y = ↑π ↔ o.oangle y x = ↑π

Tactic:
rw [oangle_rev, neg_eq_iff_eq_neg, Real.Angle.neg_coe_pi]

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Hom.lean
@[to_additive existing (attr := ext) AddMonoidHom.ext_nat]
lemma MonoidHom.ext_mnat ⦃f g : Multiplicative ℕ →* M⦄
    (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) : f = g :=
  MonoidHom.ext fun n ↦ by rw [f.apply_mnat, g.apply_mnat, h]

Proof state:
M : Type u_2
inst✝ : Monoid M
f g : Multiplicative ℕ →* M
h : f (ofAdd 1) = g (ofAdd 1)
n : Multiplicative ℕ
⊢ f n = g n

Tactic:
rw [f.apply_mnat, g.apply_mnat, h]

Result:
no goals