harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
theorem exp_inr (m : M) : exp 𝕜 (inr m : tsze R M) = 1 + inr m

Proof state:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ exp 𝕜 (inr m) = 1 + inr m

Tactic:
rw [exp_def_of_smul_comm, snd_inr, fst_inr, exp_zero, one_smul, inl_one]

Result:
case hx
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ MulOpposite.op (inr m).fst • (inr m).snd = (inr m).fst • (inr m).snd

Proof state:
case hx
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : Ring R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁷ : TopologicalSpace R
inst✝⁶ : TopologicalSpace M
inst✝⁵ : IsTopologicalRing R
inst✝⁴ : IsTopologicalAddGroup M
inst✝³ : ContinuousSMul R M
inst✝² : ContinuousSMul Rᵐᵒᵖ M
inst✝¹ : T2Space R
inst✝ : T2Space M
m : M
⊢ MulOpposite.op (inr m).fst • (inr m).snd = (inr m).fst • (inr m).snd

Tactic:
rw [snd_inr, fst_inr, MulOpposite.op_zero, zero_smul, zero_smul]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₄_of_isShortNF_of_char_three : W.b₄ = -W.a₄

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ 2 * W.a₄ = -W.a₄

Tactic:
linear_combination W.a₄ * CharP.cast_eq_zero R 3

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ W.b₄ = -W.a₄

Tactic:
rw [b₄_of_isShortNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ 2 * W.a₄ = -W.a₄
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive] lemma inv_subset_div_right (hs : 1 ∈ s) : t⁻¹ ⊆ s / t

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s * t⁻¹

Tactic:
exact subset_mul_right _ hs

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s / t

Tactic:
rw [div_eq_mul_inv]

Result:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
hs : 1 ∈ s
⊢ t⁻¹ ⊆ s * t⁻¹
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_zero_C (a : R) : coeff R 0 (C R a) = a

Proof state:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ (coeff R 0) ((C R) a) = a

Tactic:
rw [coeff_C, if_pos rfl]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean
theorem ContinuousLinearMap.hasFDerivWithinAt_of_bilinear {f : G' → E} {g : G' → F}
    {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F} {x : G'} {s : Set G'} (hf : HasFDerivWithinAt f f' s x)
    (hg : HasFDerivWithinAt g g' s x) :
    HasFDerivWithinAt (fun y => B (f y) (g y))
      (B.precompR G' (f x) g' + B.precompL G' f' (g x)) s x

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
B : E →L[𝕜] F →L[𝕜] G
f : G' → E
g : G' → F
f' : G' →L[𝕜] E
g' : G' →L[𝕜] F
x : G'
s : Set G'
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
⊢ HasFDerivWithinAt (fun y => (B (f y)) (g y)) (((precompR G' B) (f x)) g' + ((precompL G' B) f') (g x)) s x

Tactic:
exact (B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp_hasFDerivWithinAt x (hf.prod hg)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/AbelianImages.lean
theorem PreservesImage.iso_hom_ι :
    (PreservesImage.iso F f).hom ≫ Abelian.image.ι (F.map f) = F.map (Abelian.image.ι f)

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasKernels C
inst✝⁷ : HasCokernels C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
inst✝⁴ : HasKernels D
inst✝³ : HasCokernels D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair F
inst✝ : PreservesColimitsOfShape WalkingParallelPair F
X Y : C
f : X ⟶ Y
⊢ (iso F f).hom ≫ image.ι (F.map f) = F.map (image.ι f)

Tactic:
simp [iso]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
theorem rTensorOne'_tmul_one (m : M) : M.rTensorOne' (m ⊗ₜ[R] 1) = m

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
m : ↥M
⊢ M.rTensorOne' (m ⊗ₜ[R] 1) = m

Tactic:
simpa using rTensorOne'_tmul 1 m

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_false_iff : {b : Bool} → b = false ↔ b ≠ true

Proof state:
⊢ ∀ {b : Bool}, b = false ↔ b ≠ true

Tactic:
decide

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousWithinAt_insert_self :
    ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x

Tactic:
simp only [← singleton_union, continuousWithinAt_union, continuousWithinAt_singleton, true_and]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem odd_mul_odd {n m : ℕ} : n % 2 = 1 → m % 2 = 1 → n * m % 2 = 1

Proof state:
n m : ℕ
⊢ n % 2 = 1 → m % 2 = 1 → n * m % 2 = 1

Tactic:
simpa [Nat.ModEq] using @ModEq.mul 2 n 1 m 1

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem sub_mem_ker_iff {x y} : x - y ∈ ker f ↔ f x = f y

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Ring R
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_11
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
x y : M
⊢ x - y ∈ ker f ↔ f x = f y

Tactic:
rw [mem_ker, map_sub, sub_eq_zero]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem val_nsmul (n : ℕ) (y : HomogeneousLocalization 𝒜 x) : (n • y).val = n • y.val

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
n : ℕ
y : HomogeneousLocalization 𝒜 x
⊢ (n • y).val = n • y.val

Tactic:
rw [val_smul, OreLocalization.nsmul_eq_nsmul]

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem ext ⦃inst₁ inst₂ : Distrib R⦄
    (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
    (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) :
    inst₁ = inst₂

Proof state:
R : Type u
inst₁ inst₂ : Distrib R
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ inst₁ = inst₂

Tactic:
rcases inst₁ with @⟨⟨⟩, ⟨⟩⟩

Result:
case mk.mk.mk
R : Type u
inst₂ : Distrib R
mul✝ add✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ mk left_distrib✝ right_distrib✝ = inst₂

Proof state:
case mk.mk.mk
R : Type u
inst₂ : Distrib R
mul✝ add✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ mk left_distrib✝ right_distrib✝ = inst₂

Tactic:
rcases inst₂ with @⟨⟨⟩, ⟨⟩⟩

Result:
case mk.mk.mk.mk.mk.mk
R : Type u
mul✝¹ add✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
mul✝ add✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ mk left_distrib✝¹ right_distrib✝¹ = mk left_distrib✝ right_distrib✝

Proof state:
case mk.mk.mk.mk.mk.mk
R : Type u
mul✝¹ add✝¹ : R → R → R
left_distrib✝¹ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝¹ : ∀ (a b c : R), (a + b) * c = a * c + b * c
mul✝ add✝ : R → R → R
left_distrib✝ : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib✝ : ∀ (a b c : R), (a + b) * c = a * c + b * c
h_add : HAdd.hAdd = HAdd.hAdd
h_mul : HMul.hMul = HMul.hMul
⊢ mk left_distrib✝¹ right_distrib✝¹ = mk left_distrib✝ right_distrib✝

Tactic:
congr

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
lemma eq_inf : @IsClosedImmersion = (topologically IsClosedEmbedding) ⊓
    @SurjectiveOnStalks

Proof state:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ IsClosedEmbedding ⇑(ConcreteCategory.hom f.base) ∧ SurjectiveOnStalks f ↔
    ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsClosedEmbedding) ⊓ @SurjectiveOnStalks) f

Tactic:
rfl

Result:
no goals

Proof state:
⊢ @IsClosedImmersion =
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsClosedEmbedding) ⊓ @SurjectiveOnStalks

Tactic:
ext X Y f

Result:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔
    ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsClosedEmbedding) ⊓ @SurjectiveOnStalks) f

Proof state:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔
    ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsClosedEmbedding) ⊓ @SurjectiveOnStalks) f

