harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean
theorem deriv_tan (x : ℝ) : deriv tan x = 1 / cos x ^ 2 :=
  if h : cos x = 0 then by
    have : ¬DifferentiableAt ℝ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)
    simp [deriv_zero_of_not_differentiableAt this, h, sq]
  else (hasDerivAt_tan h).deriv

Proof state:
x : ℝ
h : cos x = 0
this : ¬DifferentiableAt ℝ tan x
⊢ deriv tan x = 1 / cos x ^ 2

Tactic:
simp [deriv_zero_of_not_differentiableAt this, h, sq]

Result:
no goals

Proof state:
x : ℝ
h : cos x = 0
⊢ deriv tan x = 1 / cos x ^ 2

Tactic:
have : ¬DifferentiableAt ℝ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)

Result:
x : ℝ
h : cos x = 0
this : ¬DifferentiableAt ℝ tan x
⊢ deriv tan x = 1 / cos x ^ 2
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernelSubobjectIso_comp_kernel_map (sq : Arrow.mk f ⟶ Arrow.mk f') :
    (kernelSubobjectIso _).hom ≫ kernel.map f f' sq.1 sq.2 sq.3.symm =
      kernelSubobjectMap sq ≫ (kernelSubobjectIso _).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasKernel f'
sq : Arrow.mk f ⟶ Arrow.mk f'
⊢ (kernelSubobjectIso f).hom ≫ kernel.map f f' sq.left sq.right ⋯ = kernelSubobjectMap sq ≫ (kernelSubobjectIso f').hom

Tactic:
simp [← Iso.comp_inv_eq, kernel_map_comp_kernelSubobjectIso_inv]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem bihimp_left_comm : a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)

Tactic:
simp_rw [← bihimp_assoc, bihimp_comm]

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem exists_mem_of_ne_zero {s : Multiset α} : s ≠ 0 → ∃ a : α, a ∈ s :=
  Quot.inductionOn s fun l hl =>
    match l, hl with
    | [], h => False.elim <| h rfl
    | a :: l, _ => ⟨a, by simp⟩

Proof state:
α : Type u_1
s : Multiset α
l✝ : List α
hl : Quot.mk (⇑(isSetoid α)) l✝ ≠ 0
a : α
l : List α
x✝ : Quot.mk (⇑(isSetoid α)) (a :: l) ≠ 0
⊢ a ∈ Quot.mk (⇑(isSetoid α)) (a :: l)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem map_comap_eq (H : Subgroup N) : map f (comap f H) = f.range ⊓ H :=
  SetLike.ext' <| by
    rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
⊢ ↑(map f (comap f H)) = ↑(f.range ⊓ H)

Tactic:
rw [coe_map, coe_comap, Set.image_preimage_eq_inter_range, coe_inf, coe_range, Set.inter_comm]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_monomial (n : ℕ) (ha : a ≠ 0) : degree (monomial n a) = n

Proof state:
R : Type u
a : R
inst✝ : Semiring R
n : ℕ
ha : a ≠ 0
⊢ ((monomial n) a).degree = ↑n

Tactic:
rw [degree, support_monomial n ha, max_singleton, Nat.cast_withBot]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Hom.lean
theorem id_comp (f : X →ₑ[φ] Y) :
    (MulActionHom.id N).comp f = f :=
  ext fun x => by rw [comp_apply, id_apply]

Proof state:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
f : X →ₑ[φ] Y
x : X
⊢ ((MulActionHom.id N).comp f) x = f x

Tactic:
rw [comp_apply, id_apply]

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem InjOn.pairwise_image {s : Set ι} (h : s.InjOn f) :
    (f '' s).Pairwise r ↔ s.Pairwise (r on f)

Proof state:
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
s : Set ι
h : InjOn f s
⊢ (f '' s).Pairwise r ↔ s.Pairwise (r on f)

Tactic:
simp +contextual [h.eq_iff, Set.Pairwise]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
lemma const (x : β) : IsCauSeq abv fun _ ↦ x :=
  fun ε ε0 ↦ ⟨0, fun j _ => by simpa [abv_zero] using ε0⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
x : β
ε : α
ε0 : ε > 0
j : ℕ
x✝ : j ≥ 0
⊢ abv ((fun x_1 => x) j - (fun x_1 => x) 0) < ε

