harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/Diffeomorph.lean
theorem contMDiffWithinAt_diffeomorph_comp_iff {m} (h : M ≃ₘ^n⟮I, J⟯ N) {f : M' → M} (hm : m ≤ n)
    {s x} : ContMDiffWithinAt I' J m (h ∘ f) s x ↔ ContMDiffWithinAt I' I m f s x :=
  ⟨fun Hhf => by
    simpa only [Function.comp_def, h.symm_apply_apply] using
      (h.symm.contMDiffAt.of_le hm).comp_contMDiffWithinAt _ Hhf,
    fun Hf => (h.contMDiffAt.of_le hm).comp_contMDiffWithinAt _ Hf⟩

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedSpace 𝕜 E'
F : Type u_4
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_5
inst✝⁸ : TopologicalSpace H
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
G : Type u_7
inst✝⁶ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 F G
M : Type u_9
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
M' : Type u_10
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
N : Type u_11
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n m : WithTop ℕ∞
h : M ≃ₘ^n⟮I, J⟯ N
f : M' → M
hm : m ≤ n
s : Set M'
x : M'
Hhf : ContMDiffWithinAt I' J m (⇑h ∘ f) s x
⊢ ContMDiffWithinAt I' I m f s x

Tactic:
simpa only [Function.comp_def, h.symm_apply_apply] using
  (h.symm.contMDiffAt.of_le hm).comp_contMDiffWithinAt _ Hhf

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
lemma schnirelmannDensity_setOf_even : schnirelmannDensity (setOf Even) = 0 :=
  schnirelmannDensity_eq_zero_of_one_not_mem <| by simp

Proof state:
⊢ 1 ∉ setOf Even

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/PureCoherence.lean
theorem naturality_rightUnitor {p : a ⟶ b} {f : b ⟶ c} {pf : a ⟶ c} (η_f : p ≫ f ≅ pf) :
    p ◁ (ρ_ f) ≪≫ η_f = normalizeIsoComp η_f (ρ_ pf) :=
  Iso.ext (by simp)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
p : a ⟶ b
f : b ⟶ c
pf : a ⟶ c
η_f : p ≫ f ≅ pf
⊢ (p ◁ ρ_ f ≪≫ η_f).hom = (normalizeIsoComp η_f (ρ_ pf)).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem _root_.Pi.orthonormalBasis.toBasis {η : Type*} [Fintype η] {ι : η → Type*}
    [∀ i, Fintype (ι i)] {𝕜 : Type*} [RCLike 𝕜] {E : η → Type*} [∀ i, NormedAddCommGroup (E i)]
    [∀ i, InnerProductSpace 𝕜 (E i)] (B : ∀ i, OrthonormalBasis (ι i) 𝕜 (E i)) :
    (Pi.orthonormalBasis B).toBasis =
      ((Pi.basis fun i : η ↦ (B i).toBasis).map (WithLp.linearEquiv 2 _ _).symm)

Proof state:
η : Type u_7
inst✝⁴ : Fintype η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
⊢ (Pi.orthonormalBasis B).toBasis = (Pi.basis fun i => (B i).toBasis).map (WithLp.linearEquiv 2 𝕜 ((j : η) → E j)).symm

Tactic:
ext

Result:
case a.h
η : Type u_7
inst✝⁴ : Fintype η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
i✝¹ : (i : η) × ι i
i✝ : η
⊢ (Pi.orthonormalBasis B).toBasis i✝¹ i✝ =
    ((Pi.basis fun i => (B i).toBasis).map (WithLp.linearEquiv 2 𝕜 ((j : η) → E j)).symm) i✝¹ i✝

Proof state:
case a.h
η : Type u_7
inst✝⁴ : Fintype η
ι : η → Type u_8
inst✝³ : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst✝² : RCLike 𝕜
E : η → Type u_10
inst✝¹ : (i : η) → NormedAddCommGroup (E i)
inst✝ : (i : η) → InnerProductSpace 𝕜 (E i)
B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)
i✝¹ : (i : η) × ι i
i✝ : η
⊢ (Pi.orthonormalBasis B).toBasis i✝¹ i✝ =
    ((Pi.basis fun i => (B i).toBasis).map (WithLp.linearEquiv 2 𝕜 ((j : η) → E j)).symm) i✝¹ i✝

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem eraseIdx_set_lt {l : Vector α n} {i : Nat} {w : i < n} {j : Nat} {a : α} (h : j < i) :
    (l.set i a).eraseIdx j = (l.eraseIdx j).set (i - 1) a

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
w : i < n
j : Nat
a : α
h : j < i
⊢ (l.set i a w).eraseIdx j ⋯ = (l.eraseIdx j ⋯).set (i - 1) a ⋯

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
i j : Nat
a : α
h : j < i
l : Array α
w : i < l.size
⊢ ({ toArray := l, size_toArray := ⋯ }.set i a w).eraseIdx j ⋯ =
    ({ toArray := l, size_toArray := ⋯ }.eraseIdx j ⋯).set (i - 1) a ⋯