Tactic:
rw [isClosedImmersion_iff, and_comm]

Result:
case h.h.h.a
X Y : Scheme
f : X ⟶ Y
⊢ IsClosedEmbedding ⇑(ConcreteCategory.hom f.base) ∧ SurjectiveOnStalks f ↔
    ((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsClosedEmbedding) ⊓ @SurjectiveOnStalks) f
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_union_both (h : a ≤ b) : Ioo a b ∪ {a, b} = Icc a b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
this : Icc a b \ {a, b} ∪ {a, b} = Icc a b
⊢ Ioo a b ∪ {a, b} = Icc a b

Tactic:
rw [← this, Icc_diff_both]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Ioo a b ∪ {a, b} = Icc a b

Tactic:
have : (Icc a b \ {a, b}) ∪ {a, b} = Icc a b := diff_union_of_subset fun
  | x, .inl rfl => left_mem_Icc.mpr h
  | x, .inr rfl => right_mem_Icc.mpr h

Result:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
this : Icc a b \ {a, b} ∪ {a, b} = Icc a b
⊢ Ioo a b ∪ {a, b} = Icc a b
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_midpoint_rev_right (p₁ p₂ p₃ : P) : ∡ p₁ p₂ (midpoint ℝ p₂ p₃) = ∡ p₁ p₂ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ p₁ p₂ (midpoint ℝ p₂ p₃) = ∡ p₁ p₂ p₃

Tactic:
rw [midpoint_comm, oangle_midpoint_right]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Icc_iff_integrableOn_Ioo' (ha : μ {a} ≠ ∞) (hb : μ {b} ≠ ∞) :
    IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Proof state:
α : Type u_1
E : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : PartialOrder α
inst✝ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
ha : μ {a} ≠ ⊤
hb : μ {b} ≠ ⊤
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ

Tactic:
rw [integrableOn_Icc_iff_integrableOn_Ioc' ha, integrableOn_Ioc_iff_integrableOn_Ioo' hb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Sigma.fst) :
    (ofList l).getKey? k' = some k

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Sigma.fst l
⊢ (ofList l).getKey? k' = some k