Tactic:
simpa [abv_zero] using ε0

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem finSepDegree_mul_finSepDegree_of_isAlgebraic
    [Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic E K] :
    finSepDegree F E * finSepDegree E K = finSepDegree F K

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsAlgebraic E K
⊢ finSepDegree F E * finSepDegree E K = finSepDegree F K

Tactic:
simpa only [Nat.card_prod] using Nat.card_congr (embProdEmbOfIsAlgebraic F E K)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean
theorem zero_iff_nonpos : smoothTransition x = 0 ↔ x ≤ 0

Proof state:
x : ℝ
⊢ x.smoothTransition = 0 ↔ x ≤ 0

Tactic:
simp only [smoothTransition, _root_.div_eq_zero_iff, (pos_denom x).ne', zero_iff_nonpos, or_false]

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem maximum_ne_bot_of_length_pos (h : 0 < l.length) : l.maximum ≠ ⊥ :=
  match l, h with | _ :: _, _ => by simp [maximum_cons]

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l : List α
h : 0 < l.length
head✝ : α
tail✝ : List α
x✝ : 0 < (head✝ :: tail✝).length
⊢ (head✝ :: tail✝).maximum ≠ ⊥

Tactic:
simp [maximum_cons]

Result:
no goals
-- Mathlib/Order/Filter/Finite.lean
theorem iInf_sets_eq_finite' (f : ι → Filter α) :
    (⨅ i, f i).sets = ⋃ t : Finset (PLift ι), (⨅ i ∈ t, f (PLift.down i)).sets

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
⊢ (⨅ i, f i).sets = ⋃ t, (⨅ i ∈ t, f i.down).sets

Tactic:
rw [← iInf_sets_eq_finite, ← Equiv.plift.surjective.iInf_comp, Equiv.plift_apply]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem HasFDerivWithinAt.cpow (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x)
    (h0 : f x ∈ slitPlane) : HasFDerivWithinAt (fun x => f x ^ g x)
      ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') s x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : E → ℂ
f' g' : E →L[ℂ] ℂ
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
h0 : f x ∈ slitPlane
⊢ HasFDerivWithinAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') s x

Tactic:
convert
  (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp_hasFDerivWithinAt x (hf.prod hg)

Result:
no goals
-- Mathlib/Geometry/RingedSpace/Stalks.lean
theorem stalkMap_germ {X Y : PresheafedSpace.{_, _, v} C} (α : X ⟶ Y) (U : Opens Y)
    (x : X) (hx : α x ∈ U) :
    Y.presheaf.germ U (α x) hx ≫ α.stalkMap x = α.c.app (op U) ≫
      X.presheaf.germ ((Opens.map α.base).obj U) x hx

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
U : Opens ↑↑Y
x : ↑↑X
hx : (ConcreteCategory.hom α.base) x ∈ U
⊢ Y.presheaf.germ U ((ConcreteCategory.hom α.base) x) hx ≫ Hom.stalkMap α x =
    α.c.app (op U) ≫ X.presheaf.germ ((Opens.map α.base).obj U) x hx

Tactic:
rw [Hom.stalkMap, stalkFunctor_map_germ_assoc, stalkPushforward_germ]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem restrict_mrange (f : M →* N) : mrange (f.restrict S) = S.map f

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
S : Submonoid M
f : M →* N
⊢ mrange (f.restrict S) = map f S

Tactic:
simp [SetLike.ext_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma pentagon_aux₁ {X₁ X₂ X₃ Y₁ : LocalizedMonoidal L W ε} (i : X₁ ≅ Y₁) :
    ((i.hom ▷ X₂) ▷ X₃) ≫ (α_ Y₁ X₂ X₃).hom ≫ (i.inv ▷ (X₂ ⊗ X₃)) = (α_ X₁ X₂ X₃).hom

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₁ X₂ X₃ Y₁ : LocalizedMonoidal L W ε
i : X₁ ≅ Y₁
⊢ i.hom ▷ X₂ ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom ≫ i.inv ▷ (X₂ ⊗ X₃) = (α_ X₁ X₂ X₃).hom

Tactic:
simp only [associator_naturality₁_assoc, ← whiskerRight_comp,
  Iso.hom_inv_id, whiskerRight_id, comp_id]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Grothendieck.lean
theorem covering_iff_covers_id (S : Sieve X) : S ∈ J X ↔ J.Covers S (𝟙 X)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : C
J : GrothendieckTopology C
S : Sieve X
⊢ S ∈ J X ↔ J.Covers S (𝟙 X)

Tactic:
simp [covers_iff]

Result:
no goals
-- Mathlib/Order/Irreducible.lean
theorem supPrime_iff_supIrred : SupPrime a ↔ SupIrred a :=
  ⟨SupPrime.supIrred,
    And.imp_right fun h b c => by simp_rw [← inf_eq_left, inf_sup_left]; exact @h _ _⟩

Proof state:
α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ⊓ b ⊔ a ⊓ c = a → a ⊓ b = a ∨ a ⊓ c = a

Tactic:
exact @h _ _

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ≤ b ⊔ c → a ≤ b ∨ a ≤ c

Tactic:
simp_rw [← inf_eq_left, inf_sup_left]

Result:
α : Type u_2
inst✝ : DistribLattice α
a : α
h : ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a
b c : α
⊢ a ⊓ b ⊔ a ⊓ c = a → a ⊓ b = a ∨ a ⊓ c = a
-- Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
theorem mem_balancedCore_iff : x ∈ balancedCore 𝕜 s ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
x : E
⊢ x ∈ balancedCore 𝕜 s ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t

Tactic:
simp_rw [balancedCore, mem_sUnion, mem_setOf_eq, and_assoc]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem IsNormal.apply_le_nfp (H : IsNormal f) {a b} : f b ≤ nfp f a ↔ b ≤ nfp f a :=
  ⟨H.le_apply.trans, fun h => by simpa only [H.nfp_fp] using H.le_iff.2 h⟩

Proof state:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
h : b ≤ nfp f a
⊢ f b ≤ nfp f a

Tactic:
simpa only [H.nfp_fp] using H.le_iff.2 h

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
@[simp]
lemma self_pow_inv (r : ℕ) : padicValRat p ((p : ℚ) ^ r)⁻¹ = -r

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
r : ℕ
⊢ padicValRat p (↑p ^ r)⁻¹ = -↑r

Tactic:
rw [padicValRat.inv, neg_inj, padicValRat.pow (Nat.cast_ne_zero.mpr hp.elim.ne_zero),
    padicValRat.self hp.elim.one_lt, mul_one]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem neg_le {a b : EReal} : -a ≤ b ↔ -b ≤ a

Proof state:
a b : EReal
⊢ -a ≤ b ↔ -b ≤ a

Tactic:
rw [← neg_le_neg_iff, neg_neg]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean
theorem GammaIntegral_eq_mellin : GammaIntegral = mellin fun x => ↑(Real.exp (-x)) :=
  funext fun s => by simp only [mellin, GammaIntegral, smul_eq_mul, mul_comm]

Proof state:
s : ℂ
⊢ s.GammaIntegral = mellin (fun x => ↑(rexp (-x))) s

Tactic:
simp only [mellin, GammaIntegral, smul_eq_mul, mul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IndYoneda.lean
@[reassoc (attr := simp)]
lemma coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π (i : I) :
    (coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ limit.π (F.rightOp ⋙ coyoneda) i =
      coyoneda.map (colimit.ι F ⟨i⟩).op

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
I : Type v₁
inst✝¹ : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝ : HasColimit F
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ limit.π (F.rightOp ⋙ coyoneda) i = coyoneda.map (colimit.ι F (op i)).op

Tactic:
simp only [coyonedaOpColimitIsoLimitCoyoneda', Functor.mapIso_symm, Iso.trans_hom, Iso.symm_hom,
  Functor.mapIso_inv, Category.assoc, preservesLimitIso_hom_π, ← Functor.map_comp,
  limitRightOpIsoOpColimit_inv_comp_π]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_add_one (a : α) : ⌈a + 1⌉ = ⌈a⌉ + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ⌈a + 1⌉ = ⌈a⌉ + 1

Tactic:
rw [← ceil_add_int a (1 : ℤ), cast_one]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_mul [Semiring α] (m n) : ((m * n : PosNum) : α) = m * n

Proof state:
α : Type u_1
inst✝ : Semiring α
m n : PosNum
⊢ ↑(m * n) = ↑m * ↑n

Tactic:
rw [← cast_to_nat, mul_to_nat, Nat.cast_mul, cast_to_nat, cast_to_nat]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem quotientMap_comp_mk {J : Ideal R} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided]
    {f : R →+* S} (H : J ≤ I.comap f) :
    (quotientMap I f H).comp (Quotient.mk J) = (Quotient.mk I).comp f :=
  RingHom.ext fun x => by simp only [Function.comp_apply, RingHom.coe_comp, Ideal.quotientMap_mk]

Proof state:
R : Type u
inst✝³ : Ring R
S : Type v
inst✝² : Ring S
J : Ideal R
I : Ideal S
inst✝¹ : I.IsTwoSided
inst✝ : J.IsTwoSided
f : R →+* S
H : J ≤ comap f I
x : R
⊢ ((quotientMap I f H).comp (Quotient.mk J)) x = ((Quotient.mk I).comp f) x

Tactic:
simp only [Function.comp_apply, RingHom.coe_comp, Ideal.quotientMap_mk]

Result:
no goals
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem Directed.iSup_inf_eq (h : Directed (· ≤ ·) f) :
    (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

Proof state:
ι : Sort u_1
α : Type u_2
inst✝¹ : CompleteLattice α
f : ι → α
inst✝ : IsCompactlyGenerated α
a : α
h : Directed (fun x1 x2 => x1 ≤ x2) f
⊢ (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

Tactic:
rw [iSup, h.directedOn_range.sSup_inf_eq, iSup_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem succ_mul {x y : BitVec w} : (x + 1#w) * y = x * y + y

Proof state:
w : Nat
x y : BitVec w
⊢ (x + 1#w) * y = x * y + y

Tactic:
simp [BitVec.mul_comm, BitVec.mul_add]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Basic.lean
lemma mul_mem_left (x y) (hy : y ∈ I) : x * y ∈ I

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
hy : y ∈ I
⊢ x * y ∈ I

Tactic:
simpa using I.ringCon.mul (I.ringCon.refl x) hy

Result:
no goals
-- Mathlib/Tactic/Abel.lean
lemma subst_into_smulg {α} [AddCommGroup α]
    (l r tl tr t) (prl : l = tl) (prr : r = tr)
    (prt : @smulg α _ tl tr = t) : smulg l r = t

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
l : ℤ
r : α
tl : ℤ
tr t : α
prl : l = tl
prr : r = tr
prt : smulg tl tr = t
⊢ smulg l r = t

Tactic:
simp [prl, prr, prt]

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Prod.lean
theorem FG.prod {sb : Submodule R M} {sc : Submodule R P} (hsb : sb.FG) (hsc : sc.FG) :
    (sb.prod sc).FG :=
  let ⟨tb, htb⟩ := fg_def.1 hsb
  let ⟨tc, htc⟩ := fg_def.1 hsc
  fg_def.2
    ⟨LinearMap.inl R M P '' tb ∪ LinearMap.inr R M P '' tc, (htb.1.image _).union (htc.1.image _),
      by rw [LinearMap.span_inl_union_inr, htb.2, htc.2]⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type u_3
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
sb : Submodule R M
sc : Submodule R P
hsb : sb.FG
hsc : sc.FG
tb : Set M
htb : tb.Finite ∧ span R tb = sb
tc : Set P
htc : tc.Finite ∧ span R tc = sc
⊢ span R (⇑(LinearMap.inl R M P) '' tb ∪ ⇑(LinearMap.inr R M P) '' tc) = sb.prod sc

Tactic:
rw [LinearMap.span_inl_union_inr, htb.2, htc.2]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_inter_on {f : α → β} {s t : Set α} (h : ∀ x ∈ t, ∀ y ∈ s, f x = f y → x = y) :
    f '' (s ∩ t) = f '' s ∩ f '' t :=
  (image_inter_subset _ _ _).antisymm
    fun b ⟨⟨a₁, ha₁, h₁⟩, ⟨a₂, ha₂, h₂⟩⟩ ↦
      have : a₂ = a₁ := h _ ha₂ _ ha₁ (by simp [*])
      ⟨a₁, ⟨ha₁, this ▸ ha₂⟩, h₁⟩

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
h : ∀ x ∈ t, ∀ y ∈ s, f x = f y → x = y
b : β
x✝ : b ∈ f '' s ∩ f '' t
a₁ : α
ha₁ : a₁ ∈ s
h₁ : f a₁ = b
a₂ : α
ha₂ : a₂ ∈ t
h₂ : f a₂ = b
⊢ f a₂ = f a₁

Tactic:
simp [*]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem takeD_nil (n) (a : α) : takeD n [] a = replicate n a

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

Tactic:
induction n <;> simp [*, replicate_succ]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
lemma Shatters.mono_right (h : t ⊆ s) (hs : 𝒜.Shatters s) : 𝒜.Shatters t := fun u hu ↦ by
  obtain ⟨v, hv, rfl⟩ := hs (hu.trans h); exact ⟨v, hv, inf_congr_right hu <| inf_le_of_left_le h⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
h : t ⊆ s
hs : 𝒜.Shatters s
u : Finset α
hu : u ⊆ t
⊢ ∃ u_1 ∈ 𝒜, t ∩ u_1 = u

Tactic:
obtain ⟨v, hv, rfl⟩ := hs (hu.trans h)

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
h : t ⊆ s
hs : 𝒜.Shatters s
v : Finset α
hv : v ∈ 𝒜
hu : s ∩ v ⊆ t
⊢ ∃ u ∈ 𝒜, t ∩ u = s ∩ v

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s t : Finset α
h : t ⊆ s
hs : 𝒜.Shatters s
v : Finset α
hv : v ∈ 𝒜
hu : s ∩ v ⊆ t
⊢ ∃ u ∈ 𝒜, t ∩ u = s ∩ v

Tactic:
exact ⟨v, hv, inf_congr_right hu <| inf_le_of_left_le h⟩

Result:
no goals
-- Mathlib/Data/Fintype/BigOperators.lean
@[simp] lemma card_piFinset (s : ∀ i, Finset (α i)) :
    #(piFinset s) = ∏ i, #(s i)

Proof state:
ι : Type u_4
α : ι → Type u_6
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
s : (i : ι) → Finset (α i)
⊢ #(piFinset s) = ∏ i : ι, #(s i)

Tactic:
simp [piFinset, card_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_unitOfList [EquivBEq α] [LawfulHashable α]
    {l : List α}
    (distinct : l.Pairwise (fun a b => (a == b) = false)) :
    (unitOfList l).size = l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
distinct : List.Pairwise (fun a b => (a == b) = false) l
⊢ (unitOfList l).size = l.length

Tactic:
simp_to_raw using Raw₀.Const.size_insertManyIfNewUnit_empty_list

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma eq_one_of_isUnit_natCast {n : ℕ} (h : IsUnit (n : ZMod 0)) : n = 1

Proof state:
n : ℕ
h : IsUnit ↑n
⊢ n = 1

Tactic:
rw [← Nat.mod_zero n, ← val_natCast, val_unit'.mp h]

Result:
no goals
-- Mathlib/RingTheory/Ideal/IsPrincipal.lean
theorem associatesEquivIsPrincipal_map_one :
    (associatesEquivIsPrincipal R 1 : Ideal R) = 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ↑((associatesEquivIsPrincipal R) 1) = 1

Tactic:
rw [one_eq_mk_one, associatesEquivIsPrincipal_apply, span_singleton_one, one_eq_top]

Result:
no goals
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.zero_smul (hs : StarConvex 𝕜 0 s) (c : 𝕜) : StarConvex 𝕜 0 (c • s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedCommSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : StarConvex 𝕜 0 s
c : 𝕜
⊢ StarConvex 𝕜 0 (c • s)

Tactic:
simpa using hs.smul c

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem card_le_card_mul_self' : s.card ≤ (s * s).card

Proof state:
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s : Finset α
⊢ #s ≤ #(s * s)

Tactic:
cases s.eq_empty_or_nonempty <;> simp [card_le_card_mul_right, *]

Result:
no goals
-- Mathlib/Data/Finset/Preimage.lean
theorem preimage_inter [DecidableEq α] [DecidableEq β] {f : α → β} {s t : Finset β}
    (hs : Set.InjOn f (f ⁻¹' ↑s)) (ht : Set.InjOn f (f ⁻¹' ↑t)) :
    (preimage (s ∩ t) f fun _ hx₁ _ hx₂ =>
        hs (mem_of_mem_inter_left hx₁) (mem_of_mem_inter_left hx₂)) =
      preimage s f hs ∩ preimage t f ht :=
  Finset.coe_injective (by simp)

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s t : Finset β
hs : InjOn f (f ⁻¹' ↑s)
ht : InjOn f (f ⁻¹' ↑t)
⊢ ↑((s ∩ t).preimage f ⋯) = ↑(s.preimage f hs ∩ t.preimage f ht)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Basic.lean
theorem tendstoLocallyUniformly_iff {ι : Type*} [TopologicalSpace β] {F : ι → β → α} {f : β → α}
    {p : Filter ι} :
    TendstoLocallyUniformly F f p ↔
      ∀ ε > 0, ∀ x : β, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, edist (f y) (F n y) < ε

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε

Tactic:
simp only [← tendstoLocallyUniformlyOn_univ, tendstoLocallyUniformlyOn_iff, mem_univ,
  forall_const, exists_prop, nhdsWithin_univ]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem measure_diff_symm (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ)
    (h : μ s = μ t) (hfin : μ (s ∩ t) ≠ ∞) : μ (s \ t) = μ (t \ s)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
h : μ s = μ t
hfin : μ (s ∩ t) ≠ ⊤
⊢ μ (s \ t) = μ (t \ s)

Tactic:
rw [← ENNReal.add_right_inj hfin, measure_inter_add_diff₀ _ ht, inter_comm,
  measure_inter_add_diff₀ _ hs, h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
/--
The composition of the isomorphism `pullbackSepcIso R S T` (from the pullback of
`Spec S ⟶ Spec R` and `Spec T ⟶ Spec R` to `Spec (S ⊗[R] T)`) with the morphism
`Spec (S ⊗[R] T) ⟶ Spec T` obtained by applying `Spec.map` to the ring morphism `t ↦ 1 ⊗ₜ[R] t`
is the second projection.
-/
@[reassoc (attr := simp)]
lemma pullbackSpecIso_hom_snd :
    (pullbackSpecIso R S T).hom ≫ Spec.map (ofHom (toRingHom includeRight)) = pullback.snd _ _

Proof state:
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
⊢ (pullbackSpecIso R S T).hom ≫ Spec.map (ofHom ↑includeRight) =
    pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T)))

Tactic:
rw [← pullbackSpecIso_inv_snd, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/FieldTheory/Normal/Defs.lean
theorem AlgEquiv.restrictNormal_trans [Normal F E] :
    (χ.trans ω).restrictNormal E = (χ.restrictNormal E).trans (ω.restrictNormal E) :=
  AlgEquiv.ext fun _ =>
    (algebraMap E K₃).injective
      (by simp only [AlgEquiv.trans_apply, AlgEquiv.restrictNormal_commutes])

Proof state:
F : Type u_1
inst✝¹⁵ : Field F
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝¹⁴ : Field K₁
inst✝¹³ : Field K₂
inst✝¹² : Field K₃
inst✝¹¹ : Algebra F K₁
inst✝¹⁰ : Algebra F K₂
inst✝⁹ : Algebra F K₃
χ : K₁ ≃ₐ[F] K₂
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra E K₁
inst✝⁵ : Algebra E K₂
inst✝⁴ : Algebra E K₃
inst✝³ : IsScalarTower F E K₁
inst✝² : IsScalarTower F E K₂
inst✝¹ : IsScalarTower F E K₃
inst✝ : Normal F E
x✝ : E
⊢ (algebraMap E K₃) (((χ.trans ω).restrictNormal E) x✝) =
    (algebraMap E K₃) (((χ.restrictNormal E).trans (ω.restrictNormal E)) x✝)

Tactic:
simp only [AlgEquiv.trans_apply, AlgEquiv.restrictNormal_commutes]

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

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

Tactic:
simp_rw [sdiff_le_iff, sup_le_iff, sdiff_le_iff]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Pointwise.lean
theorem smul_mem_pointwise_smul_iff {a : M} {S : Ideal R} {x : R} : a • x ∈ a • S ↔ x ∈ S :=
  ⟨fun h => by simpa using smul_mem_pointwise_smul a⁻¹ _ _ h, smul_mem_pointwise_smul _ _ _⟩

Proof state:
M : Type u_1
R : Type u_2
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x : R
h : a • x ∈ a • S
⊢ x ∈ S

Tactic:
simpa using smul_mem_pointwise_smul a⁻¹ _ _ h

Result:
no goals
-- Mathlib/Algebra/Ring/Prod.lean
theorem prod_unique (f : R →ₙ+* S × T) : ((fst S T).comp f).prod ((snd S T).comp f) = f :=
  ext fun x => by simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Proof state:
R : Type u_1
S : Type u_3
T : Type u_5
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring T
f : R →ₙ+* S × T
x : R
⊢ (((fst S T).comp f).prod ((snd S T).comp f)) x = f x

Tactic:
simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
lemma coe_variableChange_Δ' : ((W.variableChange C).Δ' : R) = C.u⁻¹ ^ 12 * W.Δ'

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ ↑(W.variableChange C).Δ' = ↑C.u⁻¹ ^ 12 * ↑W.Δ'

Tactic:
simp_rw [coe_Δ', variableChange_Δ]

Result:
no goals