Proof state:
case mk
α : Type u_1
i j : Nat
a : α
h : j < i
l : Array α
w : i < l.size
⊢ ({ toArray := l, size_toArray := ⋯ }.set i a w).eraseIdx j ⋯ =
    ({ toArray := l, size_toArray := ⋯ }.eraseIdx j ⋯).set (i - 1) a ⋯

Tactic:
simp [Array.eraseIdx_set_lt, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_replicate_eq_none_iff {n : Nat} {a : α} {p : α → Bool} :
    (replicate n a).find? p = none ↔ n = 0 ∨ !p a

Proof state:
α : Type u_1
n : Nat
a : α
p : α → Bool
⊢ find? p (replicate n a) = none ↔ n = 0 ∨ (!p a) = true

Tactic:
simp [Classical.or_iff_not_imp_left]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem mul_le_of_one_le_left [ExistsAddOfLE α] [MulPosMono α]
    [AddRightMono α] [AddRightReflectLE α]
    (hb : b ≤ 0) (h : 1 ≤ a) : a * b ≤ b

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
hb : b ≤ 0
h : 1 ≤ a
⊢ a * b ≤ b

Tactic:
simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem preimage_coe_Ioo : (some : α → WithBot α) ⁻¹' Ioo a b = Ioo a b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Ioo ↑a ↑b = Ioo a b

Tactic:
simp [← Ioi_inter_Iio]

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem mul_cancel {r : R} {s t : S} : ((s : R) /ₒ t) * (r /ₒ s) = r /ₒ t

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s t : ↥S
⊢ ↑1 * ↑s = 1 * ↑s

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s t : ↥S
⊢ ↑s /ₒ t * (r /ₒ s) = r /ₒ t

Tactic:
simp [oreDiv_mul_char s.1 r t s 1 1 (by simp)]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_inf_mul_relfinrank_of_le (h : A ≤ B) :
    A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B C : IntermediateField F E
h : A ≤ B
⊢ A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C

Tactic:
simpa using congr(toNat $(relrank_inf_mul_relrank_of_le C h))

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma two_mul_ne_two_mul_add_one : 2 * n ≠ 2 * m + 1 :=
  mt (congrArg (· % 2))
    (by rw [Nat.add_comm, add_mul_mod_self_left, mul_mod_right, mod_eq_of_lt] <;> simp)

Proof state:
m n : ℕ
⊢ ¬2 * n % 2 = (2 * m + 1) % 2

Tactic:
rw [Nat.add_comm, add_mul_mod_self_left, mul_mod_right, mod_eq_of_lt] <;> simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
@[simp]
lemma valuation_pow (x : ℤ_[p]) (n : ℕ) : (x ^ n).valuation = n * x.valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ (x ^ n).valuation = n * x.valuation

Tactic:
zify

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ ↑(x ^ n).valuation = ↑n * ↑x.valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
n : ℕ
⊢ ↑(x ^ n).valuation = ↑n * ↑x.valuation

Tactic:
simp [← valuation_coe]

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem isGreatest_himp [GeneralizedHeytingAlgebra α] (a b : α) :
    IsGreatest {w | w ⊓ a ≤ b} (a ⇨ b)

Proof state:
α : Type u
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ IsGreatest {w | w ⊓ a ≤ b} (a ⇨ b)

Tactic:
simp [IsGreatest, mem_upperBounds]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Classical.lean
theorem forall_or_exists_not (P : α → Prop) : (∀ a, P a) ∨ ∃ a, ¬ P a

Proof state:
α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ∃ a, ¬P a

Tactic:
rw [← not_forall]

Result:
α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ¬∀ (x : α), P x

Proof state:
α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ¬∀ (x : α), P x

Tactic:
exact em _

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem mem_ker (v : V₁) : v ∈ f.ker ↔ f v = 0

Proof state:
V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ v ∈ f.ker ↔ f v = 0

Tactic:
erw [f.toAddMonoidHom.mem_ker, coe_toAddMonoidHom]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
@[simp]
lemma equiv_mkInv (L : C ⥤ D) [L.IsLocalization W] {X Y : C} (f : Y ⟶ X) (hf : W f)
    [HasSmallLocalizedHom.{w} W X Y] :
    equiv.{w} W L (mkInv f hf) = (Localization.isoOfHom L W f hf).inv

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
inst✝¹ : L.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
inst✝ : HasSmallLocalizedHom W X Y
⊢ (equiv W L) (mkInv f hf) = (isoOfHom L W f hf).inv

Tactic:
simp only [equiv, mkInv, Equiv.symm_trans_apply, Equiv.symm_symm, homEquiv_symm_apply,
  Equiv.trans_apply, Equiv.symm_apply_apply, homEquiv_isoOfHom_inv]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
theorem MonoidHom.map_zpowers (f : G →* N) (x : G) :
    (Subgroup.zpowers x).map f = Subgroup.zpowers (f x)

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_3
inst✝ : Group N
f : G →* N
x : G
⊢ Subgroup.map f (Subgroup.zpowers x) = Subgroup.zpowers (f x)

Tactic:
rw [Subgroup.zpowers_eq_closure, Subgroup.zpowers_eq_closure, f.map_closure, Set.image_singleton]

Result:
no goals
-- Mathlib/Topology/Order/LeftRight.lean
theorem nhdsLE_sup_nhdsGT (a : α) : 𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a

Tactic:
rw [← nhdsWithin_union, Iic_union_Ioi, nhdsWithin_univ]

Result:
no goals
-- Mathlib/Algebra/Module/FinitePresentation.lean
lemma Module.finitePresentation_of_finite [IsNoetherianRing R] [h : Module.Finite R M] :
    Module.FinitePresentation R M

Proof state:
case mk.intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
s : Finset M
hs : Submodule.span R ↑s = ⊤
⊢ FinitePresentation R M

Tactic:
exact ⟨s, hs, IsNoetherian.noetherian _⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
h : Module.Finite R M
⊢ FinitePresentation R M

Tactic:
obtain ⟨s, hs⟩ := h

Result:
case mk.intro
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
s : Finset M
hs : Submodule.span R ↑s = ⊤
⊢ FinitePresentation R M
-- Mathlib/Data/Finsupp/BigOperators.lean
theorem Multiset.mem_sup_map_support_iff [Zero M] {s : Multiset (ι →₀ M)} {x : ι} :
    x ∈ (s.map Finsupp.support).sup ↔ ∃ f ∈ s, x ∈ f.support :=
  Quot.inductionOn s fun _ ↦ by
    simpa only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sup_coe, List.foldr_map]
    using List.mem_foldr_sup_support_iff