Tactic:
simp_to_raw using Raw₀.getKey?_insertMany_empty_list_of_mem

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/HEval.lean
theorem powerSeriesFamily_add (g : PowerSeries R) :
    powerSeriesFamily hx (f + g) = powerSeriesFamily hx f + powerSeriesFamily hx g

Proof state:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
f g : PowerSeries R
⊢ powerSeriesFamily hx (f + g) = powerSeriesFamily hx f + powerSeriesFamily hx g

Tactic:
ext1 n

Result:
case h
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
f g : PowerSeries R
n : ℕ
⊢ (powerSeriesFamily hx (f + g)) n = (powerSeriesFamily hx f + powerSeriesFamily hx g) n

Proof state:
case h
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝³ : LinearOrderedCancelAddCommMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : HahnSeries Γ V
hx : 0 < x.orderTop
f g : PowerSeries R
n : ℕ
⊢ (powerSeriesFamily hx (f + g)) n = (powerSeriesFamily hx f + powerSeriesFamily hx g) n

Tactic:
simp [add_smul]

Result:
no goals
-- Mathlib/Control/Traversable/Instances.lean
theorem id_traverse {σ α} (x : σ ⊕ α) :
    Sum.traverse (pure : α → Id α) x = x

Proof state:
σ α : Type u_1
x : σ ⊕ α
⊢ Sum.traverse pure x = x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Probability/Variance.lean
theorem ofReal_variance [IsFiniteMeasure μ] (hX : MemLp X 2 μ) :
    .ofReal (variance X μ) = evariance X μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ eVar[X; μ] ≠ ⊤

Tactic:
exact evariance_ne_top hX

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ ENNReal.ofReal Var[X; μ] = eVar[X; μ]

Tactic:
rw [variance, ENNReal.ofReal_toReal]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ eVar[X; μ] ≠ ⊤
-- Mathlib/Algebra/Order/Group/Multiset.lean
@[simp]
lemma count_nsmul (a : α) (n s) : count a (n • s) = n * count a s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
s : Multiset α
⊢ count a (n • s) = n * count a s

Tactic:
induction n <;> simp [*, succ_nsmul, succ_mul, zero_nsmul]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_add_le_pi_div_two_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) :
    angle x (x + y) ≤ π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ 0 ≤ ‖x‖ / ‖x + y‖

Tactic:
exact div_nonneg (norm_nonneg _) (norm_nonneg _)

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ angle x (x + y) ≤ π / 2

Tactic:
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_le_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ 0 ≤ ‖x‖ / ‖x + y‖
-- Mathlib/Logic/Basic.lean
theorem eq_iff_eq_cancel_right {a b : α} : (∀ {c}, a = c ↔ b = c) ↔ a = b :=
  ⟨fun h ↦ by rw [h], fun h a ↦ by rw [h]⟩

Proof state:
α : Sort u_1
a✝ b : α
h : a✝ = b
a : α
⊢ a✝ = a ↔ b = a

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Sort u_1
a b : α
h : ∀ {c : α}, a = c ↔ b = c
⊢ a = b

