harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem lcm_eq_zero_iff [Nontrivial α] (s : Multiset α) : s.lcm = 0 ↔ (0 : α) ∈ s

Proof state:
case empty
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
⊢ lcm 0 = 0 ↔ 0 ∈ 0

Tactic:
simp only [lcm_zero, one_ne_zero, not_mem_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
s : Multiset α
⊢ s.lcm = 0 ↔ 0 ∈ s

Tactic:
induction s using Multiset.induction_on with
| empty => simp only [lcm_zero, one_ne_zero, not_mem_zero]
| cons a s ihs => simp only [mem_cons, lcm_cons, lcm_eq_zero_iff, ihs, @eq_comm _ a]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : Nontrivial α
a : α
s : Multiset α
ihs : s.lcm = 0 ↔ 0 ∈ s
⊢ (a ::ₘ s).lcm = 0 ↔ 0 ∈ a ::ₘ s

Tactic:
simp only [mem_cons, lcm_cons, lcm_eq_zero_iff, ihs, @eq_comm _ a]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_zero : ⌊(0 : α)⌋ = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
⊢ ⌊0⌋ = 0

Tactic:
rw [← cast_zero, floor_intCast]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
@[simp] lemma reProdIm_nonempty : (s ×ℂ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Proof state:
s t : Set ℝ
⊢ (s ×ℂ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

Tactic:
simp [Set.Nonempty, reProdIm, Complex.exists]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem restrict_iSup {ι} (s : Set α) (m : ι → OuterMeasure α) :
    restrict s (⨆ i, m i) = ⨆ i, restrict s (m i)

Proof state:
α : Type u_1
ι : Sort u_3
s : Set α
m : ι → OuterMeasure α
⊢ (restrict s) (⨆ i, m i) = ⨆ i, (restrict s) (m i)

Tactic:
simp [restrict]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
@[simp] lemma odd_add_one_self : Odd (a + 1 + a)

Proof state:
α : Type u_2
inst✝ : Semiring α
a : α
⊢ Odd (a + 1 + a)

Tactic:
simp [add_comm _ a]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem Left.inv_lt_one_iff : a⁻¹ < 1 ↔ 1 < a

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a : α
⊢ a⁻¹ < 1 ↔ 1 < a

Tactic:
rw [← mul_lt_mul_iff_left a, mul_inv_cancel, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getD_unitOfList
    {l : List α} {k : α} {fallback : Unit} :
    getD (unitOfList l) k fallback = ()

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
l : List α
k : α
fallback : Unit
⊢ getD (unitOfList l) k fallback = ()

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_add_int (a : α) (z : ℤ) : ⌊a + z⌋ = ⌊a⌋ + z :=
  eq_of_forall_le_iff fun a => by
    rw [le_floor, ← sub_le_iff_le_add, ← sub_le_iff_le_add, le_floor, Int.cast_sub]

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a✝ : α
z a : ℤ
⊢ a ≤ ⌊a✝ + ↑z⌋ ↔ a ≤ ⌊a✝⌋ + z

Tactic:
rw [le_floor, ← sub_le_iff_le_add, ← sub_le_iff_le_add, le_floor, Int.cast_sub]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.and_contra (a : BitVec w) : a &&& ~~~a = 0#w

Proof state:
case pred
w : Nat
a : BitVec w
i : Nat
h : i < w
⊢ (a &&& ~~~a).getLsbD i = (0#w).getLsbD i

Tactic:
simp [h]

Result:
no goals

Proof state:
w : Nat
a : BitVec w
⊢ a &&& ~~~a = 0#w

Tactic:
ext i h

Result:
case pred
w : Nat
a : BitVec w
i : Nat
h : i < w
⊢ (a &&& ~~~a).getLsbD i = (0#w).getLsbD i
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem isoExt_hom_m : (isoExt hF hF').hom ≫ F'.m = F.m

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (hF.isoExt hF').hom ≫ F'.m = F.m

Tactic:
simp

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

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

Tactic:
simp_to_model [alter] using List.getValueCast_alterKey_self

Result:
no goals

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

Tactic:
rwa [contains_alter _ h, beq_self_eq_true] at hc

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem ker_eq_bot : f.ker = ⊥ ↔ Function.Injective f

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
⊢ f.ker = ⊥ ↔ Function.Injective ⇑f

Tactic:
rw [← LieSubmodule.toSubmodule_inj, ker_toSubmodule, LieSubmodule.bot_toSubmodule,
  LinearMap.ker_eq_bot, coe_toLinearMap]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_smul_left (a : R) (x y : M) : polar Q (a • x) y = a • 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
a : R
x y : M
⊢ polar (⇑Q) (a • x) y = a • polar (⇑Q) x y

Tactic:
obtain ⟨B, h⟩ := Q.exists_companion

Result:
case intro
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
a : R
x y : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ polar (⇑Q) (a • x) y = a • polar (⇑Q) x y

Proof state:
case intro
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
a : R
x y : M
B : BilinMap R M N
h : ∀ (x y : M), Q (x + y) = Q x + Q y + (B x) y
⊢ polar (⇑Q) (a • x) y = a • polar (⇑Q) x y

Tactic:
simp_rw [polar, h, Q.map_smul, LinearMap.map_smul₂, sub_sub, add_sub_cancel_left]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem four_mul_arctan_inv_5_sub_arctan_inv_239 : 4 * arctan 5⁻¹ - arctan 239⁻¹ = π / 4

Proof state:
⊢ 4 * arctan 5⁻¹ - arctan 239⁻¹ = π / 4

Tactic:
rw [show 4 * arctan _ = 2 * (2 * _) by ring, two_mul_arctan, two_mul_arctan, ← arctan_one,
  sub_eq_iff_eq_add, arctan_add] <;> norm_num

Result:
no goals

Proof state:
⊢ 4 * arctan 5⁻¹ = 2 * (2 * ?m.123718)

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma image_add_left_Ico (a b c : α) : (Ico a b).image (c + ·) = Ico (c + a) (c + b)

Proof state:
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => c + x) (Ico a b) = Ico (c + a) (c + b)

Tactic:
rw [← map_add_left_Ico, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_symmDiff (hf : Injective f) (s t : Set α) : f '' s ∆ t = (f '' s) ∆ (f '' t)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
⊢ f '' s ∆ t = (f '' s) ∆ (f '' t)

Tactic:
simp_rw [Set.symmDiff_def, image_union, image_diff hf]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_mul_cos₁ : ∫ x in a..b, sin x * cos x = (sin b ^ 2 - sin a ^ 2) / 2

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x * cos x = (sin b ^ 2 - sin a ^ 2) / 2

Tactic:
simpa using integral_sin_pow_mul_cos_pow_odd 1 0

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem some_add [AddCommMonoid M] (f g : Option α →₀ M) : (f + g).some = f.some + g.some

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
f g : Option α →₀ M
a✝ : α
⊢ (f + g).some a✝ = (f.some + g.some) a✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
f g : Option α →₀ M
⊢ (f + g).some = f.some + g.some

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : AddCommMonoid M
f g : Option α →₀ M
a✝ : α
⊢ (f + g).some a✝ = (f.some + g.some) a✝
-- Mathlib/Algebra/Polynomial/Bivariate.lean
lemma map_mapRingHom_evalEval (x y : R) :
    (p.map <| mapRingHom f).evalEval (f x) (f y) = f (p.evalEval x y)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X][Y]
x y : R
⊢ evalEval (f x) (f y) (map (mapRingHom f) p) = f (evalEval x y p)

Tactic:
rw [evalEval, ← map_mapRingHom_eval_map_eval, map_C]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma Spec.map_eqToHom {R S : CommRingCat} (e : R = S) :
    Spec.map (eqToHom e) = eqToHom (e ▸ rfl)

Proof state:
R : CommRingCat
⊢ map (eqToHom ⋯) = eqToHom ⋯

Tactic:
exact Spec.map_id _

Result:
no goals

Proof state:
R S : CommRingCat
e : R = S
⊢ map (eqToHom e) = eqToHom ⋯

Tactic:
subst e

Result:
R : CommRingCat
⊢ map (eqToHom ⋯) = eqToHom ⋯
-- Mathlib/MeasureTheory/Function/EssSup.lean
@[simp] lemma essInf_cond_count_eq_ciInf [Finite α] (hf : BddBelow (Set.range f)) :
    essInf f (uniformOn univ) = ⨅ a, f a :=
  essInf_eq_ciInf (by simpa [uniformOn, cond_apply]) hf

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝³ : ConditionallyCompleteLattice β
f : α → β
inst✝² : Nonempty α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Finite α
hf : BddBelow (range f)
⊢ ∀ (a : α), (uniformOn univ) {a} ≠ 0

Tactic:
simpa [uniformOn, cond_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_append_of_containsKey_eq_false {β : Type v} [BEq α] {l l' : List ((_ : α) × β)}
    {a : α} (h : containsKey a l' = false) : getValue? a (l ++ l') = getValue? a l

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l l' : List ((_ : α) × β)
a : α
h : containsKey a l' = false
⊢ getValue? a (l ++ l') = getValue? a l

Tactic:
rw [getValue?_append, getValue?_eq_none.2 h, Option.or_none]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_mul (x y : ℝ≥0) : sqrt (x * y) = sqrt x * sqrt y

Proof state:
x y : ℝ≥0
⊢ sqrt (x * y) = sqrt x * sqrt y

Tactic:
rw [sqrt_eq_iff_eq_sq, mul_pow, sq_sqrt, sq_sqrt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Lean/Elab/Tactic/Omega/MinNatAbs.lean
theorem minNatAbs_eq_zero_iff {xs : List Int} : xs.minNatAbs = 0 ↔ ∀ y ∈ xs, y = 0

Proof state:
xs : List Int
⊢ xs.minNatAbs = 0 ↔ ∀ (y : Int), y ∈ xs → y = 0

Tactic:
simp [minNatAbs]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Flag.lean
theorem flag_succ (b : Basis (Fin n) R M) (k : Fin n) :
    b.flag k.succ = (R ∙ b k) ⊔ b.flag k.castSucc

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ span R (⇑b '' {i | i.castSucc < k.succ}) = span R {b k} ⊔ span R (⇑b '' {i | i < k})

Tactic:
simp [Fin.castSucc_lt_iff_succ_le, le_iff_eq_or_lt, setOf_or, image_insert_eq, span_insert]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ b.flag k.succ = span R {b k} ⊔ b.flag k.castSucc

Tactic:
simp only [flag, Fin.castSucc_lt_castSucc_iff]

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ span R (⇑b '' {i | i.castSucc < k.succ}) = span R {b k} ⊔ span R (⇑b '' {i | i < k})
-- Mathlib/Combinatorics/SetFamily/Intersecting.lean
theorem intersecting_singleton : ({a} : Set α).Intersecting ↔ a ≠ ⊥

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a : α
⊢ {a}.Intersecting ↔ a ≠ ⊥

Tactic:
simp [Intersecting]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem isTheta_norm_left : (fun x ↦ ‖f' x‖) =Θ[l] g ↔ f' =Θ[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x => ‖f' x‖) =Θ[l] g ↔ f' =Θ[l] g

Tactic:
simp [IsTheta]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem frequently_frequently_nhds {p : X → Prop} :
    (∃ᶠ x' in 𝓝 x, ∃ᶠ x'' in 𝓝 x', p x'') ↔ ∃ᶠ x in 𝓝 x, p x

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
p : X → Prop
⊢ (∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ∃ᶠ (x : X) in 𝓝 x, p x

Tactic:
rw [← not_iff_not]

Result:
X : Type u
x : X
inst✝ : TopologicalSpace X
p : X → Prop
⊢ (¬∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ¬∃ᶠ (x : X) in 𝓝 x, p x

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
p : X → Prop
⊢ (¬∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ¬∃ᶠ (x : X) in 𝓝 x, p x

Tactic:
simp only [not_frequently, eventually_eventually_nhds]

Result:
no goals
-- Mathlib/LinearAlgebra/Contraction.lean
theorem map_dualTensorHom (f : Module.Dual R M) (p : P) (g : Module.Dual R N) (q : Q) :
    TensorProduct.map (dualTensorHom R M P (f ⊗ₜ[R] p)) (dualTensorHom R N Q (g ⊗ₜ[R] q)) =
      dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q) (dualDistrib R M N (f ⊗ₜ g) ⊗ₜ[R] p ⊗ₜ[R] q)

Proof state:
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : Dual R M
p : P
g : Dual R N
q : Q
⊢ TensorProduct.map ((dualTensorHom R M P) (f ⊗ₜ[R] p)) ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) =
    (dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q)) ((dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] p ⊗ₜ[R] q)

Tactic:
ext m n

Result:
case H.h.h
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : Dual R M
p : P
g : Dual R N
q : Q
m : M
n : N
⊢ (((TensorProduct.mk R M N).compr₂
          (TensorProduct.map ((dualTensorHom R M P) (f ⊗ₜ[R] p)) ((dualTensorHom R N Q) (g ⊗ₜ[R] q))))
        m)
      n =
    (((TensorProduct.mk R M N).compr₂
          ((dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q)) ((dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] p ⊗ₜ[R] q)))
        m)
      n

Proof state:
case H.h.h
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : Dual R M
p : P
g : Dual R N
q : Q
m : M
n : N
⊢ (((TensorProduct.mk R M N).compr₂
          (TensorProduct.map ((dualTensorHom R M P) (f ⊗ₜ[R] p)) ((dualTensorHom R N Q) (g ⊗ₜ[R] q))))
        m)
      n =
    (((TensorProduct.mk R M N).compr₂
          ((dualTensorHom R (M ⊗[R] N) (P ⊗[R] Q)) ((dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] p ⊗ₜ[R] q)))
        m)
      n

Tactic:
simp only [compr₂_apply, mk_apply, map_tmul, dualTensorHom_apply, dualDistrib_apply, ←
  smul_tmul_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_modify [LawfulBEq α] {k k' : α} {f : β k → β k} (h : m.WF) :
    (m.modify k f).get? k' =
      if h : k == k' then
        (cast (congrArg (Option ∘ β) (eq_of_beq h)) ((m.get? k).map f))
      else
        m.get? k'

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

Tactic:
simp_to_raw using Raw₀.get?_modify

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem prodComparison_natural (f : A ⟶ A') (g : B ⟶ B') :
    F.map (f ⊗ g) ≫ prodComparison F A' B' =
      prodComparison F A B ≫ (F.map f ⊗ F.map g)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ChosenFiniteProducts C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : ChosenFiniteProducts D
F : C ⥤ D
A B A' B' : C
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (f ⊗ g) ≫ prodComparison F A' B' = prodComparison F A B ≫ (F.map f ⊗ F.map g)

Tactic:
apply hom_ext <;>
simp only [Category.assoc, prodComparison_fst, tensorHom_fst, prodComparison_fst_assoc,
  prodComparison_snd, tensorHom_snd, prodComparison_snd_assoc, ← F.map_comp]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem ofArrows_surj {ι : Type*} {Y : ι → C} (f : ∀ i, Y i ⟶ X) {Z : C} (g : Z ⟶ X)
    (hg : ofArrows Y f g) : ∃ (i : ι) (h : Y i = Z),
    g = eqToHom h.symm ≫ f i

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y✝ : ι → C
f : (i : ι) → Y✝ i ⟶ X
Y : C
i : ι
⊢ f i = eqToHom ⋯ ≫ f i

Tactic:
simp only [eqToHom_refl, id_comp]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
g : Z ⟶ X
hg : ofArrows Y f g
⊢ ∃ i, ∃ (h : Y i = Z), g = eqToHom ⋯ ≫ f i

Tactic:
obtain ⟨i⟩ := hg

Result:
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y✝ : ι → C
f : (i : ι) → Y✝ i ⟶ X
Y : C
i : ι
⊢ ∃ i_1, ∃ (h : Y✝ i_1 = Y✝ i), f i = eqToHom ⋯ ≫ f i_1

Proof state:
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y✝ : ι → C
f : (i : ι) → Y✝ i ⟶ X
Y : C
i : ι
⊢ ∃ i_1, ∃ (h : Y✝ i_1 = Y✝ i), f i = eqToHom ⋯ ≫ f i_1

Tactic:
exact ⟨i, rfl, by simp only [eqToHom_refl, id_comp]⟩

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
@[stacks 0CKM]
lemma linearIndependent_algHom_toLinearMap
    (K M L) [CommSemiring K] [Semiring M] [Algebra K M] [CommRing L] [IsDomain L] [Algebra K L] :
    LinearIndependent L (AlgHom.toLinearMap : (M →ₐ[K] L) → M →ₗ[K] L)

Proof state:
K : Type u_6
M : Type u_7
L : Type u_8
inst✝⁵ : CommSemiring K
inst✝⁴ : Semiring M
inst✝³ : Algebra K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ LinearIndependent L (⇑(ltoFun K M L) ∘ AlgHom.toLinearMap)

Tactic:
exact (linearIndependent_monoidHom M L).comp
  (RingHom.toMonoidHom ∘ AlgHom.toRingHom)
  (fun _ _ e ↦ AlgHom.ext (DFunLike.congr_fun e :))

Result:
no goals

Proof state:
K : Type u_6
M : Type u_7
L : Type u_8
inst✝⁵ : CommSemiring K
inst✝⁴ : Semiring M
inst✝³ : Algebra K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ LinearIndependent L AlgHom.toLinearMap

Tactic:
apply LinearIndependent.of_comp (LinearMap.ltoFun K M L)

Result:
K : Type u_6
M : Type u_7
L : Type u_8
inst✝⁵ : CommSemiring K
inst✝⁴ : Semiring M
inst✝³ : Algebra K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ LinearIndependent L (⇑(ltoFun K M L) ∘ AlgHom.toLinearMap)
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
@[simp]
lemma coeff_preΨ' (n : ℕ) : (W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) =
    if Even n then n / 2 else n

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) = ↑(if Even n then n / 2 else n)

Tactic:
convert (W.natDegree_coeff_preΨ' n).right using 1

Result:
case h.e'_3
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ ↑(if Even n then n / 2 else n) = ↑(WeierstrassCurve.expCoeff n)

Proof state:
case h.e'_3
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ ↑(if Even n then n / 2 else n) = ↑(WeierstrassCurve.expCoeff n)

Tactic:
rcases n.even_or_odd' with ⟨n, rfl | rfl⟩ <;> simp [expCoeff, n.not_even_two_mul_add_one]

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem lineDeriv_neg : lineDeriv 𝕜 f x (-v) = - lineDeriv 𝕜 f x v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
⊢ lineDeriv 𝕜 f x (-v) = -lineDeriv 𝕜 f x v

Tactic:
rw [← neg_one_smul (R := 𝕜) v, lineDeriv_smul, neg_one_smul]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_nndist_eq_of_L2 (x y : WithLp 2 (α × β)) :
    nndist x y = NNReal.sqrt (nndist x.fst y.fst ^ 2 + nndist x.snd y.snd ^ 2) :=
  NNReal.eq <| by
    push_cast
    exact prod_dist_eq_of_L2 _ _

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 2 (α × β)
⊢ dist x y = √(dist x.1 y.1 ^ 2 + dist x.2 y.2 ^ 2)

Tactic:
exact prod_dist_eq_of_L2 _ _

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 2 (α × β)
⊢ ↑(nndist x y) = ↑(NNReal.sqrt (nndist x.1 y.1 ^ 2 + nndist x.2 y.2 ^ 2))

Tactic:
push_cast

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 2 (α × β)
⊢ dist x y = √(dist x.1 y.1 ^ 2 + dist x.2 y.2 ^ 2)
-- Mathlib/Geometry/Manifold/VectorField.lean
theorem mlieBracketWithin_eq_mlieBracket (hs : UniqueMDiffWithinAt I s x)
    (hV : MDifferentiableAt I I.tangent (fun x ↦ (V x : TangentBundle I M)) x)
    (hW : MDifferentiableAt I I.tangent (fun x ↦ (W x : TangentBundle I M)) x) :
    mlieBracketWithin I V W s x = mlieBracket I V W x

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hs : UniqueMDiffWithinAt I s x
hV : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := V x }) x
hW : MDifferentiableAt I I.tangent (fun x => { proj := x, snd := W x }) x
⊢ mlieBracketWithin I V W s x = mlieBracket I V W x

Tactic:
simp only [← mlieBracketWithin_univ, ← mdifferentiableWithinAt_univ] at hV hW ⊢

Result:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hs : UniqueMDiffWithinAt I s x
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) univ x
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) univ x
⊢ mlieBracketWithin I V W s x = mlieBracketWithin I V W univ x

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁶ : TopologicalSpace H
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
s : Set M
x : M
V W : (x : M) → TangentSpace I x
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hs : UniqueMDiffWithinAt I s x
hV : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := V x }) univ x
hW : MDifferentiableWithinAt I I.tangent (fun x => { proj := x, snd := W x }) univ x
⊢ mlieBracketWithin I V W s x = mlieBracketWithin I V W univ x

Tactic:
exact mlieBracketWithin_subset (subset_univ _) hs hV hW

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem map_inf_eq (H K : Subgroup G) (f : G →* N) (hf : Function.Injective f) :
    map f (H ⊓ K) = map f H ⊓ map f K

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H K : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ map f (H ⊓ K) = map f H ⊓ map f K

Tactic:
rw [← SetLike.coe_set_eq]

Result:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H K : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ ↑(map f (H ⊓ K)) = ↑(map f H ⊓ map f K)

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H K : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ ↑(map f (H ⊓ K)) = ↑(map f H ⊓ map f K)

Tactic:
simp [Set.image_inter hf]

Result:
no goals