harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Basic.lean
theorem filter_and (s : Finset α) : (s.filter fun a => p a ∧ q a) = s.filter p ∩ s.filter q :=
  ext fun _ => by simp [mem_filter, mem_inter, and_comm, and_left_comm, and_self_iff, and_assoc]

Proof state:
α : Type u_1
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
x✝ : α
⊢ x✝ ∈ filter (fun a => p a ∧ q a) s ↔ x✝ ∈ filter p s ∩ filter q s

Tactic:
simp [mem_filter, mem_inter, and_comm, and_left_comm, and_self_iff, and_assoc]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem vecMul_surjective_iff_isUnit {A : Matrix m m R} :
    Function.Surjective A.vecMul ↔ IsUnit A

Proof state:
m : Type u
inst✝² : DecidableEq m
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype m
A : Matrix m m R
⊢ (Function.Surjective fun v => v ᵥ* A) ↔ IsUnit A

Tactic:
rw [vecMul_surjective_iff_exists_left_inverse, exists_left_inverse_iff_isUnit]

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem mkAlgHom_rel {s : A → A → Prop} {x y : A} (w : s x y) :
    mkAlgHom S s x = mkAlgHom S s y

Proof state:
S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
s : A → A → Prop
x y : A
w : s x y
⊢ (mkAlgHom S s) x = (mkAlgHom S s) y

Tactic:
simp [mkAlgHom_def, mkRingHom_def, Quot.sound (Rel.of w)]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_orthogonal_val (u : E) :
    (orthogonalProjection Kᗮ u : E) = u - orthogonalProjection K u :=
  eq_orthogonalProjection_of_mem_orthogonal' (sub_orthogonalProjection_mem_orthogonal _)
    (K.le_orthogonal_orthogonal (orthogonalProjection K u).2) <| by simp

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
u : E
⊢ u = u - ↑((orthogonalProjection K) u) + ↑((orthogonalProjection K) u)

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
theorem shadow_singleton (a : α) : ∂ {{a}} = {∅}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ ∂ {{a}} = {∅}

