harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem map_update_neg [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x : M₁ i) :
    f (update m i (-x)) = -f (update m i x) :=
  eq_neg_of_add_eq_zero_left <| by
    rw [← MultilinearMap.map_update_add, neg_add_cancel, f.map_coord_zero i (update_self i 0 m)]

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x : M₁ i
⊢ f (update m i (-x)) + f (update m i x) = 0

Tactic:
rw [← MultilinearMap.map_update_add, neg_add_cancel, f.map_coord_zero i (update_self i 0 m)]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem erase_idem (f : α →₀ M) (a : α) :
    erase a (erase a f) = erase a f

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
⊢ erase a (erase a f) = erase a f

Tactic:
rw [erase_eq_update_zero, erase_eq_update_zero, update_idem]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem sup_toSubmodule :
    (↑(N ⊔ N') : Submodule R M) = (N : Submodule R M) ⊔ (N' : Submodule R M)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
⊢ ↑(N ⊔ N') = ↑N ⊔ ↑N'

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_sub' {n} (x y : BitVec n) :
    (x - y).toNat = ((x.toNat + (2^n - y.toNat)) % 2^n)

Proof state:
n : Nat
x y : BitVec n
⊢ (x - y).toNat = (x.toNat + (2 ^ n - y.toNat)) % 2 ^ n

Tactic:
rw [toNat_sub, Nat.add_comm]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_sSup {p : α → Prop} {fs : Set (Filter α)} :
    (∃ᶠ x in sSup fs, p x) ↔ ∃ f ∈ fs, ∃ᶠ x in f, p x

Proof state:
α : Type u
p : α → Prop
fs : Set (Filter α)
⊢ (∃ᶠ (x : α) in sSup fs, p x) ↔ ∃ f ∈ fs, ∃ᶠ (x : α) in f, p x

Tactic:
simp only [Filter.Frequently, not_forall, eventually_sSup, exists_prop]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.tendsto_iff (hla : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) :
    Tendsto f la lb ↔ ∀ ib, pb ib → ∃ ia, pa ia ∧ ∀ x ∈ sa ia, f x ∈ sb ib

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
ι' : Sort u_5
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hla : la.HasBasis pa sa
hlb : lb.HasBasis pb sb
⊢ Tendsto f la lb ↔ ∀ (ib : ι'), pb ib → ∃ ia, pa ia ∧ ∀ x ∈ sa ia, f x ∈ sb ib

Tactic:
simp [hlb.tendsto_right_iff, hla.eventually_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem repr_support_subset_of_mem_span (s : Set ι) {m : M}
    (hm : m ∈ span R (b '' s)) : ↑(b.repr m).support ⊆ s

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
s : Set ι
m : M
hm : m ∈ span R (⇑b '' s)
⊢ ↑(b.repr m).support ⊆ s

Tactic:
rcases (Finsupp.mem_span_image_iff_linearCombination _).1 hm with ⟨l, hl, rfl⟩

Result:
case intro.intro
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
s : Set ι
l : ι →₀ R
hl : l ∈ supported R R s
hm : (linearCombination R ⇑b) l ∈ span R (⇑b '' s)
⊢ ↑(b.repr ((linearCombination R ⇑b) l)).support ⊆ s

Proof state:
case intro.intro
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
s : Set ι
l : ι →₀ R
hl : l ∈ supported R R s
hm : (linearCombination R ⇑b) l ∈ span R (⇑b '' s)
⊢ ↑(b.repr ((linearCombination R ⇑b) l)).support ⊆ s

Tactic:
rwa [repr_linearCombination, ← Finsupp.mem_supported R l]

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem _root_.PartialHomeomorph.isLocalStructomorphWithinAt_source_iff {G : StructureGroupoid H}
    [ClosedUnderRestriction G] (f : PartialHomeomorph H H) {x : H} :
    G.IsLocalStructomorphWithinAt (⇑f) f.source x ↔
      x ∈ f.source → ∃ e : PartialHomeomorph H H,
      e ∈ G ∧ e.source ⊆ f.source ∧ EqOn f (⇑e) e.source ∧ x ∈ e.source :=
  haveI : x ∈ f.source ∪ f.sourceᶜ

Proof state:
H : Type u_1
inst✝¹ : TopologicalSpace H
G : StructureGroupoid H
inst✝ : ClosedUnderRestriction G
f : PartialHomeomorph H H
x : H
⊢ x ∈ f.source ∪ f.sourceᶜ

Tactic:
simp_rw [union_compl_self, mem_univ]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma rpow_neg_mul_rpow {a : A} (x : ℝ) (ha : 0 ∉ spectrum ℝ≥0 a)
    (ha' : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
x : ℝ
ha : 0 ∉ spectrum ℝ≥0 a
ha' : autoParam (0 ≤ a) _auto✝
⊢ a ^ (-x) * a ^ x = 1

Tactic:
rw [← rpow_add ha, neg_add_cancel, rpow_zero a]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem negOfNat_add (m n : Nat) : negOfNat m + negOfNat n = negOfNat (m + n)

Proof state:
m n : Nat
⊢ negOfNat m + negOfNat n = negOfNat (m + n)

Tactic:
cases m <;> cases n <;> simp [Nat.succ_add] <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem inclusion_inj_on_objects {S T : Subgroupoid C} (h : S ≤ T) :
    Function.Injective (inclusion h).obj := fun ⟨s, hs⟩ ⟨t, ht⟩ => by
  simpa only [inclusion, Subtype.mk_eq_mk] using id

Proof state:
C : Type u
inst✝ : Groupoid C
S T : Subgroupoid C
h : S ≤ T
x✝¹ x✝ : ↑S.objs
s : C
hs : s ∈ S.objs
t : C
ht : t ∈ S.objs
⊢ (inclusion h).obj ⟨s, hs⟩ = (inclusion h).obj ⟨t, ht⟩ → ⟨s, hs⟩ = ⟨t, ht⟩

Tactic:
simpa only [inclusion, Subtype.mk_eq_mk] using id

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem isLeft_eq_false {x : α ⊕ β} : x.isLeft = false ↔ x.isRight

Proof state:
α : Type u_1
β : Type u_2
x : α ⊕ β
⊢ x.isLeft = false ↔ x.isRight = true

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.lift_map {V W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : V ⟶ W)
    (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) :
    prod.lift f g ≫ prod.map h k = prod.lift (f ≫ h) (g ≫ k)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
V W X Y Z : C
inst✝¹ : HasBinaryProduct W X
inst✝ : HasBinaryProduct Y Z
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ lift f g ≫ map h k = lift (f ≫ h) (g ≫ k)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem IsRoot.map {f : R →+* S} {x : R} {p : R[X]} (h : IsRoot p x) : IsRoot (p.map f) (f x)

Proof state:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
x : R
p : R[X]
h : p.IsRoot x
⊢ (Polynomial.map f p).IsRoot (f x)

Tactic:
rw [IsRoot, eval_map, eval₂_hom, h.eq_zero, f.map_zero]

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma hom_inv_apply {R S : CommSemiRingCat} (e : R ≅ S) (s : S) : e.hom (e.inv s) = s

Proof state:
R S : CommSemiRingCat
e : R ≅ S
s : ↑S
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zipWith_eq_nil_iff {f : α → β → γ} {l l'} : zipWith f l l' = [] ↔ l = [] ∨ l' = []

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l : List α
l' : List β
⊢ zipWith f l l' = [] ↔ l = [] ∨ l' = []

Tactic:
cases l <;> cases l' <;> simp

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
/-- A column partitioned matrix multipiled by a block matrix results in a column partitioned
matrix. -/
lemma fromCols_mul_fromBlocks [Fintype m₁] [Fintype m₂] (A₁ : Matrix m m₁ R) (A₂ : Matrix m m₂ R)
    (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
    (fromCols A₁ A₂) * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ =
      fromCols (A₁ * B₁₁ + A₂ * B₂₁) (A₁ * B₁₂ + A₂ * B₂₂)

Proof state:
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
A₁ : Matrix m m₁ R
A₂ : Matrix m m₂ R
B₁₁ : Matrix m₁ n₁ R
B₁₂ : Matrix m₁ n₂ R
B₂₁ : Matrix m₂ n₁ R
B₂₂ : Matrix m₂ n₂ R
⊢ A₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂)

Tactic:
ext _ (_ | _) <;> simp [mul_apply]

Result:
no goals
-- Mathlib/Algebra/Lie/Matrix.lean
theorem Matrix.lieConj_apply (P A : Matrix n n R) (h : Invertible P) :
    P.lieConj h A = P * A * P⁻¹

Proof state:
R : Type u
inst✝² : CommRing R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
P A : Matrix n n R
h : Invertible P
⊢ (P.lieConj h) A = P * A * P⁻¹

Tactic:
simp [LinearEquiv.conj_apply, Matrix.lieConj, LinearMap.toMatrix'_comp,
  LinearMap.toMatrix'_toLin']

Result:
no goals
-- Mathlib/Dynamics/Newton.lean
theorem newtonMap_apply_of_not_isUnit (h : ¬ (IsUnit <| aeval x (derivative P))) :
    P.newtonMap x = x

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : ¬IsUnit ((aeval x) (derivative P))
⊢ P.newtonMap x = x

Tactic:
simp [newtonMap_apply, Ring.inverse, h]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive (attr := simp) dite_smul]
lemma pow_dite (p : Prop) [Decidable p] (a : α) (b : p → β) (c : ¬ p → β) :
    a ^ (if h : p then b h else c h) = if h : p then a ^ b h else a ^ c h

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Pow α β
p : Prop
inst✝ : Decidable p
a : α
b : p → β
c : ¬p → β
⊢ (a ^ if h : p then b h else c h) = if h : p then a ^ b h else a ^ c h

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/FintypeCat.lean
lemma uSwitchEquiv_naturality {X Y : FintypeCat.{u}} (f : X ⟶ Y)
    (x : uSwitch.{u, v}.obj X) :
    f (X.uSwitchEquiv x) = Y.uSwitchEquiv (uSwitch.map f x)

Proof state:
X Y : FintypeCat
f : X ⟶ Y
x : (uSwitch.obj X).carrier
⊢ f (X.uSwitchEquiv x) = Y.uSwitchEquiv (uSwitch.map f x)

Tactic:
simp only [uSwitch, uSwitchEquiv, Equiv.trans_apply, Equiv.ulift_apply, Equiv.symm_apply_apply]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem measurable_rangeSplitting (hf : MeasurableEmbedding f) :
    Measurable (rangeSplitting f) := fun s hs => by
  rwa [preimage_rangeSplitting hf.injective,
    ← (subtype_coe hf.measurableSet_range).measurableSet_image, ← image_comp,
    coe_comp_rangeFactorization, hf.measurableSet_image]

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (rangeSplitting f ⁻¹' s)

Tactic:
rwa [preimage_rangeSplitting hf.injective,
  ← (subtype_coe hf.measurableSet_range).measurableSet_image, ← image_comp,
  coe_comp_rangeFactorization, hf.measurableSet_image]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem comap_op_mul (M N : Submodule R Aᵐᵒᵖ) :
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) (M * N) =
      comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) N *
        comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) M

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R Aᵐᵒᵖ
⊢ comap (↑(opLinearEquiv R)) (M * N) = comap (↑(opLinearEquiv R)) N * comap (↑(opLinearEquiv R)) M

Tactic:
simp_rw [comap_equiv_eq_map_symm, map_unop_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
lemma fromRows_one_isTotallyUnimodular_iff [DecidableEq n] (A : Matrix m n R) :
    (fromRows A (1 : Matrix n n R)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular :=
  fromRows_isTotallyUnimodular_iff_rows <| fun h i ↦
    ⟨i, 1, funext fun j ↦ by simp [one_apply, Pi.single_apply, eq_comm]⟩

Proof state:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
h : Nonempty n
i j : n
⊢ 1 i j = Pi.single i (↑1) j

Tactic:
simp [one_apply, Pi.single_apply, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem reverse_eq_iff {t t' : RBNode α} : t.reverse = t' ↔ t = t'.reverse

Proof state:
α : Type u_1
t t' : RBNode α
⊢ t.reverse = t' ↔ t = t'.reverse

Tactic:
constructor <;> rintro rfl <;> simp

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem compl_image_coe (s : Set X) : ((↑) '' s : Set (OnePoint X))ᶜ = (↑) '' sᶜ ∪ {∞}

Proof state:
X : Type u_1
s : Set X
⊢ (some '' s)ᶜ = some '' sᶜ ∪ {∞}

Tactic:
rw [coe_injective.compl_image_eq, compl_range_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isEq_iff_eq_eq {o : Ordering} : o.isEq ↔ o = .eq

Proof state:
o : Ordering
⊢ o.isEq = true ↔ o = eq

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem hasDerivWithinAt_Ioi_iff_Ici [PartialOrder 𝕜] :
    HasDerivWithinAt f f' (Ioi x) x ↔ HasDerivWithinAt f f' (Ici x) x

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
inst✝ : PartialOrder 𝕜
⊢ HasDerivWithinAt f f' (Ioi x) x ↔ HasDerivWithinAt f f' (Ici x) x

Tactic:
rw [← Ici_diff_left, hasDerivWithinAt_diff_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findRev?_cons_of_neg (l : Vector α n) (h : ¬p a) :
    findRev? p (l.push a) = findRev? p l

Proof state:
case mk
α : Type
n : Nat
p : α → Bool
a : α
h : ¬p a = true
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ findRev? p ({ toArray := toArray✝, size_toArray := size_toArray✝ }.push a) =
    findRev? p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type
n : Nat
p : α → Bool
a : α
l : Vector α n
h : ¬p a = true
⊢ findRev? p (l.push a) = findRev? p l

Tactic:
cases l

Result:
case mk
α : Type
n : Nat
p : α → Bool
a : α
h : ¬p a = true
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ findRev? p ({ toArray := toArray✝, size_toArray := size_toArray✝ }.push a) =
    findRev? p { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Computability/Partrec.lean
theorem option_getD {f : α → Option β} {g : α → β} (hf : Computable f) (hg : Computable g) :
    Computable fun a => (f a).getD (g a) :=
  (Computable.option_casesOn hf hg (show Computable₂ fun _ b => b from Computable.snd)).of_eq
    fun a => by cases f a <;> rfl

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → Option β
g : α → β
hf : Computable f
hg : Computable g
a : α
⊢ (Option.casesOn (f a) (g a) fun b => b) = (f a).getD (g a)

Tactic:
cases f a <;> rfl

Result:
no goals
-- Mathlib/Data/Set/Monotone.lean
lemma MonotoneOn_insert_iff {a : α} :
    MonotoneOn f (insert a s) ↔
      (∀ b ∈ s, b ≤ a → f b ≤ f a) ∧ (∀ b ∈ s, a ≤ b → f a ≤ f b) ∧ MonotoneOn f s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
⊢ MonotoneOn f (insert a s) ↔ (∀ b ∈ s, b ≤ a → f b ≤ f a) ∧ (∀ b ∈ s, a ≤ b → f a ≤ f b) ∧ MonotoneOn f s

Tactic:
simp [MonotoneOn, forall_and]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/SubMulAction.lean
@[to_additive]
lemma mem_orbit_subMul_iff {p : SubMulAction R M} {x m : p} :
    x ∈ MulAction.orbit R m ↔ (x : M) ∈ MulAction.orbit R (m : M)

Proof state:
R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
x m : ↥p
⊢ x ∈ MulAction.orbit R m ↔ ↑x ∈ MulAction.orbit R ↑m

Tactic:
rw [← val_preimage_orbit, Set.mem_preimage]

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem sym2_cons (a : α) (s : Finset α) (ha : a ∉ s) :
    (s.cons a ha).sym2 = ((s.cons a ha).map <| Sym2.mkEmbedding a).disjUnion s.sym2 (by
      simp [Finset.disjoint_left, ha]) :=
  val_injective <| Multiset.sym2_cons _ _

Proof state:
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b a : α
s : Finset α
ha : a ∉ s
⊢ Disjoint (map (Sym2.mkEmbedding a) (cons a s ha)) s.sym2

Tactic:
simp [Finset.disjoint_left, ha]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma pushouts_le [P.IsStableUnderCobaseChange] : P.pushouts ≤ P

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderCobaseChange
⊢ P.pushouts ≤ P

Tactic:
rwa [← isStableUnderCobaseChange_iff_pushouts_le]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma mul_expect [SMulCommClass ℚ≥0 M M] (s : Finset ι) (f : ι → M) (a : M) :
    a * 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a * f i

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : Semiring M
inst✝¹ : Module ℚ≥0 M
inst✝ : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
a : M
⊢ a * 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a * f i

Tactic:
rw [expect, expect, mul_smul_comm, mul_sum]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_p_pow (n : ℕ) : ‖(p : ℚ_[p]) ^ n‖ = (p : ℝ) ^ (-n : ℤ)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖↑p ^ n‖ = ↑p ^ (-↑n)

Tactic:
rw [← norm_p_zpow, zpow_natCast]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_one_add {A : M} (h : IsUnit A.det) (i : ℤ) : A ^ (1 + i) = A * A ^ i

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
i : ℤ
⊢ A ^ (1 + i) = A * A ^ i

Tactic:
rw [zpow_add h, zpow_one]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_principal {s : Set α} : f =O[𝓟 s] g ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
s : Set α
⊢ f =O[𝓟 s] g ↔ ∃ c, ∀ x ∈ s, ‖f x‖ ≤ c * ‖g x‖

Tactic:
simp_rw [isBigO_iff, eventually_principal]

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

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

Tactic:
rw [← centralizer_univ, ← coe_top, ← hS, centralizer_closure]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
/-- If `f` tends to infinity along a nontrivial filter `l`, then
`x ↦ f x * r` tends to infinity if and only if `0 < r`. -/
lemma tendsto_div_const_atTop_iff_pos [NeBot l] (h : Tendsto f l atTop) :
    Tendsto (fun x ↦ f x / r) l atTop ↔ 0 < r

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto (fun x => f x / r) l atTop ↔ 0 < r

Tactic:
simp only [div_eq_mul_inv, tendsto_mul_const_atTop_iff_pos h, inv_pos]

Result:
no goals
-- Mathlib/Data/Finset/Slice.lean
@[simp] lemma sized_singleton : ({s} : Set (Finset α)).Sized r ↔ #s = r

Proof state:
α : Type u_1
s : Finset α
r : ℕ
⊢ Sized r {s} ↔ #s = r

Tactic:
simp [Sized]

Result:
no goals
-- Mathlib/Algebra/Ring/Basic.lean
@[field_simps]
lemma neg_div' (a b : R) : -(b / a) = -b / a

Proof state:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -(b / a) = -b / a

Tactic:
simp [neg_div]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem mem_twoCocycles_def (f : G × G → A) :
    f ∈ twoCocycles A ↔ ∀ g h j : G,
      A.ρ g (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0 :=
  LinearMap.mem_ker.trans <| by
    rw [funext_iff]
    simp only [dTwo_apply, Prod.mk.eta, Pi.zero_apply, Prod.forall]

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A.V
⊢ (dTwo A) f = 0 ↔ ∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0

Tactic:
rw [funext_iff]

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A.V
⊢ (∀ (x : G × G × G), (dTwo A) f x = 0 x) ↔
    ∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A.V
⊢ (∀ (x : G × G × G), (dTwo A) f x = 0 x) ↔
    ∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0

Tactic:
simp only [dTwo_apply, Prod.mk.eta, Pi.zero_apply, Prod.forall]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem preimage_restrictPreimage {u : Set t} :
    t.restrictPreimage f ⁻¹' u = (fun a : f ⁻¹' t ↦ f a) ⁻¹' (Subtype.val '' u)

Proof state:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set ↑t
⊢ t.restrictPreimage f ⁻¹' u = (fun a => f ↑a) ⁻¹' (Subtype.val '' u)

Tactic:
rw [← preimage_preimage (g := f) (f := Subtype.val), ← image_val_preimage_restrictPreimage,
  preimage_image_eq _ Subtype.val_injective]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
lemma disjoint_insert_erase (ha : a ∉ t) : Disjoint (s.erase a) (insert a t) ↔ Disjoint s t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
⊢ Disjoint (s.erase a) (insert a t) ↔ Disjoint s t

Tactic:
rw [disjoint_erase_comm, erase_insert ha]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem repr_add_sub_repr_add_repr_mem_span (h : IsAdjoinRoot S f) (x y : S) :
    h.repr (x + y) - (h.repr x + h.repr y) ∈ Ideal.span ({f} : Set R[X])

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRoot S f
x y : S
⊢ h.repr (x + y) - (h.repr x + h.repr y) ∈ Ideal.span {f}

Tactic:
rw [← h.ker_map, RingHom.mem_ker, map_sub, h.map_repr, map_add, h.map_repr, h.map_repr, sub_self]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
lemma Complex.hasProd_of_hasSum_log (f : ι → ℂ) (hfn : ∀ n, f n ≠ 0) {a : ℂ}
    (hf : HasSum (fun n => log (f n)) a) : HasProd (fun b ↦ f b) (cexp a) :=
    hf.cexp.congr (by simp [exp_log, hfn])

Proof state:
ι : Type u_2
f : ι → ℂ
hfn : ∀ (n : ι), f n ≠ 0
a : ℂ
hf : HasSum (fun n => log (f n)) a
⊢ ∀ (x : Finset ι), ∏ b ∈ x, (cexp ∘ fun n => log (f n)) b = ∏ b ∈ x, (fun b => f b) b

Tactic:
simp [exp_log, hfn]

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem comp_eq_fun (f : γ → β) : r ∘r (· = f ·) = (r · <| f ·)

Proof state:
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
f : γ → β
x : α
y : γ
⊢ (r ∘r fun x1 x2 => x1 = f x2) x y ↔ r x (f y)

Tactic:
simp [Comp]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
f : γ → β
⊢ (r ∘r fun x1 x2 => x1 = f x2) = fun x1 x2 => r x1 (f x2)

Tactic:
ext x y

Result:
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
f : γ → β
x : α
y : γ
⊢ (r ∘r fun x1 x2 => x1 = f x2) x y ↔ r x (f y)