Proof state:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
s : Multiset (ι →₀ M)
x : ι
x✝ : List (ι →₀ M)
⊢ x ∈ (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) x✝)).sup ↔
    ∃ f ∈ Quot.mk (⇑(List.isSetoid (ι →₀ M))) x✝, x ∈ f.support

Tactic:
simpa only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.sup_coe, List.foldr_map]
using List.mem_foldr_sup_support_iff

Result:
no goals
-- Mathlib/Algebra/Ring/Semiconj.lean
theorem sub_left (ha : SemiconjBy a x y) (hb : SemiconjBy b x y) :
    SemiconjBy (a - b) x y

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocRing R
a b x y : R
ha : SemiconjBy a x y
hb : SemiconjBy b x y
⊢ SemiconjBy (a - b) x y

Tactic:
simpa only [sub_eq_add_neg] using ha.add_left hb.neg_left

Result:
no goals
-- Mathlib/Analysis/Convex/Strict.lean
theorem Set.OrdConnected.strictConvex {s : Set β} (hs : OrdConnected s) :
    StrictConvex 𝕜 s

Proof state:
𝕜 : Type u_1
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : OrderTopology β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set β
hs : s.OrdConnected
⊢ StrictConvex 𝕜 s

Tactic:
refine strictConvex_iff_openSegment_subset.2 fun x hx y hy hxy => ?_

