harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullback_map_eq_pullbackFstFstIso_inv {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S)
    (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S')
    (e₁ : f ≫ i₃ = i₁ ≫ f') (e₂ : g ≫ i₃ = i₂ ≫ g') [Mono i₃] :
    pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ =
      (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv ≫ pullback.snd _ _ ≫ pullback.fst _ _

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ map f g f' g' i₁ i₂ i₃ e₁ e₂ =
    (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv ≫
      snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ fst (snd f' g') i₂

Tactic:
simp only [pullbackFstFstIso_inv, lift_snd_assoc, lift_fst]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.closure_diff_singleton_ssubset (hI : M.Indep I) (he : e ∈ I) :
    M.closure (I \ {e}) ⊂ M.closure I :=
  hI.closure_ssubset_closure <| by simpa

Proof state:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ I
⊢ I \ {e} ⊂ I

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ofNat_dvd_right {n : Nat} {z : Int} : z ∣ (↑n : Int) ↔ z.natAbs ∣ n

Proof state:
n : Nat
z : Int
⊢ z ∣ ↑n ↔ z.natAbs ∣ n

Tactic:
rw [← natAbs_dvd_natAbs, natAbs_ofNat]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem Fintype.not_linearIndependent_iff [Fintype ι] :
    ¬LinearIndependent R v ↔ ∃ g : ι → R, ∑ i, g i • v i = 0 ∧ ∃ i, g i ≠ 0

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Fintype ι
⊢ ¬LinearIndependent R v ↔ ∃ g, ∑ i : ι, g i • v i = 0 ∧ ∃ i, g i ≠ 0

Tactic:
simpa using not_iff_not.2 Fintype.linearIndependent_iff

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem le_csInf_image {s : Set α} (hs : s.Nonempty) {B : α} (hB : B ∈ lowerBounds s) :
    f B ≤ sInf (f '' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
hs : s.Nonempty
B : α
hB : B ∈ lowerBounds s
f' : αᵒᵈ → βᵒᵈ := f
⊢ f B ≤ sInf (f '' s)

Tactic:
exact csSup_image_le (α := αᵒᵈ) (β := βᵒᵈ)
  (show Monotone f' from fun x y hxy => h_mono hxy) hs hB

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
hs : s.Nonempty
B : α
hB : B ∈ lowerBounds s
⊢ f B ≤ sInf (f '' s)

Tactic:
let f' : αᵒᵈ → βᵒᵈ := f

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
hs : s.Nonempty
B : α
hB : B ∈ lowerBounds s
f' : αᵒᵈ → βᵒᵈ := f
⊢ f B ≤ sInf (f '' s)
-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
theorem FinitePlace.norm_def (x : WithVal (v.valuation K)) : ‖embedding v x‖ = adicAbv v x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : WithVal (valuation K v)
⊢ ‖(embedding v) x‖ = (adicAbv v) x

Tactic:
simp [NormedField.toNorm, instNormedFieldValuedAdicCompletion, Valued.toNormedField, Valued.norm,
  Valuation.RankOne.hom, embedding_apply, ← toNNReal_valued_eq_adicAbv]

Result:
no goals
-- Mathlib/Data/BitVec.lean
theorem toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z

Proof state:
w : ℕ
z : ℤ
⊢ (↑z).toFin = ↑z

Tactic:
apply toFin_inj.mpr <| (ofFin_intCast z).symm

Result:
no goals
-- Mathlib/Algebra/Group/NatPowAssoc.lean
theorem npow_mul_comm (m n : ℕ) (x : M) :
    x ^ m * x ^ n = x ^ n * x ^ m

Proof state:
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
m n : ℕ
x : M
⊢ x ^ m * x ^ n = x ^ n * x ^ m

Tactic:
simp only [← npow_add, add_comm]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem algebraMap_injective : Injective (algebraMap R A)

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
⊢ Injective ⇑(algebraMap R A)

Tactic:
simpa [Function.comp_def] using
  (Injective.of_comp_iff (algebraicIndependent_iff_injective_aeval.1 hx) MvPolynomial.C).2
    (MvPolynomial.C_injective _ _)

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem coord_apply_ne (h : i ≠ j) : b.coord i (b j) = 0

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
i j : ι
h : i ≠ j
⊢ (b.coord i) (b j) = 0

Tactic:
rw [coord, AffineMap.coe_mk, ← @Subtype.coe_mk _ (fun j => j ≠ i) j h.symm, ← b.basisOf_apply,
  Basis.sumCoords_self_apply, sub_self]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem le_sum_card [Fintype α] (h : ∀ a, n ≤ #{b ∈ B | a ∈ b}) :
    Fintype.card α * n ≤ ∑ s ∈ B, #s :=
  calc
    Fintype.card α * n ≤ ∑ s ∈ B, #(univ ∩ s) := le_sum_card_inter fun a _ ↦ h a
    _ = ∑ s ∈ B, #s

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), n ≤ #(filter (fun b => a ∈ b) B)
⊢ ∑ s ∈ B, #(univ ∩ s) = ∑ s ∈ B, #s

Tactic:
simp_rw [univ_inter]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
@[reassoc]
lemma tensor_comp {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : LocalizedMonoidal L W ε}
    (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) :
    (f₁ ≫ g₁) ⊗ (f₂ ≫ g₂) = (f₁ ⊗ f₂) ≫ (g₁ ⊗ g₂)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ f₁ ≫ g₁ ⊗ f₂ ≫ g₂ = (f₁ ⊗ f₂) ≫ (g₁ ⊗ g₂)

Tactic:
simp [monoidalCategoryStruct]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Prod.lean
theorem lintegral_id_prod {f : (α × β) → ℝ≥0∞} (hf : Measurable f) (κ : Kernel α β)
    [IsSFiniteKernel κ] (a : α) :
    ∫⁻ p, f p ∂(Kernel.id ×ₖ κ) a = ∫⁻ b, f (a, b) ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α × β → ℝ≥0∞
hf : Measurable f
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
a : α
⊢ ∫⁻ (p : α × β), f p ∂(Kernel.id ×ₖ κ) a = ∫⁻ (b : β), f (a, b) ∂κ a

Tactic:
rw [Kernel.id, lintegral_deterministic_prod _ _ _ hf, id_eq]

Result:
no goals
-- Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean
theorem to_localInverse (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    HasStrictFDerivAt (hf.localInverse f f' a) (f'.symm : F →L[𝕜] E) (f a) :=
  (hf.toPartialHomeomorph f).hasStrictFDerivAt_symm hf.image_mem_toPartialHomeomorph_target <| by
    simpa [← localInverse_def] using hf

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
f : E → F
f' : E ≃L[𝕜] F
a : E
inst✝ : CompleteSpace E
hf : HasStrictFDerivAt f (↑f') a
⊢ HasStrictFDerivAt (↑(toPartialHomeomorph f hf)) (↑f') (↑(toPartialHomeomorph f hf).symm (f a))

Tactic:
simpa [← localInverse_def] using hf

Result:
no goals
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem IccExtend_range (f : Icc a b → β) : range (IccExtend h f) = range f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : ↑(Icc a b) → β
⊢ range (IccExtend h f) = range f

Tactic:
simp only [IccExtend, range_comp f, range_projIcc, image_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_ne_empty_of_left_ne_empty {s : Array α} (h : s ≠ #[]) (t : Array α) :
    s ++ t ≠ #[]

Proof state:
α : Type u_1
s : Array α
h : s ≠ #[]
t : Array α
⊢ s ++ t ≠ #[]

Tactic:
simp_all

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem Ico_mem_nhds_iff [NoMinOrder α] {a b x : α} : Ico a b ∈ 𝓝 x ↔ x ∈ Ioo a b

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b x : α
⊢ Ico a b ∈ 𝓝 x ↔ x ∈ Ioo a b

Tactic:
rw [← interior_Ico, mem_interior_iff_mem_nhds]

Result:
no goals
-- Mathlib/Data/Fintype/BigOperators.lean
theorem Fintype.card_fun [DecidableEq α] [Fintype α] [Fintype β] :
    Fintype.card (α → β) = Fintype.card β ^ Fintype.card α

Proof state:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card (α → β) = card β ^ card α

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Integrals.lean
theorem bernoulli_expectation {p : ℝ≥0∞} (h : p ≤ 1) :
    ∫ b, cond b 1 0 ∂((bernoulli p h).toMeasure) = p.toReal

Proof state:
p : ℝ≥0∞
h : p ≤ 1
⊢ ∫ (b : Bool), bif b then 1 else 0 ∂(bernoulli p h).toMeasure = p.toReal

Tactic:
simp [integral_eq_sum]

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem diag_eq_of_commute_stdBasisMatrix {i j : n} {M : Matrix n n α}
    (hM : Commute (stdBasisMatrix i j 1) M) : M i i = M j j

Proof state:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j : n
M : Matrix n n α
hM : Commute (stdBasisMatrix i j 1) M
this : (stdBasisMatrix i j 1 * M) i j = (M * stdBasisMatrix i j 1) i j
⊢ M i i = M j j

Tactic:
aesop

Result:
no goals

Proof state:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j : n
M : Matrix n n α
hM : Commute (stdBasisMatrix i j 1) M
⊢ M i i = M j j

Tactic:
have := ext_iff.mpr hM i j

Result:
n : Type u_3
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j : n
M : Matrix n n α
hM : Commute (stdBasisMatrix i j 1) M
this : (stdBasisMatrix i j 1 * M) i j = (M * stdBasisMatrix i j 1) i j
⊢ M i i = M j j
-- Mathlib/Data/Set/Lattice.lean
theorem univ_subtype {p : α → Prop} : (univ : Set (Subtype p)) = ⋃ (x) (h : p x), {⟨x, h⟩} :=
  Set.ext fun ⟨x, h⟩ => by simp [h]

Proof state:
α : Type u_1
p : α → Prop
x✝ : Subtype p
x : α
h : p x
⊢ ⟨x, h⟩ ∈ univ ↔ ⟨x, h⟩ ∈ ⋃ x, ⋃ (h : p x), {⟨x, h⟩}

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Order/CompleteLattice/Finset.lean
theorem iInf_singleton (a : α) (s : α → β) : ⨅ x ∈ ({a} : Finset α), s x = s a

Proof state:
α : Type u_2
β : Type u_3
inst✝ : CompleteLattice β
a : α
s : α → β
⊢ ⨅ x ∈ {a}, s x = s a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
lemma evalEval_mk (g : R[X][Y]) : evalEval h (mk p g) = g.evalEval x y

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
p : R[X][Y]
h : Polynomial.evalEval x y p = 0
g : R[X][Y]
⊢ (evalEval h) ((mk p) g) = Polynomial.evalEval x y g

Tactic:
rw [evalEval, lift_mk, eval₂_evalRingHom]

Result:
no goals
-- Mathlib/FieldTheory/Galois/Profinite.lean
lemma mk_toAlgEquivAux [IsGalois k K] (g : limit (asProfiniteGaloisGroupFunctor k K)) (x : K)
    (L : FiniteGaloisIntermediateField k K) (hx' : toAlgEquivAux g x ∈ L.toIntermediateField)
    (hx : x ∈ L.toIntermediateField) :
    (⟨toAlgEquivAux g x, hx'⟩ : L.toIntermediateField) = proj L g ⟨x, hx⟩

Proof state:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
g : ↑(limit (asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
x : K
L : FiniteGaloisIntermediateField k K
hx' : InfiniteGalois.toAlgEquivAux g x ∈ L.toIntermediateField
hx : x ∈ L.toIntermediateField
⊢ ⟨InfiniteGalois.toAlgEquivAux g x, hx'⟩ = ((proj L) g) ⟨x, hx⟩

Tactic:
rw [Subtype.eq_iff, Subtype.coe_mk, toAlgEquivAux_eq_proj_of_mem]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
@[simp] lemma shatterer_idem : 𝒜.shatterer.shatterer = 𝒜.shatterer

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ 𝒜.shatterer.shatterer = 𝒜.shatterer

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma mem_quasispectrum_iff {R A : Type*} [Semifield R] [Ring A]
    [Algebra R A] {a : A} {x : R} :
    x ∈ quasispectrum R a ↔ x = 0 ∨ x ∈ spectrum R a

Proof state:
R : Type u_3
A : Type u_4
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
x : R
⊢ x ∈ quasispectrum R a ↔ x = 0 ∨ x ∈ spectrum R a

Tactic:
simp [quasispectrum_eq_spectrum_union_zero]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma le_add_one_iff : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1

Proof state:
m n : ℕ
⊢ m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem shiftRight_negSucc (m n : ℕ) : -[m+1] >>> (n : ℤ) = -[m >>> n+1]

Proof state:
m n : ℕ
⊢ -[m+1] >>> ↑n = -[m >>> n+1]

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
lemma isLocalDiffeomorph_iff {f : M → N} :
    IsLocalDiffeomorph I J n f ↔ ∀ x : M, IsLocalDiffeomorphAt I J n f 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
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
f : M → N
⊢ IsLocalDiffeomorph I J n f ↔ ∀ (x : M), IsLocalDiffeomorphAt I J n f x

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getThenInsertIfNew?_snd [LawfulBEq α] (h : m.WF) {k : α} {v : β k} :
    (m.getThenInsertIfNew? k v).2 = m.insertIfNew k v

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k : α
v : β k
⊢ (m.getThenInsertIfNew? k v).snd = m.insertIfNew k v

Tactic:
simp_to_raw using congrArg Subtype.val (Raw₀.getThenInsertIfNew?_snd _)

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
/-- The empty set is a block. -/
@[to_additive (attr := simp) "The empty set is a block."]
lemma IsBlock.empty : IsBlock G (∅ : Set X)

Proof state:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
⊢ IsBlock G ∅

Tactic:
simp [IsBlock]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_pair (h : a ≠ b) : #{a, b} = 2

Proof state:
α : Type u_1
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ #{a, b} = 2

Tactic:
rw [card_insert_of_not_mem (not_mem_singleton.2 h), card_singleton]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem eps_pow_five_pos (hPε : 100 ≤ (4 : ℝ) ^ #P.parts * ε ^ 5) : ↑0 < ε ^ 5 :=
  pos_of_mul_pos_right ((by norm_num : (0 : ℝ) < 100).trans_le hPε) <| pow_nonneg (by norm_num) _

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
ε : ℝ
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ 0 < 100

Tactic:
norm_num

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
ε : ℝ
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ 0 ≤ 4

Tactic:
norm_num

Result:
no goals
-- Mathlib/Topology/Connected/LocPathConnected.lean
theorem Topology.IsOpenEmbedding.locPathConnectedSpace {e : Y → X} (he : IsOpenEmbedding e) :
    LocPathConnectedSpace Y :=
  have (y : Y) :
      (𝓝 y).HasBasis (fun s ↦ s ∈ 𝓝 (e y) ∧ IsPathConnected s ∧ s ⊆ range e) (e ⁻¹' ·) :=
    he.basis_nhds <| pathConnected_subset_basis he.isOpen_range (mem_range_self _)
  .of_bases this fun x s ⟨_, hs, hse⟩ ↦ by
    rwa [he.isPathConnected_iff, image_preimage_eq_of_subset hse]

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocPathConnectedSpace X
e : Y → X
he : IsOpenEmbedding e
this : ∀ (y : Y), (𝓝 y).HasBasis (fun s => s ∈ 𝓝 (e y) ∧ IsPathConnected s ∧ s ⊆ range e) fun x => e ⁻¹' x
x : Y
s : Set X
x✝ : s ∈ 𝓝 (e x) ∧ IsPathConnected s ∧ s ⊆ range e
left✝ : s ∈ 𝓝 (e x)
hs : IsPathConnected s
hse : s ⊆ range e
⊢ IsPathConnected (e ⁻¹' s)

Tactic:
rwa [he.isPathConnected_iff, image_preimage_eq_of_subset hse]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Defs.lean
theorem mk_eq_mk_iff_sub_mem (x y : R) : mk I x = mk I y ↔ x - y ∈ I

Proof state:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x y : R
⊢ (mk I) x = (mk I) y ↔ x - y ∈ I

Tactic:
rw [← eq_zero_iff_mem, map_sub, sub_eq_zero]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem norm_inv_eq {x : FreeGroup α} : norm x⁻¹ = norm x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
⊢ x⁻¹.norm = x.norm

Tactic:
simp only [norm, toWord_inv, invRev_length]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem degree_cubic_le : degree (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d) ≤ 3

Proof state:
R : Type u
a b c d : R
inst✝ : Semiring R
⊢ (C a * X ^ 3 + C b * X ^ 2 + C c * X + C d).degree ≤ 3

Tactic:
simpa only [add_assoc] using
  degree_add_le_of_degree_le (degree_C_mul_X_pow_le 3 a)
    (le_trans degree_quadratic_le <| WithBot.coe_le_coe.mpr <| Nat.le_succ 2)

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem adjoin_eq_top_of_adjoin_eq_top [Algebra E K] [IsScalarTower F E K]
    {S : Set K} (hprim : adjoin F S = ⊤) : adjoin E S = ⊤ :=
  restrictScalars_injective F <| by
    rw [restrictScalars_top, ← top_le_iff, ← hprim, adjoin_le_iff,
      coe_restrictScalars, ← adjoin_le_iff]

Proof state:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
S : Set K
hprim : adjoin F S = ⊤
⊢ restrictScalars F (adjoin E S) = restrictScalars F ⊤

Tactic:
rw [restrictScalars_top, ← top_le_iff, ← hprim, adjoin_le_iff,
  coe_restrictScalars, ← adjoin_le_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueFreeOn_empty : G.CliqueFreeOn ∅ n ↔ n ≠ 0

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.CliqueFreeOn ∅ n ↔ n ≠ 0

Tactic:
simp [CliqueFreeOn, Set.subset_empty_iff]

Result:
no goals
-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem constantCoeff_wittStructureRat_zero (Φ : MvPolynomial idx ℚ) :
    constantCoeff (wittStructureRat p Φ 0) = constantCoeff Φ

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℚ
⊢ constantCoeff (wittStructureRat p Φ 0) = constantCoeff Φ

Tactic:
simp only [wittStructureRat, bind₁, map_aeval, xInTermsOfW_zero, constantCoeff_rename,
  constantCoeff_wittPolynomial, aeval_X, constantCoeff_comp_algebraMap, eval₂Hom_zero'_apply,
  RingHom.id_apply]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
@[simp]
lemma compProd_of_not_isSFiniteKernel (μ : Measure α) (κ : Kernel α β) (h : ¬ IsSFiniteKernel κ) :
    μ ⊗ₘ κ = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ = 0

Tactic:
rw [compProd, Kernel.compProd_of_not_isSFiniteKernel_right, Kernel.zero_apply]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ ¬IsSFiniteKernel (Kernel.prodMkLeft Unit κ)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
h : ¬IsSFiniteKernel κ
⊢ ¬IsSFiniteKernel (Kernel.prodMkLeft Unit κ)

Tactic:
rwa [Kernel.isSFiniteKernel_prodMkLeft_unit]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem fundSystem_mk (i : Fin (rank K)) :
    Additive.ofMul (QuotientGroup.mk (fundSystem K i)) = (basisModTorsion K i)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Fin (rank K)
⊢ Additive.ofMul ↑(fundSystem K i) = sorry

Tactic:
simp_rw [fundSystem, Equiv.apply_eq_iff_eq_symm_apply, Additive.ofMul_symm_eq, Quotient.out_eq']

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Fin (rank K)
⊢ ↑(sorry K i) = Additive.toMul sorry
-- Mathlib/Data/Nat/GCD/BigOperators.lean
theorem coprime_list_prod_left_iff {l : List ℕ} {k : ℕ} :
    Coprime l.prod k ↔ ∀ n ∈ l, Coprime n k

Proof state:
l : List ℕ
k : ℕ
⊢ l.prod.Coprime k ↔ ∀ n ∈ l, n.Coprime k

Tactic:
induction l <;> simp [Nat.coprime_mul_iff_left, *]

Result:
no goals
-- Mathlib/Analysis/Complex/RealDeriv.lean
theorem HasDerivAt.ofReal_comp {f : ℝ → ℝ} {u : ℝ} (hf : HasDerivAt f u z) :
    HasDerivAt (fun y : ℝ => ↑(f y) : ℝ → ℂ) u z

Proof state:
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt f u z
⊢ HasDerivAt (fun y => ↑(f y)) (↑u) z

Tactic:
simpa only [ofRealCLM_apply, ofReal_one, real_smul, mul_one] using
  ofRealCLM.hasDerivAt.scomp z hf

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nat_nadd (n : ℕ) : ↑n ♯ a = a + n

Proof state:
a : Ordinal.{u}
n : ℕ
⊢ ↑n ♯ a = a + ↑n

Tactic:
rw [nadd_comm, nadd_nat]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem leftQuotientEquiv_apply {f : G ⧸ H → G} (hf : ∀ q, (f q : G ⧸ H) = q) (q : G ⧸ H) :
    (leftQuotientEquiv (isComplement_range_left hf) q : G) = f q

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
q : G ⧸ H
⊢ ⋯.leftQuotientEquiv q = ⟨f q, ⋯⟩

Tactic:
exact (leftQuotientEquiv (isComplement_range_left hf)).apply_eq_iff_eq_symm_apply.mpr (hf q).symm

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
q : G ⧸ H
⊢ ↑(⋯.leftQuotientEquiv q) = f q

Tactic:
refine (Subtype.ext_iff.mp ?_).trans (Subtype.coe_mk (f q) ⟨q, rfl⟩)

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
q : G ⧸ H
⊢ ⋯.leftQuotientEquiv q = ⟨f q, ⋯⟩
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma hurwitzZetaEven_neg (a : UnitAddCircle) (s : ℂ) :
    hurwitzZetaEven (-a) s = hurwitzZetaEven a s

Proof state:
a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaEven (-a) s = hurwitzZetaEven a s

Tactic:
simp [hurwitzZetaEven]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma add_eq_max_iff : m + n = max m n ↔ m = 0 ∨ n = 0

Proof state:
m n : ℕ
⊢ m + n = max m n ↔ m = 0 ∨ n = 0

Tactic:
omega

Result:
no goals
-- Mathlib/Order/Hom/CompleteLattice.lean
theorem map_iSup₂ [SupSet α] [SupSet β] [sSupHomClass F α β] (f : F) (g : ∀ i, κ i → α) :
    f (⨆ (i) (j), g i j) = ⨆ (i) (j), f (g i j)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
ι : Sort u_6
κ : ι → Sort u_7
inst✝³ : FunLike F α β
inst✝² : SupSet α
inst✝¹ : SupSet β
inst✝ : sSupHomClass F α β
f : F
g : (i : ι) → κ i → α
⊢ f (⨆ i, ⨆ j, g i j) = ⨆ i, ⨆ j, f (g i j)

Tactic:
simp_rw [map_iSup]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/EpiMono.lean
theorem epi_iff_surjective : Epi f ↔ Function.Surjective f

Proof state:
R : Type u
inst✝ : Ring R
X Y : ModuleCat R
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
rw [epi_iff_range_eq_top, LinearMap.range_eq_top]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem mem_map_restrict_ae_iff {β} {s : Set α} {t : Set β} {f : α → β} (hs : MeasurableSet s) :
    t ∈ Filter.map f (ae (μ.restrict s)) ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
s : Set α
t : Set β
f : α → β
hs : MeasurableSet s
⊢ t ∈ Filter.map f (ae (μ.restrict s)) ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0

Tactic:
rw [mem_map, mem_ae_iff, Measure.restrict_apply' hs]

Result:
no goals