Tactic:
rw [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getD_insertMany_list_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (m.insertMany l).getD k' fallback = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v :=
  Raw₀.getD_insertMany_list_of_mem ⟨m.1, _⟩ m.2 k_beq distinct mem

Proof state:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factorThru_add {X Y : C} {P : Subobject Y} (f g : X ⟶ Y) (w : P.Factors (f + g))
    (wf : P.Factors f) (wg : P.Factors g) :
    P.factorThru (f + g) w = P.factorThru f wf + P.factorThru g wg

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
wg : P.Factors g
⊢ P.factorThru (f + g) w ≫ P.arrow = (P.factorThru f wf + P.factorThru g wg) ≫ P.arrow

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
wg : P.Factors g
⊢ P.factorThru (f + g) w = P.factorThru f wf + P.factorThru g wg

Tactic:
ext

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
wg : P.Factors g
⊢ P.factorThru (f + g) w ≫ P.arrow = (P.factorThru f wf + P.factorThru g wg) ≫ P.arrow
-- Mathlib/Data/Finset/Max.lean
theorem max'_insert (a : α) (s : Finset α) (H : s.Nonempty) :
    (insert a s).max' (s.insert_nonempty a) = max (s.max' H) a :=
  (isGreatest_max' _ _).unique <| by
    rw [coe_insert, max_comm]
    exact (isGreatest_max' _ _).insert _

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (insert a ↑s) (a ⊔ s.max' H)

Tactic:
exact (isGreatest_max' _ _).insert _

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (↑(insert a s)) (s.max' H ⊔ a)

Tactic:
rw [coe_insert, max_comm]

Result:
α : Type u_2
inst✝ : LinearOrder α
a : α
s : Finset α
H : s.Nonempty
⊢ IsGreatest (insert a ↑s) (a ⊔ s.max' H)
-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem contMDiff_neg_sphere {m : WithTop ℕ∞} {n : ℕ} [Fact (finrank ℝ E = n + 1)] :
    ContMDiff (𝓡 n) (𝓡 n) m fun x : sphere (0 : E) 1 => -x

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ ContMDiff (𝓡 n) 𝓘(ℝ, E) m Subtype.val

Tactic:
exact contMDiff_coe_sphere

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ ContMDiff (𝓡 n) (𝓡 n) m fun x => -x

Tactic:
apply ContMDiff.codRestrict_sphere

Result:
case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ ContMDiff (𝓡 n) 𝓘(ℝ, E) m fun x => -↑x

Proof state:
case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ ContMDiff (𝓡 n) 𝓘(ℝ, E) m fun x => -↑x

Tactic:
apply contDiff_neg.contMDiff.comp _

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
m : WithTop ℕ∞
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
⊢ ContMDiff (𝓡 n) 𝓘(ℝ, E) m Subtype.val
-- Mathlib/Data/Set/Basic.lean
theorem isEmpty_coe_sort {s : Set α} : IsEmpty (↥s) ↔ s = ∅ :=
  not_iff_not.1 <| by simpa using nonempty_iff_ne_empty

Proof state:
α : Type u
s : Set α
⊢ ¬IsEmpty ↑s ↔ ¬s = ∅

Tactic:
simpa using nonempty_iff_ne_empty

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem ker_orthogonalProjection : LinearMap.ker (orthogonalProjection K) = Kᗮ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
⊢ LinearMap.ker (orthogonalProjection K) = Kᗮ

Tactic:
ext

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x✝ : E
⊢ x✝ ∈ LinearMap.ker (orthogonalProjection K) ↔ x✝ ∈ Kᗮ

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
x✝ : E
⊢ x✝ ∈ LinearMap.ker (orthogonalProjection K) ↔ x✝ ∈ Kᗮ

Tactic:
exact orthogonalProjection_eq_zero_iff

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
theorem quot_neg_mul_neg (x y : PGame) : ⟦-x * -y⟧ = (⟦x * y⟧ : Game)

Proof state:
x y : PGame
⊢ ⟦-x * -y⟧ = ⟦x * y⟧

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_comm {s : Set α} {t : Set β} (f : α → β → M) (hs : s.Finite) (ht : t.Finite) :
    (∏ᶠ i ∈ s, ∏ᶠ j ∈ t, f i j) = ∏ᶠ j ∈ t, ∏ᶠ i ∈ s, f i j

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → β → M
s : Finset α
t : Finset β
⊢ ∏ i ∈ s, ∏ i_1 ∈ t, f i i_1 = ∏ i ∈ t, ∏ i_1 ∈ s, f i_1 i

Tactic:
exact Finset.prod_comm

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → β → M
s : Finset α
t : Finset β
⊢ ∏ᶠ (i : α) (_ : i ∈ ↑s) (j : β) (_ : j ∈ ↑t), f i j = ∏ᶠ (j : β) (_ : j ∈ ↑t) (i : α) (_ : i ∈ ↑s), f i j

Tactic:
simp only [finprod_mem_coe_finset]

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → β → M
s : Finset α
t : Finset β
⊢ ∏ i ∈ s, ∏ i_1 ∈ t, f i i_1 = ∏ i ∈ t, ∏ i_1 ∈ s, f i_1 i

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Set α
t : Set β
f : α → β → M
hs : s.Finite
ht : t.Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ s), f i j

Tactic:
lift s to Finset α using hs

Result:
case intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
t : Set β
f : α → β → M
ht : t.Finite
s : Finset α
⊢ ∏ᶠ (i : α) (_ : i ∈ ↑s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ ↑s), f i j

Proof state:
case intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
t : Set β
f : α → β → M
ht : t.Finite
s : Finset α
⊢ ∏ᶠ (i : α) (_ : i ∈ ↑s) (j : β) (_ : j ∈ t), f i j = ∏ᶠ (j : β) (_ : j ∈ t) (i : α) (_ : i ∈ ↑s), f i j

Tactic:
lift t to Finset β using ht

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → β → M
s : Finset α
t : Finset β
⊢ ∏ᶠ (i : α) (_ : i ∈ ↑s) (j : β) (_ : j ∈ ↑t), f i j = ∏ᶠ (j : β) (_ : j ∈ ↑t) (i : α) (_ : i ∈ ↑s), f i j