Result:
𝕜 : Type u_1
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : OrderTopology β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set β
hs : s.OrdConnected
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
⊢ (fun x y => openSegment 𝕜 x y ⊆ interior s) x y

Proof state:
𝕜 : Type u_1
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : OrderTopology β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set β
hs : s.OrdConnected
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
⊢ (fun x y => openSegment 𝕜 x y ⊆ interior s) x y

Tactic:
rcases hxy.lt_or_lt with hlt | hlt <;> [skip; rw [openSegment_symm]] <;>
  exact
    (openSegment_subset_Ioo hlt).trans
      (isOpen_Ioo.subset_interior_iff.2 <| Ioo_subset_Icc_self.trans <| hs.out ‹_› ‹_›)

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
lemma adjoin_eq_span (s : Set A) :
    (adjoin R s).toSubmodule = Submodule.span R (Subsemigroup.closure (s ∪ star s))

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ (adjoin R s).toSubmodule = Submodule.span R ↑(Subsemigroup.closure (s ∪ star s))

Tactic:
rw [adjoin_toNonUnitalSubalgebra, NonUnitalAlgebra.adjoin_eq_span]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem _root_.Cardinal.natCast_lt_toENat_iff {n : ℕ} {c : Cardinal} :
    ↑n < toENat c ↔ ↑n < c

Proof state:
n : ℕ
c : Cardinal.{u_3}
⊢ ↑n < toENat c ↔ ↑n < c

Tactic:
simp only [← not_le, Cardinal.toENat_le_natCast_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Defs.lean
/-- Equality holds when `a ≠ 0`. See `mul_inv_cancel_left`. -/
lemma mul_inv_left_le (hb : 0 ≤ b) : a * (a⁻¹ * b) ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
hb : 0 ≤ b
⊢ a * (a⁻¹ * b) ≤ b

Tactic:
obtain rfl | ha := eq_or_ne a 0 <;> simp [*]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_diagonal (d₁ : l → α) (d₂ : m → α) :
    fromBlocks (diagonal d₁) 0 0 (diagonal d₂) = diagonal (Sum.elim d₁ d₂)

Proof state:
case a
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
i j : l ⊕ m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) i j = diagonal (Sum.elim d₁ d₂) i j

Tactic:
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [diagonal]

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) = diagonal (Sum.elim d₁ d₂)

Tactic:
ext i j

