harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_insertListIfNewUnit_of_contains [BEq α] [EquivBEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α}
    {k fallback : α}
    (contains : containsKey k l = true) :
    getKeyD k (insertListIfNewUnit l toInsert) fallback = getKeyD k l fallback

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k fallback : α
contains : containsKey k l = true
⊢ getKeyD k (insertListIfNewUnit l toInsert) fallback = getKeyD k l fallback

Tactic:
rw [getKeyD_eq_getKey?,
  getKey?_insertListIfNewUnit_of_contains contains, getKeyD_eq_getKey?]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean
theorem opNNNorm_le_of_unit_nnnorm [NormedSpace ℝ E] [NormedSpace ℝ F] {f : E →L[ℝ] F} {C : ℝ≥0}
    (hf : ∀ x, ‖x‖₊ = 1 → ‖f x‖₊ ≤ C) : ‖f‖₊ ≤ C :=
  opNorm_le_of_unit_norm C.coe_nonneg fun x hx => hf x <| by rwa [← NNReal.coe_eq_one]

Proof state:
E : Type u_4
F : Type u_6
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
f : E →L[ℝ] F
C : ℝ≥0
hf : ∀ (x : E), ‖x‖₊ = 1 → ‖f x‖₊ ≤ C
x : E
hx : ‖x‖ = 1
⊢ ‖x‖₊ = 1

Tactic:
rwa [← NNReal.coe_eq_one]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive] lemma left_inv_eq_right_inv (hba : b * a = 1) (hac : a * c = 1) : b = c

Proof state:
M : Type u_2
inst✝ : Monoid M
a b c : M
hba : b * a = 1
hac : a * c = 1
⊢ b = c

Tactic:
rw [← one_mul c, ← hba, mul_assoc, hac, mul_one b]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_getLsbD : eval assign (.getLsbD expr idx) = (expr.eval assign).getLsbD idx

Proof state:
assign : BVExpr.Assignment
a✝ : Nat
expr : BVExpr a✝
idx : Nat
⊢ eval assign (getLsbD expr idx) = (BVExpr.eval assign expr).getLsbD idx

Tactic:
rfl

Result:
no goals
-- Mathlib/Computability/MyhillNerode.lean
theorem leftQuotient_append (x y : List α) :
    L.leftQuotient (x ++ y) = (L.leftQuotient x).leftQuotient y

Proof state:
α : Type u
L : Language α
x y : List α
⊢ L.leftQuotient (x ++ y) = (L.leftQuotient x).leftQuotient y

Tactic:
simp [leftQuotient, Language]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem det_nonsing_inv_mul_det (h : IsUnit A.det) : A⁻¹.det * A.det = 1

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A⁻¹.det * A.det = 1