Tactic:
simp [shadow]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem tendsto_lift' {m : γ → β} {l : Filter γ} :
    Tendsto m l (f.lift' h) ↔ ∀ s ∈ f, ∀ᶠ a in l, m a ∈ h s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
h : Set α → Set β
m : γ → β
l : Filter γ
⊢ Tendsto m l (f.lift' h) ↔ ∀ s ∈ f, ∀ᶠ (a : γ) in l, m a ∈ h s

Tactic:
simp only [Filter.lift', tendsto_lift, tendsto_principal, comp]

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem sumCasesOn_left {f : α → β ⊕ γ} {g : α → β →. σ} {h : α → γ → σ} (hf : Computable f)
    (hg : Partrec₂ g) (hh : Computable₂ h) :
    @Partrec _ σ _ _ fun a => Sum.casesOn (f a) (g a) fun c => Part.some (h a c) :=
  (sumCasesOn_right (sumCasesOn hf (sumInr.comp snd).to₂ (sumInl.comp snd).to₂) hh hg).of_eq
    fun a => by cases f a <;> simp

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
⊢ Sum.casesOn (Sum.casesOn (f a) (fun b => Sum.inr (a, b).2) fun b => Sum.inl (a, b).2) (fun b => Part.some (h a b))
      (g a) =
    Sum.casesOn (f a) (g a) fun c => Part.some (h a c)

Tactic:
cases f a <;> simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.mul_left_eq_zero_iff (h : Monic p) {q : R[X]} : q * p = 0 ↔ q = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.Monic
q : R[X]
⊢ q * p = 0 ↔ q = 0

Tactic:
by_cases hq : q = 0 <;> simp [h.mul_left_ne_zero, hq]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem eq_zero_of_inner_left (hK : Dense (K : Set E)) (h : ∀ v : K, ⟪x, v⟫ = 0) : x = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
hK : Dense ↑K
h : ∀ (v : ↥K), ⟪x, ↑v⟫_𝕜 = 0
this : (fun x_1 => ⟪x, x_1⟫_𝕜) = 0
⊢ x = 0

Tactic:
simpa using congr_fun this x

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem le_rpow_iff_log_le (hx : 0 < x) (hy : 0 < y) : x ≤ y ^ z ↔ log x ≤ z * log y

Proof state:
x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ x ≤ y ^ z ↔ log x ≤ z * log y

Tactic:
rw [← log_le_log_iff hx (rpow_pos_of_pos hy z), log_rpow hy]

Result:
no goals
-- Mathlib/RingTheory/MatrixAlgebra.lean
theorem invFun_add (M N : Matrix n n A) :
    invFun n R A (M + N) = invFun n R A M + invFun n R A N

Proof state:
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M N : Matrix n n A
⊢ invFun n R A (M + N) = invFun n R A M + invFun n R A N

Tactic:
simp [invFun, add_tmul, Finset.sum_add_distrib]

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem lineDerivWithin_congr (hs : EqOn f₁ f s) (hx : f₁ x = f x) :
    lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v :=
  derivWithin_congr (fun _ hy ↦ hs hy) (by simpa using hx)

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 f₁ : E → F
s : Set E
x v : E
hs : EqOn f₁ f s
hx : f₁ x = f x
⊢ f₁ (x + 0 • v) = f (x + 0 • v)

Tactic:
simpa using hx

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem aleph_mul_aleph (o₁ o₂ : Ordinal) : ℵ_ o₁ * ℵ_ o₂ = ℵ_ (max o₁ o₂)

Proof state:
o₁ o₂ : Ordinal.{u_1}
⊢ ℵ_ o₁ * ℵ_ o₂ = ℵ_ (o₁ ⊔ o₂)

Tactic:
rw [Cardinal.mul_eq_max (aleph0_le_aleph o₁) (aleph0_le_aleph o₂), aleph_max]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
theorem leftUnitor_tensor_inv' (X Y : C) :
    (λ_ (X ⊗ Y)).inv = ((λ_ X).inv ⊗ 𝟙 Y) ≫ (α_ (𝟙_ C) X Y).hom

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (λ_ (X ⊗ Y)).inv = ((λ_ X).inv ⊗ 𝟙 Y) ≫ (α_ (𝟙_ C) X Y).hom

Tactic:
monoidal_coherence

Result:
no goals
-- Mathlib/Logic/Embedding/Basic.lean
theorem setValue_eq {α β} (f : α ↪ β) (a : α) (b : β) [∀ a', Decidable (a' = a)]
    [∀ a', Decidable (f a' = b)] : setValue f a b a = b

Proof state:
α : Sort u_1
β : Sort u_2
f : α ↪ β
a : α
b : β
inst✝¹ : (a' : α) → Decidable (a' = a)
inst✝ : (a' : α) → Decidable (f a' = b)
⊢ (f.setValue a b) a = b

Tactic:
simp [setValue]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem dite_ne_right_iff : (dite P A fun _ ↦ b) ≠ b ↔ ∃ h, A h ≠ b

Proof state:
α : Sort u_1
P : Prop
inst✝ : Decidable P
b : α
A : P → α
⊢ (dite P A fun x => b) ≠ b ↔ ∃ h, A h ≠ b

Tactic:
simp only [Ne, dite_eq_right_iff, not_forall]

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem Finset.centerMass_empty : (∅ : Finset ι).centerMass w z = 0

Proof state:
R : Type u_1
E : Type u_3
ι : Type u_5
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
w : ι → R
z : ι → E
⊢ ∅.centerMass w z = 0

Tactic:
simp only [centerMass, sum_empty, smul_zero]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_zero (h : a ≠ 0) : a / 0 = ∞

Proof state:
a : ℝ≥0∞
h : a ≠ 0
⊢ a / 0 = ⊤

Tactic:
simp [div_eq_mul_inv, h]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderIso.lean
theorem preimage_Ioc (e : α ≃o β) (a b : β) : e ⁻¹' Ioc a b = Ioc (e.symm a) (e.symm b)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : β
⊢ ⇑e ⁻¹' Ioc a b = Ioc (e.symm a) (e.symm b)

Tactic:
simp [← Ioi_inter_Iic]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_X_pow : degree ((X : R[X]) ^ n) = n

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
⊢ (X ^ n).degree = ↑n

Tactic:
rw [X_pow_eq_monomial, degree_monomial _ (one_ne_zero' R)]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem preimage_eq (f : α → β) (s : Set β) : f ⁻¹' s = (Function.graph f).preimage s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = (Function.graph f).preimage s

Tactic:
simp [Set.preimage, Rel.preimage, Rel.inv, flip, Rel.image]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem nhdsSet_univ : 𝓝ˢ (univ : Set X) = ⊤

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ 𝓝ˢ univ = ⊤

Tactic:
rw [isOpen_univ.nhdsSet_eq, principal_univ]

Result:
no goals
-- Mathlib/GroupTheory/HNNExtension.lean
theorem of_smul_eq_smul (g : G) (w : NormalWord d) :
    (of g : HNNExtension G A B φ) • w = g • w

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
w : NormalWord d
⊢ of g • w = g • w

Tactic:
simp [instHSMul, SMul.smul, MulAction.toEndHom]

Result:
no goals
-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem integrableOn_image_iff_integrableOn_abs_deriv_smul {s : Set ℝ} {f : ℝ → ℝ} {f' : ℝ → ℝ}
    (hs : MeasurableSet s) (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : InjOn f s)
    (g : ℝ → F) : IntegrableOn g (f '' s) ↔ IntegrableOn (fun x => |f' x| • g (f x)) s

Proof state:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set ℝ
f f' : ℝ → ℝ
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
hf : InjOn f s
g : ℝ → F
⊢ IntegrableOn g (f '' s) volume ↔ IntegrableOn (fun x => |f' x| • g (f x)) s volume

Tactic:
simpa only [det_one_smulRight] using
  integrableOn_image_iff_integrableOn_abs_det_fderiv_smul volume hs
    (fun x hx => (hf' x hx).hasFDerivWithinAt) hf g

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem toReal_eq_toReal_iff' {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ ⊤) :
    x.toReal = y.toReal ↔ x = y

Proof state:
x y : ℝ≥0∞
hx : x ≠ ⊤
hy : y ≠ ⊤
⊢ x.toReal = y.toReal ↔ x = y

Tactic:
simp only [ENNReal.toReal, NNReal.coe_inj, toNNReal_eq_toNNReal_iff' hx hy]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Decomposition.lean
theorem decompose_lhom_ext {N} [AddCommMonoid N] [Module R N] ⦃f g : M →ₗ[R] N⦄
    (h : ∀ i, f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype) : f = g :=
  LinearMap.ext <| (decomposeLinearEquiv ℳ).symm.surjective.forall.mpr <|
    suffices f ∘ₗ (decomposeLinearEquiv ℳ).symm
           = (g ∘ₗ (decomposeLinearEquiv ℳ).symm : (⨁ i, ℳ i) →ₗ[R] N) from
      DFunLike.congr_fun this
    linearMap_ext _ fun i => by
      simp_rw [LinearMap.comp_assoc, decomposeLinearEquiv_symm_comp_lof ℳ i, h]

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ℳ : ι → Submodule R M
inst✝² : Decomposition ℳ
N : Type u_5
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
h : ∀ (i : ι), f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype
i : ι
⊢ (f ∘ₗ ↑(decomposeLinearEquiv ℳ).symm) ∘ₗ lof R ι (fun i => ↥(ℳ i)) i =
    (g ∘ₗ ↑(decomposeLinearEquiv ℳ).symm) ∘ₗ lof R ι (fun i => ↥(ℳ i)) i

Tactic:
simp_rw [LinearMap.comp_assoc, decomposeLinearEquiv_symm_comp_lof ℳ i, h]

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_singleton_left (t : Set E) (x : E) :
    convexJoin 𝕜 {x} t = ⋃ y ∈ t, segment 𝕜 x y

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t : Set E
x : E
⊢ convexJoin 𝕜 {x} t = ⋃ y ∈ t, segment 𝕜 x y

Tactic:
simp [convexJoin]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isIndepSet_induce {F : Set α} {s : Set F} :
    ((⊤ : Subgraph G).induce F).coe.IsIndepSet s ↔ G.IsIndepSet (Subtype.val '' s)

Proof state:
α : Type u_1
G : SimpleGraph α
F : Set α
s : Set ↑F
⊢ (⊤.induce F).coe.IsIndepSet s ↔ G.IsIndepSet (Subtype.val '' s)

Tactic:
simp [Set.Pairwise]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_singleton {a : α} : mapIdx f [a] = [f 0 a]

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
a : α
⊢ mapIdx f [a] = [f 0 a]

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/Language.lean
lemma reverse_mem_reverse : a.reverse ∈ l.reverse ↔ a ∈ l

Proof state:
α : Type u_1
l : Language α
a : List α
⊢ a.reverse ∈ l.reverse ↔ a ∈ l

Tactic:
rw [mem_reverse, List.reverse_reverse]

Result:
no goals
-- Mathlib/Data/Set/Equitable.lean
theorem equitableOn_iff_exists_eq_eq_add_one {s : Set α} {f : α → ℕ} :
    s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, f a = b ∨ f a = b + 1

Proof state:
α : Type u_1
s : Set α
f : α → ℕ
⊢ s.EquitableOn f ↔ ∃ b, ∀ a ∈ s, f a = b ∨ f a = b + 1

Tactic:
simp_rw [equitableOn_iff_exists_le_le_add_one, Nat.le_and_le_add_one_iff]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem rank_pair (x y : PSet) : rank {x, y} = max (succ (rank x)) (succ (rank y))

Proof state:
x y : PSet.{u_1}
⊢ {x, y}.rank = succ x.rank ⊔ succ y.rank

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem adjointAux_inner_left (A : E →L[𝕜] F) (x : E) (y : F) : ⟪adjointAux A y, x⟫ = ⟪y, A x⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace E
A : E →L[𝕜] F
x : E
y : F
⊢ ⟪(adjointAux A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜

Tactic:
rw [adjointAux_apply, toDual_symm_apply, toSesqForm_apply_coe, coe_comp', innerSL_apply_coe,
  Function.comp_apply]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem add_lt_add_iff_left' (a) {b c : Ordinal} : a + b < a + c ↔ b < c

Proof state:
a b c : Ordinal.{u_4}
⊢ a + b < a + c ↔ b < c

Tactic:
rw [← not_le, ← not_le, add_le_add_iff_left]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem mem_support_bernoulli_iff : b ∈ (bernoulli p h).support ↔ cond b (p ≠ 0) (p ≠ 1)

Proof state:
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ b ∈ (bernoulli p h).support ↔ bif b then p ≠ 0 else p ≠ 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tmod_one (a : Int) : tmod a 1 = 0

Proof state:
a : Int
⊢ a.tmod 1 = 0

Tactic:
simp [tmod_def, Int.tdiv_one, Int.one_mul, Int.sub_self]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
lemma lTensor.inverse_comp_lTensor :
    (lTensor.inverse Q hfg hg).comp (lTensor Q g) =
      Submodule.mkQ (p := LinearMap.range (lTensor Q f))

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
⊢ inverse Q hfg hg ∘ₗ lTensor Q g = (range (lTensor Q f)).mkQ

Tactic:
rw [lTensor.inverse, lTensor.inverse_of_rightInverse_comp_lTensor]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler_neg_orientation (x y : E) : (-o).kahler x y = conj (o.kahler x y)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ((-o).kahler x) y = (starRingEnd ℂ) ((o.kahler x) y)

Tactic:
simp [kahler_apply_apply, Complex.conj_ofReal]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Basic.lean
@[to_additive]
lemma hom_inv_apply {X Y : Grp} (e : X ≅ Y) (s : Y) : e.hom (e.inv s) = s

Proof state:
X Y : Grp
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem constantCoeff_invOfUnit (φ : MvPowerSeries σ R) (u : Rˣ) :
    constantCoeff σ R (invOfUnit φ u) = ↑u⁻¹

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
⊢ (constantCoeff σ R) (φ.invOfUnit u) = ↑u⁻¹

Tactic:
rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
⊢ (constantCoeff σ R) (φ.invOfUnit u) = ↑u⁻¹

Tactic:
classical
rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]

Result:
no goals
-- Mathlib/MeasureTheory/PiSystem.lean
theorem isPiSystem_Ixx {Ixx : α → α → Set α} {p : α → α → Prop}
    (Hne : ∀ {a b}, (Ixx a b).Nonempty → p a b)
    (Hi : ∀ {a₁ b₁ a₂ b₂}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)) (f : ι → α)
    (g : ι' → α) : @IsPiSystem α { S | ∃ i j, p (f i) (g j) ∧ Ixx (f i) (g j) = S }

Proof state:
α : Type u_1
ι : Sort u_3
ι' : Sort u_4
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, (Ixx a b).Nonempty → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (a₁ ⊔ a₂) (b₁ ⊓ b₂)
f : ι → α
g : ι' → α
⊢ IsPiSystem {S | ∃ i j, p (f i) (g j) ∧ Ixx (f i) (g j) = S}

Tactic:
simpa only [exists_range_iff] using isPiSystem_Ixx_mem (@Hne) (@Hi) (range f) (range g)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replicate_eq_nil_iff {n : Nat} (a : α) : replicate n a = [] ↔ n = 0

Proof state:
α : Type u_1
n : Nat
a : α
⊢ replicate n a = [] ↔ n = 0

Tactic:
cases n <;> simp

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

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

Tactic:
simp [emultiplicity_eq_zero]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_sdiff (a b c : α) : (a \ b) \ c = a \ (b ⊔ c) :=
  eq_of_forall_ge_iff fun d => by simp_rw [sdiff_le_iff, sup_assoc]

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a \ b) \ c ≤ d ↔ a \ (b ⊔ c) ≤ d

Tactic:
simp_rw [sdiff_le_iff, sup_assoc]

Result:
no goals
-- Mathlib/LinearAlgebra/Isomorphisms.lean
theorem quotientInfEquivSupQuotient_symm_apply_eq_zero_iff {p p' : Submodule R M} {x : ↥(p ⊔ p')} :
    (quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = 0 ↔ (x : M) ∈ p' :=
  (LinearEquiv.symm_apply_eq _).trans <| by simp

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : ↥(p ⊔ p')
⊢ Submodule.Quotient.mk x = (quotientInfEquivSupQuotient p p') 0 ↔ ↑x ∈ p'

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/FintypeCat.lean
/-- `Fintype.Skeleton` is a skeleton of `Fintype`. -/
lemma isSkeleton : IsSkeletonOf FintypeCat Skeleton Skeleton.incl where
  skel := Skeleton.is_skeletal
  eqv

Proof state:
⊢ Skeleton.incl.IsEquivalence

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean
lemma centralizer_coe_iSup {ι : Sort*} (S : ι → Subalgebra R A) :
    centralizer R ((⨆ i, S i : Subalgebra R A) : Set A) = ⨅ i, centralizer R (S i) :=
  eq_of_forall_le_iff fun K ↦ by
    simp_rw [le_centralizer_iff, iSup_le_iff, le_iInf_iff, K.le_centralizer_iff]

Proof state:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_3
S : ι → Subalgebra R A
K : Subalgebra R A
⊢ K ≤ centralizer R ↑(⨆ i, S i) ↔ K ≤ ⨅ i, centralizer R ↑(S i)

Tactic:
simp_rw [le_centralizer_iff, iSup_le_iff, le_iInf_iff, K.le_centralizer_iff]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem bound_of_shell (f : MultilinearMap 𝕜 E G) {ε : ι → ℝ} {C : ℝ} {c : ι → 𝕜}
    (hε : ∀ i, 0 < ε i) (hc : ∀ i, 1 < ‖c i‖)
    (hf : ∀ m : ∀ i, E i, (∀ i, ε i / ‖c i‖ ≤ ‖m i‖) → (∀ i, ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖)
    (m : ∀ i, E i) : ‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
  bound_of_shell_of_norm_map_coord_zero f
    (fun h ↦ by rw [map_coord_zero f _ (norm_eq_zero.1 h), norm_zero]) hε hc hf m

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : Fintype ι
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : MultilinearMap 𝕜 E G
ε : ι → ℝ
C : ℝ
c : ι → 𝕜
hε : ∀ (i : ι), 0 < ε i
hc : ∀ (i : ι), 1 < ‖c i‖
hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
m m✝ : (i : ι) → E i
i✝ : ι
h : ‖m✝ i✝‖ = 0
⊢ ‖f m✝‖ = 0

Tactic:
rw [map_coord_zero f _ (norm_eq_zero.1 h), norm_zero]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem prod_single [CommSemiring k] [CommMonoid G] {s : Finset ι} {a : ι → G} {b : ι → k} :
    (∏ i ∈ s, single (a i) (b i)) = single (∏ i ∈ s, a i) (∏ i ∈ s, b i) :=
  Finset.cons_induction_on s rfl fun a s has ih => by
    rw [prod_cons has, ih, single_mul_single, prod_cons has, prod_cons has]

Proof state:
k : Type u₁
G : Type u₂
ι : Type ui
inst✝¹ : CommSemiring k
inst✝ : CommMonoid G
s✝ : Finset ι
a✝ : ι → G
b : ι → k
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, single (a✝ i) (b i) = single (∏ i ∈ s, a✝ i) (∏ i ∈ s, b i)
⊢ ∏ i ∈ Finset.cons a s has, single (a✝ i) (b i) =
    single (∏ i ∈ Finset.cons a s has, a✝ i) (∏ i ∈ Finset.cons a s has, b i)

Tactic:
rw [prod_cons has, ih, single_mul_single, prod_cons has, prod_cons has]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean
@[reassoc (attr := simp)]
lemma inl_biprodXIso_inv (i : ι) :
    biprod.inl ≫ (biprodXIso K L i).inv = (biprod.inl : K ⟶ K ⊞ L).f i

Proof state:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ biprod.inl ≫ (K.biprodXIso L i).inv = biprod.inl.f i

Tactic:
simp [biprodXIso]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
theorem hasProd_subtype_iff_of_mulSupport_subset {s : Set β} (hf : mulSupport f ⊆ s) :
    HasProd (f ∘ (↑) : s → α) a ↔ HasProd f a :=
  Subtype.coe_injective.hasProd_iff <| by simpa using mulSupport_subset_iff'.1 hf

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set β
hf : mulSupport f ⊆ s
⊢ ∀ x ∉ Set.range fun a => ↑a, f x = 1

Tactic:
simpa using mulSupport_subset_iff'.1 hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)} {k : α}
    (h' : (l.map Prod.fst).contains k = false) :
    (insertMany m l).1.getKey? k = m.getKey? k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
k : α
h' : (List.map Prod.fst l).contains k = false
⊢ (insertMany m l).val.getKey? k = m.getKey? k

Tactic:
simp_to_model [Const.insertMany] using List.getKey?_insertListConst_of_contains_eq_false

Result:
no goals
-- Mathlib/Data/Nat/Periodic.lean
theorem _root_.Function.Periodic.map_mod_nat {α : Type*} {f : ℕ → α} {a : ℕ} (hf : Periodic f a) :
    ∀ n, f (n % a) = f n := fun n => by
  conv_rhs => rw [← Nat.mod_add_div n a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]

Proof state:
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
⊢ f (n % a) = f n

Tactic:
conv_rhs => rw [← Nat.mod_add_div n a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem toSubsemiring_injective :
    Function.Injective (toSubsemiring : Subalgebra R A → Subsemiring A) := fun S T h =>
  ext fun x => by rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
h : S.toSubsemiring = T.toSubsemiring
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem out_fst_mem (e : Sym2 α) : e.out.1 ∈ e :=
  ⟨e.out.2, by rw [Sym2.mk, e.out_eq]⟩

Proof state:
α : Type u_1
e : Sym2 α
⊢ e = s((Quot.out e).1, (Quot.out e).2)

Tactic:
rw [Sym2.mk, e.out_eq]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Multinomial.lean
@[simp] lemma multinomial_empty : multinomial ∅ f = 1

Proof state:
α : Type u_1
f : α → ℕ
⊢ multinomial ∅ f = 1

Tactic:
simp [multinomial]

Result:
no goals