Result:
case a
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
d₁ : l → α
d₂ : m → α
i j : l ⊕ m
⊢ fromBlocks (diagonal d₁) 0 0 (diagonal d₂) i j = diagonal (Sum.elim d₁ d₂) i j
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factorThru_right {X Y Z : C} {P : Subobject Z} (f : X ⟶ Y) (g : Y ⟶ Z) (h : P.Factors g) :
    f ≫ P.factorThru g h = P.factorThru (f ≫ g) (factors_of_factors_right f h)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : P.Factors g
⊢ f ≫ P.factorThru g h = P.factorThru (f ≫ g) ⋯

Tactic:
apply (cancel_mono P.arrow).mp

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : P.Factors g
⊢ (f ≫ P.factorThru g h) ≫ P.arrow = P.factorThru (f ≫ g) ⋯ ≫ P.arrow

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : P.Factors g
⊢ (f ≫ P.factorThru g h) ≫ P.arrow = P.factorThru (f ≫ g) ⋯ ≫ P.arrow

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem HasFTaylorSeriesUpToOn.add {n : WithTop ℕ∞} {q g} (hf : HasFTaylorSeriesUpToOn n f p s)
    (hg : HasFTaylorSeriesUpToOn n g q s) : HasFTaylorSeriesUpToOn n (f + g) (p + q) s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
p : E → FormalMultilinearSeries 𝕜 E F
n : WithTop ℕ∞
q : E → FormalMultilinearSeries 𝕜 E F
g : E → F
hf : HasFTaylorSeriesUpToOn n f p s
hg : HasFTaylorSeriesUpToOn n g q s
⊢ HasFTaylorSeriesUpToOn n (f + g) (p + q) s

Tactic:
exact HasFTaylorSeriesUpToOn.continuousLinearMap_comp
  (ContinuousLinearMap.fst 𝕜 F F + .snd 𝕜 F F) (hf.prod hg)

Result:
no goals
-- Mathlib/Analysis/Convex/Intrinsic.lean
theorem intrinsicClosure_empty : intrinsicClosure 𝕜 (∅ : Set P) = ∅

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
⊢ intrinsicClosure 𝕜 ∅ = ∅

Tactic:
simp [intrinsicClosure]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_nnnorm_eq_of_L1 (x : WithLp 1 (α × β)) :
    ‖x‖₊ = ‖x.fst‖₊ + ‖x.snd‖₊ :=
  NNReal.eq <| by
    push_cast
    exact prod_norm_eq_of_L1 x

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
⊢ ↑‖x‖₊ = ↑(‖x.1‖₊ + ‖x.2‖₊)

Tactic:
push_cast

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
⊢ ‖x‖ = ‖x.1‖ + ‖x.2‖

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

Tactic:
exact prod_norm_eq_of_L1 x

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem empty [h : IsCyclotomicExtension ∅ A B] : (⊥ : Subalgebra A B) = ⊤

Proof state:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension ∅ A B
⊢ ⊥ = ⊤

Tactic:
simpa [Algebra.eq_top_iff, isCyclotomicExtension_iff] using h

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem subset_iterate_compRel {s t : Set (α × α)} (h : idRel ⊆ s) (n : ℕ) :
    t ⊆ (s ○ ·)^[n] t

Proof state:
case zero
α : Type ua
s : Set (α × α)
h : idRel ⊆ s
t : Set (α × α)
⊢ t ⊆ (fun x => s ○ x)^[0] t

Tactic:
exact Subset.rfl

Result:
no goals

Proof state:
case succ
α : Type ua
s : Set (α × α)
h : idRel ⊆ s
n : ℕ
ihn : ∀ {t : Set (α × α)}, t ⊆ (fun x => s ○ x)^[n] t
t : Set (α × α)
⊢ t ⊆ (fun x => s ○ x)^[n + 1] t

Tactic:
exact (right_subset_compRel h).trans ihn

Result:
no goals

Proof state:
α : Type ua
s t : Set (α × α)
h : idRel ⊆ s
n : ℕ
⊢ t ⊆ (fun x => s ○ x)^[n] t