Tactic:
rw [← det_mul, A.nonsing_inv_mul h, det_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem cons_add_cons (x) (xs : IntList) (y) (ys : IntList) :
    (x :: xs) + (y :: ys) = (x + y) :: (xs + ys)

Proof state:
x : Int
xs : IntList
y : Int
ys : IntList
⊢ x :: xs + y :: ys = (x + y) :: (xs + ys)

Tactic:
simp [add_def]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_eq_pi_div_two {x} : arccos x = π / 2 ↔ x = 0

Proof state:
x : ℝ
⊢ arccos x = π / 2 ↔ x = 0

Tactic:
simp [arccos]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_natCast_mul (x : ℝ≥0∞) (n : ℕ) (z : ℝ) : x ^ (n * z) = (x ^ n) ^ z

Proof state:
x : ℝ≥0∞
n : ℕ
z : ℝ
⊢ x ^ (↑n * z) = (x ^ n) ^ z

Tactic:
rw [rpow_mul, rpow_natCast]

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

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

Tactic:
simp_to_raw using Raw₀.contains_insertIfNew_self

Result:
no goals
-- Mathlib/Data/Int/Sqrt.lean
theorem exists_mul_self (x : ℤ) : (∃ n, n * n = x) ↔ sqrt x * sqrt x = x :=
  ⟨fun ⟨n, hn⟩ => by rw [← hn, sqrt_eq, ← Int.ofNat_mul, natAbs_mul_self], fun h => ⟨sqrt x, h⟩⟩

Proof state:
x : ℤ
x✝ : ∃ n, n * n = x
n : ℤ
hn : n * n = x
⊢ sqrt x * sqrt x = x

Tactic:
rw [← hn, sqrt_eq, ← Int.ofNat_mul, natAbs_mul_self]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Control/ForInStep/Lemmas.lean
theorem ForInStep.bindList_append [Monad m] [LawfulMonad m]
    (f : α → β → m (ForInStep β)) (s : ForInStep β) (l₁ l₂) :
    s.bindList f (l₁ ++ l₂) = s.bindList f l₁ >>= (·.bindList f l₂)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
s : ForInStep β
l₁ l₂ : List α
⊢ bindList f (l₁ ++ l₂) s = do
    let x ← bindList f l₁ s
    bindList f l₂ x

Tactic:
induction l₁ generalizing s <;> simp [*]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_neg_right (x y : M) : polar Q x (-y) = -polar Q x y

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x y : M
⊢ polar (⇑Q) x (-y) = -polar (⇑Q) x y

Tactic:
rw [← neg_one_smul R y, polar_smul_right, neg_one_smul]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem multiplicity_ne_zero :
    multiplicity a b ≠ 0 ↔ a ∣ b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
⊢ multiplicity a b ≠ 0 ↔ a ∣ b

Tactic:
simp [multiplicity_eq_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/HomEquiv.lean
lemma homEquiv_comp (f : L₁.obj X ⟶ L₁.obj Y) (g : L₁.obj Y ⟶ L₁.obj Z) :
    homEquiv W L₁ L₂ (f ≫ g) = homEquiv W L₁ L₂ f ≫ homEquiv W L₁ L₂ g

Proof state:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{u_9, u_1} C
inst✝³ : Category.{u_8, u_5} D₁
inst✝² : Category.{u_10, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X Y Z : C
f : L₁.obj X ⟶ L₁.obj Y
g : L₁.obj Y ⟶ L₁.obj Z
⊢ (homEquiv W L₁ L₂) (f ≫ g) = (homEquiv W L₁ L₂) f ≫ (homEquiv W L₁ L₂) g

Tactic:
apply LocalizerMorphism.homMap_comp

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem star_iff [InvolutiveStar R] {x : R} : IsSelfAdjoint (star x) ↔ IsSelfAdjoint x

Proof state:
R : Type u_1
inst✝ : InvolutiveStar R
x : R
⊢ IsSelfAdjoint (star x) ↔ IsSelfAdjoint x

Tactic:
simpa only [IsSelfAdjoint, star_star] using eq_comm

Result:
no goals
-- Mathlib/Data/Finset/Dedup.lean
theorem toFinset_eq_iff_perm_dedup : l.toFinset = l'.toFinset ↔ l.dedup ~ l'.dedup

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ l.toFinset = l'.toFinset ↔ l.dedup ~ l'.dedup

Tactic:
simp [Finset.ext_iff, perm_ext_iff_of_nodup (nodup_dedup _) (nodup_dedup _)]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
theorem abs_sign_of_nonzero {z : ℤ} (hz : z ≠ 0) : |z.sign| = 1

Proof state:
z : ℤ
hz : z ≠ 0
⊢ |z.sign| = 1

Tactic:
rw [abs_eq_natAbs, natAbs_sign_of_nonzero hz, Int.ofNat_one]

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
lemma bot_imp (φ : L.BoundedFormula α n) : ⊥ ⟹[T] φ := fun M v xs => by
  simp only [BoundedFormula.realize_imp, BoundedFormula.realize_bot, false_implies]

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (⊥ ⟹ φ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_bot, false_implies]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma tensorHom_id {X₁ X₂ : LocalizedMonoidal L W ε} (f : X₁ ⟶ X₂) (Y : LocalizedMonoidal L W ε) :
    f ⊗ 𝟙 Y = f ▷ Y

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ : LocalizedMonoidal L W ε
f : X₁ ⟶ X₂
Y : LocalizedMonoidal L W ε
⊢ f ⊗ 𝟙 Y = f ▷ Y

Tactic:
simp [monoidalCategoryStruct]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_const (s : Set α) (c : ℝ≥0∞) : ∫⁻ _ in s, c ∂μ = c * μ s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
c : ℝ≥0∞
⊢ ∫⁻ (x : α) in s, c ∂μ = c * μ s

Tactic:
rw [lintegral_const, Measure.restrict_apply_univ]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem pi_nonempty_iff : (s.pi t).Nonempty ↔ ∀ i, ∃ x, i ∈ s → x ∈ t i

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
⊢ (s.pi t).Nonempty ↔ ∀ (i : ι), ∃ x, i ∈ s → x ∈ t i

Tactic:
simp [Classical.skolem, Set.Nonempty]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem iUnion_Icc_intCast : ⋃ n : ℤ, Icc (n : α) (n + 1) = Set.univ

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
⊢ ⋃ n, Icc (↑n) (↑n + 1) = univ

Tactic:
simpa only [zero_add] using iUnion_Icc_add_intCast (0 : α)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_eq_isSome_getKey? [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
    m.contains a = (m.getKey? a).isSome

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
⊢ m.contains a = (m.getKey? a).isSome

Tactic:
simp_to_model using List.containsKey_eq_isSome_getKey?

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnected.lean
@[simp]
lemma image_subtype_val_Ioo {s : Set α} [OrdConnected s] (x y : s) :
    Subtype.val '' Ioo x y = Ioo x.1 y :=
  (OrderEmbedding.subtype (· ∈ s)).image_Ioo (by simpa) x y

Proof state:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : s.OrdConnected
x y : ↑s
⊢ (range ⇑(OrderEmbedding.subtype fun x => x ∈ s)).OrdConnected

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_dite_irrel (p : Prop) [Decidable p] (s : Finset α) (f : p → α → β) (g : ¬p → α → β) :
    ∏ x ∈ s, (if h : p then f h x else g h x) =
      if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
p : Prop
inst✝ : Decidable p
s : Finset α
f : p → α → β
g : ¬p → α → β
⊢ (∏ x ∈ s, if h : p then f h x else g h x) = if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x

Tactic:
split_ifs with h <;> rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
@[reassoc, elementwise]
lemma map_ΓIso_inv {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) :
    Y.presheaf.map (homOfLE inf_le_right).op ≫ (ΓIso f U).inv = f.app U

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ Y.presheaf.map (homOfLE ⋯).op ≫ (ΓIso f U).inv = Scheme.Hom.app f U

Tactic:
simp [Scheme.Hom.appLE_eq_app]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Finsupp.lean
theorem factorization_zero : factorization (0 : α) = 0

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
⊢ factorization 0 = 0

Tactic:
simp [factorization]

Result:
no goals
-- Mathlib/Analysis/Meromorphic/Basic.lean
@[simp] lemma inv_iff : MeromorphicOn s⁻¹ U ↔ MeromorphicOn s U :=
  ⟨fun h ↦ by simpa only [inv_inv] using h.inv, inv⟩

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
s : 𝕜 → 𝕜
U : Set 𝕜
h : MeromorphicOn s⁻¹ U
⊢ MeromorphicOn s U

Tactic:
simpa only [inv_inv] using h.inv

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem ult_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    (BitVec.ult lhs' rhs') = (BitVec.ult lhs rhs)

Proof state:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs'.ult rhs' = lhs.ult rhs

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_neg' (a b : α) : toIcoDiv hp (-a) b = -(toIocDiv hp a (-b) + 1)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp (-a) b = -(toIocDiv hp a (-b) + 1)

Tactic:
simpa only [neg_neg] using toIcoDiv_neg hp (-a) (-b)

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
lemma casesOn'_eq_elim (b : β) (f : α → β) (a : Option α) :
    Option.casesOn' a b f = Option.elim a b f

Proof state:
α : Type u_1
β : Type u_2
b : β
f : α → β
a : Option α
⊢ a.casesOn' b f = a.elim b f

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_mul_right (m n k : Nat) : gcd (m * n) (k * n) = gcd m k * n

Proof state:
m n k : Nat
⊢ (m * n).gcd (k * n) = m.gcd k * n

Tactic:
rw [Nat.mul_comm m n, Nat.mul_comm k n, Nat.mul_comm (gcd m k) n, gcd_mul_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_eq_empty_iff : p ++ q = #[] ↔ p = #[] ∧ q = #[]

Proof state:
α✝ : Type u_1
p q : Array α✝
⊢ p ++ q = #[] ↔ p = #[] ∧ q = #[]

Tactic:
cases p <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem Complex.hasStrictDerivAt_cpow_const (h : x ∈ slitPlane) :
    HasStrictDerivAt (fun z : ℂ => z ^ c) (c * x ^ (c - 1)) x

Proof state:
x c : ℂ
h : x ∈ slitPlane
⊢ HasStrictDerivAt (fun z => z ^ c) (c * x ^ (c - 1)) x

Tactic:
simpa only [mul_zero, add_zero, mul_one] using
  (hasStrictDerivAt_id x).cpow (hasStrictDerivAt_const x c) h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem zero_of_to_zero {X : C} (f : X ⟶ 0) : f = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
f : X ⟶ 0
⊢ f = 0

Tactic:
ext

Result:
no goals
-- Mathlib/NumberTheory/Multiplicity.lean
theorem Int.two_pow_two_pow_sub_pow_two_pow {x y : ℤ} (n : ℕ) (hxy : 4 ∣ x - y) (hx : ¬2 ∣ x) :
    emultiplicity 2 (x ^ 2 ^ n - y ^ 2 ^ n) = emultiplicity 2 (x - y) + n

Proof state:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
⊢ emultiplicity 2 (x ^ 2 ^ n - y ^ 2 ^ n) = emultiplicity 2 (x - y) + ↑n

Tactic:
simp only [pow_two_pow_sub_pow_two_pow n, emultiplicity_mul Int.prime_two,
  Finset.emultiplicity_prod Int.prime_two, add_comm, Nat.cast_one, Finset.sum_const,
  Finset.card_range, nsmul_one, Int.two_pow_two_pow_add_two_pow_two_pow hx hxy]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean
lemma integral_rnDeriv_mul_log [SigmaFinite μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ ≪ ν) :
    ∫ a, (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν = ∫ a, llr μ ν a ∂μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ ∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν = ∫ (a : α), llr μ ν a ∂μ

Tactic:
simp_rw [← smul_eq_mul, integral_rnDeriv_smul hμν, llr]

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
@[simp] lemma zero_union : 0 ∪ s = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ 0 ∪ s = s

Tactic:
simp [union_def, Multiset.zero_sub]

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

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

Tactic:
simp only [contains_alter h, beq_self_eq_true, reduceIte]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem of_eq_eq_true {a b : Prop} (h : (a = b) = True) : (¬a ∨ b) ∧ (¬b ∨ a)

Proof state:
a b : Prop
h : (a = b) = True
⊢ (¬a ∨ b) ∧ (¬b ∨ a)

Tactic:
by_cases a <;> by_cases b <;> simp_all

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem Δ_of_isCharThreeJNeZeroNF : W.Δ = -64 * W.a₂ ^ 3 * W.a₆ - 432 * W.a₆ ^ 2

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharThreeJNeZeroNF
⊢ W.Δ = -64 * W.a₂ ^ 3 * W.a₆ - 432 * W.a₆ ^ 2

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mdifferentiable_prod_iff (f : M → M' × N') :
    MDifferentiable I (I'.prod J') f ↔
      MDifferentiable I I' (Prod.fst ∘ f) ∧ MDifferentiable I J' (Prod.snd ∘ f) :=
  ⟨fun h => ⟨h.fst, h.snd⟩, fun h => by convert h.1.prod_mk h.2⟩

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
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' : Type u_14
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
G' : Type u_15
inst✝² : TopologicalSpace G'
J' : ModelWithCorners 𝕜 F' G'
N' : Type u_16
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
f : M → M' × N'
h : MDifferentiable I I' (Prod.fst ∘ f) ∧ MDifferentiable I J' (Prod.snd ∘ f)
⊢ MDifferentiable I (I'.prod J') f

Tactic:
convert h.1.prod_mk h.2

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem braiding_leftUnitor_aux₁ (X : C) :
    (α_ (𝟙_ C) (𝟙_ C) X).hom ≫
        (𝟙_ C ◁ (β_ X (𝟙_ C)).inv) ≫ (α_ _ X _).inv ≫ ((λ_ X).hom ▷ _) =
      ((λ_ _).hom ▷ X) ≫ (β_ X (𝟙_ C)).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (β_ X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (λ_ X).hom ▷ 𝟙_ C =
    (λ_ (𝟙_ C)).hom ▷ X ≫ (β_ X (𝟙_ C)).inv

Tactic:
monoidal

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/SMul.lean
theorem eval_smul [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (s : S) (p : R[X])
    (x : R) : (s • p).eval x = s • p.eval x

Proof state:
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
x : R
⊢ eval x (s • p) = s • eval x p

Tactic:
rw [← smul_one_smul R s p, eval, eval₂_smul, RingHom.id_apply, smul_one_mul]

Result:
no goals
-- Mathlib/Order/Filter/Tendsto.lean
theorem tendsto_pure {f : α → β} {a : Filter α} {b : β} :
    Tendsto f a (pure b) ↔ ∀ᶠ x in a, f x = b

Proof state:
α : Type u_1
β : Type u_2
f : α → β
a : Filter α
b : β
⊢ Tendsto f a (pure b) ↔ ∀ᶠ (x : α) in a, f x = b

Tactic:
simp only [Tendsto, le_pure_iff, mem_map', mem_singleton_iff, Filter.Eventually]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
theorem mulRothNumber_map_mul_right :
    mulRothNumber (s.map <| mulRightEmbedding a) = mulRothNumber s

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ mulRothNumber (map (mulRightEmbedding a) s) = mulRothNumber s

Tactic:
rw [← mulLeftEmbedding_eq_mulRightEmbedding, mulRothNumber_map_mul_left s a]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_eq_of_eq_mul' {a b c : G} (h : a = b * c) : a / b = c

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c : G
h : a = b * c
⊢ a / b = c

Tactic:
rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]

Result:
no goals
-- Mathlib/Data/Finsupp/Order.lean
theorem single_le_iff {i : ι} {x : α} {f : ι →₀ α} : single i x ≤ f ↔ x ≤ f i :=
  (le_iff' _ _ support_single_subset).trans <| by simp

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
i : ι
x : α
f : ι →₀ α
⊢ (∀ i_1 ∈ {i}, (single i x) i_1 ≤ f i_1) ↔ x ≤ f i

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem map_bot [IsScalarTower R B B] [SMulCommClass R B B]
    (f : A →ₙₐ[R] B) : (⊥ : NonUnitalSubalgebra R A).map f = ⊥ :=
  SetLike.coe_injective <| by simp [NonUnitalAlgebra.coe_bot, NonUnitalSubalgebra.coe_map]

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁸ : CommSemiring R
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Module R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
f : A →ₙₐ[R] B
⊢ ↑(NonUnitalSubalgebra.map f ⊥) = ↑⊥

Tactic:
simp [NonUnitalAlgebra.coe_bot, NonUnitalSubalgebra.coe_map]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
lemma LSeriesSummable.neg {f : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s) :
    LSeriesSummable (-f) s

Proof state:
f : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
⊢ LSeriesSummable (-f) s

Tactic:
simpa [LSeriesSummable, term_neg] using Summable.neg hf

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem head {n : ℕ} : @Primrec' n.succ head :=
  (get 0).of_eq fun v => by simp [get_zero]

Proof state:
n : ℕ
v : List.Vector ℕ n.succ
⊢ v.get 0 = v.head

Tactic:
simp [get_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap'
    (h : S.HomologyData) (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData) :
    leftRightHomologyComparison' h₁ h₂ =
      leftHomologyMap' (𝟙 S) h₁ h.left ≫ h.iso.hom ≫ rightHomologyMap' (𝟙 S) h.right h₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ leftRightHomologyComparison' h₁ h₂ = leftHomologyMap' (𝟙 S) h₁ h.left ≫ h.iso.hom ≫ rightHomologyMap' (𝟙 S) h.right h₂

Tactic:
simpa only [h.leftRightHomologyComparison'_eq] using
  leftRightHomologyComparison'_compatibility h₁ h.left h₂ h.right

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem isUnit_inv_iff {x : tsze R M} : IsUnit x⁻¹ ↔ IsUnit x

Proof state:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
⊢ IsUnit x⁻¹ ↔ IsUnit x

Tactic:
simp_rw [isUnit_iff_isUnit_fst, fst_inv, isUnit_iff_ne_zero, ne_eq, inv_eq_zero]

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem CovBy.Ioi_eq (h : a ⋖ b) : Ioi a = Ici b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Ioi a = Ici b

Tactic:
rw [← Ioo_union_Ici_eq_Ioi h.lt, h.Ioo_eq, empty_union]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_cons {x : BitVec w} : (cons a x).setWidth w = x

Proof state:
w : Nat
a : Bool
x : BitVec w
⊢ setWidth w (cons a x) = x

Tactic:
simp [cons, setWidth_append]

Result:
no goals
-- Mathlib/Dynamics/BirkhoffSum/Average.lean
theorem birkhoffAverage_apply_sub_birkhoffAverage {α M : Type*} (R : Type*) [DivisionRing R]
    [AddCommGroup M] [Module R M] (f : α → α) (g : α → M) (n : ℕ) (x : α) :
    birkhoffAverage R f g n (f x) - birkhoffAverage R f g n x =
      (n : R)⁻¹ • (g (f^[n] x) - g x)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : α → α
g : α → M
n : ℕ
x : α
⊢ birkhoffAverage R f g n (f x) - birkhoffAverage R f g n x = (↑n)⁻¹ • (g (f^[n] x) - g x)

Tactic:
simp only [birkhoffAverage, birkhoffSum_apply_sub_birkhoffSum, ← smul_sub]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.sub_eq [AddGroup α] (h : Periodic f c) (x : α) : f (x - c) = f x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
x : α
⊢ f (x - c) = f x

Tactic:
simpa only [sub_add_cancel] using (h (x - c)).symm

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_type_lt [LinearOrder α] [IsWellOrder α (· < ·)] :
    (@type α (· < ·) _).cof = @Order.cof α (· ≤ ·)

Proof state:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : IsWellOrder α fun x1 x2 => x1 < x2
⊢ (type fun x1 x2 => x1 < x2).cof = Order.cof fun x1 x2 => x1 ≤ x2

Tactic:
rw [cof_type, compl_lt, swap_ge]

Result:
no goals