Tactic:
induction n generalizing t with
| zero => exact Subset.rfl
| succ n ihn => exact (right_subset_compRel h).trans ihn

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem zero_mul : (0 : MvPowerSeries σ R) * φ = 0 :=
  ext fun n => by classical simp [coeff_mul]

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff R n) (0 * φ) = (coeff R n) 0

Tactic:
classical simp [coeff_mul]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff R n) (0 * φ) = (coeff R n) 0

Tactic:
simp [coeff_mul]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_eq_single_of_mem (i : ι) (hi : i ∈ s) (h : ∀ j ∈ s, j ≠ i → f j = 0) :
    𝔼 i ∈ s, f i = f i /ℚ #s

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
i : ι
hi : i ∈ s
h : ∀ j ∈ s, j ≠ i → f j = 0
⊢ 𝔼 i ∈ s, f i = (↑(#s))⁻¹ • f i

Tactic:
rw [expect, sum_eq_single_of_mem _ hi h]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HolderNorm.lean
lemma MemHolder.nnHolderNorm_eq_zero {r : ℝ≥0} {f : X → Y} (hf : MemHolder r f) :
    nnHolderNorm r f = 0 ↔ ∀ x₁ x₂, f x₁ = f x₂

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
⊢ nnHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂

Tactic:
rw [← ENNReal.coe_eq_zero, hf.coe_nnHolderNorm_eq_eHolderNorm, eHolderNorm_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem PartialOrder.rel_of_eq {x y : α} (h : x = y) : x ⊑ y

Proof state:
case refl
α : Sort u
inst✝ : PartialOrder α
x : α
⊢ x ⊑ x

Tactic:
apply rel_refl

Result:
no goals

Proof state:
α : Sort u
inst✝ : PartialOrder α
x y : α
h : x = y
⊢ x ⊑ y

Tactic:
cases h

Result:
case refl
α : Sort u
inst✝ : PartialOrder α
x : α
⊢ x ⊑ x
-- Mathlib/Combinatorics/Colex.lean
@[simp]
lemma mem_initSeg : t ∈ initSeg s ↔ #s = #t ∧ toColex t ≤ toColex s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
s t : Finset α
inst✝ : Fintype α
⊢ t ∈ initSeg s ↔ #s = #t ∧ { ofColex := t } ≤ { ofColex := s }

Tactic:
simp [initSeg]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem mem_nhds_of_pi_mem_nhds {I : Set ι} {s : ∀ i, Set (π i)} (a : ∀ i, π i) (hs : I.pi s ∈ 𝓝 a)
    {i : ι} (hi : i ∈ I) : s i ∈ 𝓝 (a i)

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
I : Set ι
s : (i : ι) → Set (π i)
a : (i : ι) → π i
hs : I.pi s ∈ 𝓝 a
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)

Tactic:
rw [nhds_pi] at hs

Result:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
I : Set ι
s : (i : ι) → Set (π i)
a : (i : ι) → π i
hs : I.pi s ∈ Filter.pi fun i => 𝓝 (a i)
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
I : Set ι
s : (i : ι) → Set (π i)
a : (i : ι) → π i
hs : I.pi s ∈ Filter.pi fun i => 𝓝 (a i)
i : ι
hi : i ∈ I
⊢ s i ∈ 𝓝 (a i)

Tactic:
exact mem_of_pi_mem_pi hs hi

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Defs.lean
theorem xgcdAux_rec {r s t r' s' t' : R} (h : r ≠ 0) :
    xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
⊢ xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

Tactic:
conv =>
  lhs
  rw [xgcdAux]

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
⊢ (if _hr : r = 0 then (r', s', t')
    else
      let q := r' / r;
      let_fun x := ⋯;
      xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t) =
    xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
r s t r' s' t' : R
h : r ≠ 0
⊢ (if _hr : r = 0 then (r', s', t')
    else
      let q := r' / r;
      let_fun x := ⋯;
      xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t) =
    xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t

Tactic:
exact if_neg h

Result:
no goals