harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/HNNExtension.lean
theorem inv_t_mul_of (b : B) :
    t⁻¹ * (of (b : G) : HNNExtension G A B φ) = of (φ.symm b : G) * t⁻¹

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ t⁻¹ * of ↑b = of ↑(φ.symm b) * t⁻¹

Tactic:
rw [equiv_symm_eq_conj]

Result:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ t⁻¹ * of ↑b = t⁻¹ * of ↑b * t * t⁻¹

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
b : ↥B
⊢ t⁻¹ * of ↑b = t⁻¹ * of ↑b * t * t⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem Raw.buckets_empty {c} {i : Nat} {h} :
    (Raw.empty c : Raw α β).buckets[i]'h = AssocList.nil

Proof state:
α : Type u
β : α → Type v
c i : Nat
h : i < (Raw.empty c).buckets.size
⊢ (Raw.empty c).buckets[i] = AssocList.nil

Tactic:
simp [Raw.empty]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
theorem square_from_iso_invert {X Y : T} (i : X ≅ Y) (p : Arrow T) (sq : Arrow.mk i.hom ⟶ p) :
    i.inv ≫ sq.left ≫ p.hom = sq.right

Proof state:
T : Type u
inst✝ : Category.{v, u} T
X Y : T
i : X ≅ Y
p : Arrow T
sq : mk i.hom ⟶ p
⊢ i.inv ≫ sq.left ≫ p.hom = sq.right

Tactic:
simp only [Iso.inv_hom_id_assoc, Arrow.w, Arrow.mk_hom]

Result:
no goals
-- Mathlib/Order/Filter/CountableInter.lean
theorem eventually_countable_forall [Countable ι] {p : α → ι → Prop} :
    (∀ᶠ x in l, ∀ i, p x i) ↔ ∀ i, ∀ᶠ x in l, p x i

Proof state:
ι : Sort u_1
α : Type u_2
l : Filter α
inst✝¹ : CountableInterFilter l
inst✝ : Countable ι
p : α → ι → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i

Tactic:
simpa only [Filter.Eventually, setOf_forall] using
  @countable_iInter_mem _ _ l _ _ fun i => { x | p x i }

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_div' (x) {y : ℝ} (hy : 0 ≤ y) : √(x / y) = √x / √y

Proof state:
x y : ℝ
hy : 0 ≤ y
⊢ √(x / y) = √x / √y

Tactic:
rw [division_def, sqrt_mul' x (inv_nonneg.2 hy), sqrt_inv, division_def]

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
lemma singleton_eq_univ [Subsingleton α] (a : α) : ({a} : Finset α) = univ

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Subsingleton α
a : α
⊢ {a} = univ

Tactic:
ext b

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Subsingleton α
a b : α
⊢ b ∈ {a} ↔ b ∈ univ

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Subsingleton α
a b : α
⊢ b ∈ {a} ↔ b ∈ univ

Tactic:
simp [Subsingleton.elim a b]

Result:
no goals
-- Mathlib/Condensed/Epi.lean
lemma epi_iff_surjective_on_stonean : Epi f ↔
    ∀ (S : Stonean), Function.Surjective (f.val.app (op S.compHaus))

Proof state:
A : Type u'
inst✝⁹ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁸ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁷ : ConcreteCategory A FA
inst✝⁶ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁵ : PreservesFiniteProducts (CategoryTheory.forget A)
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝³ : (extensiveTopology Stonean).WEqualsLocallyBijective A
inst✝² : HasSheafify (extensiveTopology Stonean) A
inst✝¹ : (extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)
inst✝ : Balanced (Sheaf (extensiveTopology Stonean) A)
⊢ IsLocallySurjective
      (Presheaf.coherentExtensiveEquivalence.functor.map ((StoneanCompHaus.equivalence A).inverse.map f)) ↔
    ∀ (S : Stonean), Function.Surjective ⇑(hom (f.val.app (op S.compHaus)))

Tactic:
exact extensiveTopology.isLocallySurjective_iff (D := A) _

Result:
no goals

Proof state:
A : Type u'
inst✝⁹ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁸ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁷ : ConcreteCategory A FA
inst✝⁶ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁵ : PreservesFiniteProducts (CategoryTheory.forget A)
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝³ : (extensiveTopology Stonean).WEqualsLocallyBijective A
inst✝² : HasSheafify (extensiveTopology Stonean) A
inst✝¹ : (extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)
inst✝ : Balanced (Sheaf (extensiveTopology Stonean) A)
⊢ Epi f ↔ ∀ (S : Stonean), Function.Surjective ⇑(hom (f.val.app (op S.compHaus)))

Tactic:
rw [← (StoneanCompHaus.equivalence A).inverse.epi_map_iff_epi,
  ← Presheaf.coherentExtensiveEquivalence.functor.epi_map_iff_epi,
  ← isLocallySurjective_iff_epi']

Result:
A : Type u'
inst✝⁹ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type v'
inst✝⁸ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁷ : ConcreteCategory A FA
inst✝⁶ : HasFunctorialSurjectiveInjectiveFactorization A
X Y : Condensed A
f : X ⟶ Y
inst✝⁵ : PreservesFiniteProducts (CategoryTheory.forget A)
inst✝⁴ : ∀ (X : CompHausᵒᵖ), HasLimitsOfShape (StructuredArrow X Stonean.toCompHaus.op) A
inst✝³ : (extensiveTopology Stonean).WEqualsLocallyBijective A
inst✝² : HasSheafify (extensiveTopology Stonean) A
inst✝¹ : (extensiveTopology Stonean).HasSheafCompose (CategoryTheory.forget A)
inst✝ : Balanced (Sheaf (extensiveTopology Stonean) A)
⊢ IsLocallySurjective
      (Presheaf.coherentExtensiveEquivalence.functor.map ((StoneanCompHaus.equivalence A).inverse.map f)) ↔
    ∀ (S : Stonean), Function.Surjective ⇑(hom (f.val.app (op S.compHaus)))
-- Mathlib/Topology/Basic.lean
theorem isClosed_of_closure_subset (h : closure s ⊆ s) : IsClosed s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : closure s ⊆ s
⊢ IsClosed s

Tactic:
rw [subset_closure.antisymm h]

Result:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : closure s ⊆ s
⊢ IsClosed (closure s)

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : closure s ⊆ s
⊢ IsClosed (closure s)

Tactic:
exact isClosed_closure

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
lemma subset_span {s : Set R} : s ⊆ (span s : Set R)

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
hx : x ∈ s
⊢ (span s).ringCon x 0

Tactic:
exact RingConGen.Rel.of _ _ (by simpa using hx)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
⊢ s ⊆ ↑(span s)

Tactic:
intro x hx

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
hx : x ∈ s
⊢ x ∈ ↑(span s)

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
hx : x ∈ s
⊢ x - 0 ∈ s

Tactic:
simpa using hx

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
hx : x ∈ s
⊢ x ∈ ↑(span s)

Tactic:
rw [SetLike.mem_coe, mem_iff]

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
hx : x ∈ s
⊢ (span s).ringCon x 0
-- Mathlib/Data/Finset/NatAntidiagonal.lean
lemma antidiagonal_eq_image' (n : ℕ) :
    antidiagonal n = (range (n + 1)).image fun i ↦ (n - i, i)

Proof state:
n : ℕ
⊢ antidiagonal n = image (fun i => (n - i, i)) (range (n + 1))

Tactic:
simp only [antidiagonal_eq_map', map_eq_image, Function.Embedding.coeFn_mk]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
protected lemma IsOfFinOrder.eq_one (ha₀ : 0 ≤ a) (ha : IsOfFinOrder a) : a = 1

Proof state:
case intro.intro
G : Type u_1
inst✝ : LinearOrderedSemiring G
a : G
ha₀ : 0 ≤ a
ha✝ : IsOfFinOrder a
n : ℕ
hn : 0 < n
ha : a ^ n = 1
⊢ a = 1

Tactic:
exact (pow_eq_one_iff_of_nonneg ha₀ hn.ne').1 ha

Result:
no goals

Proof state:
G : Type u_1
inst✝ : LinearOrderedSemiring G
a : G
ha₀ : 0 ≤ a
ha : IsOfFinOrder a
⊢ a = 1

Tactic:
obtain ⟨n, hn, ha⟩ := ha.exists_pow_eq_one

Result:
case intro.intro
G : Type u_1
inst✝ : LinearOrderedSemiring G
a : G
ha₀ : 0 ≤ a
ha✝ : IsOfFinOrder a
n : ℕ
hn : 0 < n
ha : a ^ n = 1
⊢ a = 1
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma p_descOpcycles {A : C} (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j)
    (hk : K.d j i ≫ k = 0) : K.pOpcycles i ≫ K.descOpcycles k j hj hk = k

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
hk : K.d j i ≫ k = 0
⊢ K.pOpcycles i ≫ K.descOpcycles k j hj hk = k

Tactic:
dsimp [descOpcycles, pOpcycles]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
hk : K.d j i ≫ k = 0
⊢ (K.sc i).pOpcycles ≫ (K.sc i).descOpcycles k ⋯ = k

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
hk : K.d j i ≫ k = 0
⊢ (K.sc i).pOpcycles ≫ (K.sc i).descOpcycles k ⋯ = k

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem snd_lt_of_mem_zipIdx {x : α × Nat} {l : Array α} {k : Nat} (h : x ∈ l.zipIdx k) : x.2 < l.size + k

Proof state:
α : Type u_1
x : α × Nat
l : Array α
k : Nat
h : x ∈ l.zipIdx k
⊢ x.snd < l.size + k

Tactic:
simpa [Nat.add_comm] using snd_lt_add_of_mem_zipIdx h

Result:
no goals
-- Mathlib/Algebra/FreeMonoid/Count.lean
theorem count_of [DecidableEq α] (x y : α) :
    count x (of y) = Pi.mulSingle (f := fun _ => Multiplicative ℕ) x (Multiplicative.ofAdd 1) y :=
  by simp only [count, eq_comm, countP_of, ofAdd_zero, Pi.mulSingle_apply]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (count x) (of y) = Pi.mulSingle x (Multiplicative.ofAdd 1) y

Tactic:
simp only [count, eq_comm, countP_of, ofAdd_zero, Pi.mulSingle_apply]

Result:
no goals
-- Mathlib/Data/Multiset/Fintype.lean
@[simp] lemma coe_mem {x : m} : ↑x ∈ m := Multiset.count_pos.mp (by have := x.2.2; omega)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x : m.ToType
this : ↑x.snd < count x.fst m
⊢ 0 < count x.fst m

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x : m.ToType
⊢ 0 < count x.fst m

Tactic:
have := x.2.2

Result:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
x : m.ToType
this : ↑x.snd < count x.fst m
⊢ 0 < count x.fst m
-- Mathlib/Probability/Independence/Basic.lean
lemma iIndepFun_iff_iIndep {β : ι → Type*}
    (m : ∀ x : ι, MeasurableSpace (β x)) (f : ∀ x : ι, Ω → β x) (μ : Measure Ω) :
    iIndepFun m f μ ↔ iIndep (fun x ↦ (m x).comap (f x)) μ

Proof state:
Ω : Type u_1
ι : Type u_2
x✝ : MeasurableSpace Ω
β : ι → Type u_6
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
μ : Measure Ω
⊢ iIndepFun m f μ ↔ iIndep (fun x => MeasurableSpace.comap (f x) (m x)) μ

Tactic:
simp only [iIndepFun, iIndep, Kernel.iIndepFun]

Result:
no goals
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
lemma apply_natAbs_eq (x : ℤ) : abv (natAbs x) = abv x

Proof state:
R : Type u_3
S : Type u_4
inst✝² : OrderedCommRing S
inst✝¹ : Ring R
abv : AbsoluteValue R S
inst✝ : NoZeroDivisors S
x : ℤ
⊢ abv ↑x.natAbs = abv ↑x

Tactic:
obtain ⟨_, rfl | rfl⟩ := eq_nat_or_neg x <;> simp

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
lemma wInner_smul_left {𝕝 : Type*} [CommSemiring 𝕝] [StarRing 𝕝] [Algebra 𝕝 𝕜] [StarModule 𝕝 𝕜]
    [SMulCommClass ℝ 𝕝 𝕜] [∀ i, Module 𝕝 (E i)] [∀ i, IsScalarTower 𝕝 𝕜 (E i)] (c : 𝕝)
    (w : ι → ℝ) (f g : ∀ i, E i) : ⟪c • f, g⟫_[𝕜, w] = star c • ⟪f, g⟫_[𝕜, w]

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝¹⁰ : Fintype ι
inst✝⁹ : RCLike 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → InnerProductSpace 𝕜 (E i)
𝕝 : Type u_5
inst✝⁶ : CommSemiring 𝕝
inst✝⁵ : StarRing 𝕝
inst✝⁴ : Algebra 𝕝 𝕜
inst✝³ : StarModule 𝕝 𝕜
inst✝² : SMulCommClass ℝ 𝕝 𝕜
inst✝¹ : (i : ι) → Module 𝕝 (E i)
inst✝ : ∀ (i : ι), IsScalarTower 𝕝 𝕜 (E i)
c : 𝕝
w : ι → ℝ
f g : (i : ι) → E i
⊢ wInner w (c • f) g = star c • wInner w f g

Tactic:
simp_rw [wInner, Pi.smul_apply, inner_smul_left_eq_star_smul, starRingEnd_apply, smul_sum,
  smul_comm (w _)]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem rightInvSeq_reverse (ω : List B) :
    ris (ω.reverse) = (lis ω).reverse

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
⊢ cs.rightInvSeq ω.reverse = (cs.leftInvSeq ω).reverse

Tactic:
simp [leftInvSeq_eq_reverse_rightInvSeq_reverse]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
@[simp] lemma rpow_rpow_inv (hx : 0 ≤ x) (hy : y ≠ 0) : (x ^ y) ^ y⁻¹ = x

Proof state:
x y : ℝ
hx : 0 ≤ x
hy : y ≠ 0
⊢ (x ^ y) ^ y⁻¹ = x

Tactic:
rw [← rpow_mul hx, mul_inv_cancel₀ hy, rpow_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_congr {as bs : Array α} (h : as = bs)
    {f : α → Option β} {g : α → Option β} (h' : f = g) {start stop start' stop' : Nat}
    (h₁ : start = start') (h₂ : stop = stop') :
    filterMap f as start stop = filterMap g bs start' stop'

Proof state:
α : Type u_1
β : Type u_2
as bs : Array α
h : as = bs
f g : α → Option β
h' : f = g
start stop start' stop' : Nat
h₁ : start = start'
h₂ : stop = stop'
⊢ filterMap f as start stop = filterMap g bs start' stop'

Tactic:
congr

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem lmapDomain_linearCombination (f : α → α') (g : M →ₗ[R] M') (h : ∀ i, g (v i) = v' (f i)) :
    (linearCombination R v').comp (lmapDomain R R f) = g.comp (linearCombination R v)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v : α → M
v' : α' → M'
f : α → α'
g : M →ₗ[R] M'
h : ∀ (i : α), g (v i) = v' (f i)
⊢ linearCombination R v' ∘ₗ lmapDomain R R f = g ∘ₗ linearCombination R v

Tactic:
ext l

Result:
case h.h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v : α → M
v' : α' → M'
f : α → α'
g : M →ₗ[R] M'
h : ∀ (i : α), g (v i) = v' (f i)
l : α
⊢ ((linearCombination R v' ∘ₗ lmapDomain R R f) ∘ₗ lsingle l) 1 = ((g ∘ₗ linearCombination R v) ∘ₗ lsingle l) 1

Proof state:
case h.h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v : α → M
v' : α' → M'
f : α → α'
g : M →ₗ[R] M'
h : ∀ (i : α), g (v i) = v' (f i)
l : α
⊢ ((linearCombination R v' ∘ₗ lmapDomain R R f) ∘ₗ lsingle l) 1 = ((g ∘ₗ linearCombination R v) ∘ₗ lsingle l) 1

Tactic:
simp [linearCombination_apply, Finsupp.sum_mapDomain_index, add_smul, h]

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
theorem _root_.ContDiff.contDiffBump {c g : X → E} {f : ∀ x, ContDiffBump (c x)}
    (hc : ContDiff ℝ n c) (hr : ContDiff ℝ n fun x => (f x).rIn)
    (hR : ContDiff ℝ n fun x => (f x).rOut) (hg : ContDiff ℝ n g) :
    ContDiff ℝ n fun x => f x (g x)

Proof state:
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
hc : ContDiff ℝ (↑n) c
hr : ContDiff ℝ ↑n fun x => (f x).rIn
hR : ContDiff ℝ ↑n fun x => (f x).rOut
hg : ContDiff ℝ (↑n) g
⊢ ContDiff ℝ ↑n fun x => ↑(f x) (g x)

Tactic:
rw [contDiff_iff_contDiffAt] at *

Result:
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
hc : ∀ (x : X), ContDiffAt ℝ (↑n) c x
hr : ∀ (x : X), ContDiffAt ℝ (↑n) (fun x => (f x).rIn) x
hR : ∀ (x : X), ContDiffAt ℝ (↑n) (fun x => (f x).rOut) x
hg : ∀ (x : X), ContDiffAt ℝ (↑n) g x
⊢ ∀ (x : X), ContDiffAt ℝ (↑n) (fun x => ↑(f x) (g x)) x

Proof state:
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
hc : ∀ (x : X), ContDiffAt ℝ (↑n) c x
hr : ∀ (x : X), ContDiffAt ℝ (↑n) (fun x => (f x).rIn) x
hR : ∀ (x : X), ContDiffAt ℝ (↑n) (fun x => (f x).rOut) x
hg : ∀ (x : X), ContDiffAt ℝ (↑n) g x
⊢ ∀ (x : X), ContDiffAt ℝ (↑n) (fun x => ↑(f x) (g x)) x

Tactic:
exact fun x => (hc x).contDiffBump (hr x) (hR x) (hg x)

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem inv_mul_eq_div : a⁻¹ * b = b / a

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
⊢ a⁻¹ * b = b / a

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Compare.lean
theorem swap_eq_iff_eq_swap {o o' : Ordering} : o.swap = o' ↔ o = o'.swap

Proof state:
o o' : Ordering
⊢ o.swap = o' ↔ o = o'.swap

Tactic:
rw [← swap_inj, swap_swap]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem set_support_mul_subset : { x | (p * q) x ≠ x } ⊆ { x | p x ≠ x } ∪ { x | q x ≠ x }

Proof state:
α : Type u_1
p q : Perm α
x : α
⊢ ¬p (q x) = x → ¬p x = x ∨ ¬q x = x

Tactic:
by_cases hq : q x = x <;> simp [hq]

Result:
no goals

Proof state:
α : Type u_1
p q : Perm α
x : α
⊢ x ∈ {x | (p * q) x ≠ x} → x ∈ {x | p x ≠ x} ∪ {x | q x ≠ x}

Tactic:
simp only [Perm.coe_mul, Function.comp_apply, Ne, Set.mem_union, Set.mem_setOf_eq]

Result:
α : Type u_1
p q : Perm α
x : α
⊢ ¬p (q x) = x → ¬p x = x ∨ ¬q x = x

Proof state:
α : Type u_1
p q : Perm α
⊢ {x | (p * q) x ≠ x} ⊆ {x | p x ≠ x} ∪ {x | q x ≠ x}

Tactic:
intro x

Result:
α : Type u_1
p q : Perm α
x : α
⊢ x ∈ {x | (p * q) x ≠ x} → x ∈ {x | p x ≠ x} ∪ {x | q x ≠ x}
-- Mathlib/Algebra/Lie/Nilpotent.lean
@[simp] lemma iInf_lowerCentralSeries_eq_bot_of_isNilpotent [IsNilpotent L M] :
    ⨅ k, lowerCentralSeries R L M k = ⊥

Proof state:
case intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ ⨅ k, lowerCentralSeries R L M k = ⊥

Tactic:
rw [eq_bot_iff, ← hk]

Result:
case intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ ⨅ k, lowerCentralSeries R L M k ≤ lowerCentralSeries R L M k

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
⊢ ⨅ k, lowerCentralSeries R L M k = ⊥

Tactic:
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R L M

Result:
case intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ ⨅ k, lowerCentralSeries R L M k = ⊥

Proof state:
case intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNilpotent L M
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ ⨅ k, lowerCentralSeries R L M k ≤ lowerCentralSeries R L M k

Tactic:
exact iInf_le _ _

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem leadingCoeff_of_b_ne_zero (ha : P.a = 0) (hb : P.b ≠ 0) : P.toPoly.leadingCoeff = P.b

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b ≠ 0
⊢ P.toPoly.leadingCoeff = P.b

Tactic:
rw [of_a_eq_zero ha, leadingCoeff_quadratic hb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem forall_mem_mkVector {p : α → Prop} {a : α} {n} :
    (∀ b, b ∈ mkVector n a → p b) ↔ n = 0 ∨ p a

Proof state:
α : Type u_1
p : α → Prop
a : α
n : Nat
⊢ (∀ (b : α), b ∈ mkVector n a → p b) ↔ n = 0 ∨ p a

Tactic:
cases n <;> simp [mem_mkVector]

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem mem_support_onFinset {s : Finset α} {f : α → M} (hf : ∀ a : α, f a ≠ 0 → a ∈ s) {a : α} :
    a ∈ (Finsupp.onFinset s f hf).support ↔ f a ≠ 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
s : Finset α
f : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
a : α
⊢ a ∈ (onFinset s f hf).support ↔ f a ≠ 0

Tactic:
rw [Finsupp.mem_support_iff, Finsupp.onFinset_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem partialProd_succ' (f : Fin (n + 1) → α) (j : Fin (n + 1)) :
    partialProd f j.succ = f 0 * partialProd (Fin.tail f) j

Proof state:
α : Type u_1
inst✝ : Monoid α
n : ℕ
f : Fin (n + 1) → α
j : Fin (n + 1)
⊢ partialProd f j.succ = f 0 * partialProd (tail f) j

Tactic:
simp [partialProd]

Result:
α : Type u_1
inst✝ : Monoid α
n : ℕ
f : Fin (n + 1) → α
j : Fin (n + 1)
⊢ f 0 * (List.take (↑j) (List.ofFn fun i => f i.succ)).prod = f 0 * (List.take (↑j) (List.ofFn (tail f))).prod

Proof state:
α : Type u_1
inst✝ : Monoid α
n : ℕ
f : Fin (n + 1) → α
j : Fin (n + 1)
⊢ f 0 * (List.take (↑j) (List.ofFn fun i => f i.succ)).prod = f 0 * (List.take (↑j) (List.ofFn (tail f))).prod

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Image.lean
lemma image_le_iff (G : Subpresheaf F) (f : F ⟶ F') (G' : Subpresheaf F') :
    G.image f ≤ G' ↔ G ≤ G'.preimage f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
f : F ⟶ F'
G' : Subpresheaf F'
⊢ G.image f ≤ G' ↔ G ≤ G'.preimage f

Tactic:
simp [Subpresheaf.le_def]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma zero_le_ofNat (n : ℕ) : 0 ≤ ofNat n := @le.intro _ _ n (by rw [Int.zero_add]; rfl)

Proof state:
n : ℕ
⊢ ↑n = ofNat n

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ 0 + ↑n = ofNat n

Tactic:
rw [Int.zero_add]

Result:
n : ℕ
⊢ ↑n = ofNat n
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem of_toQuadraticForm' [DecidableEq n] {M : Matrix n n ℝ} (hM : M.IsSymm)
    (hMq : M.toQuadraticMap'.PosDef) : M.PosDef

Proof state:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.IsSymm
hMq : M.toQuadraticMap'.PosDef
⊢ M.PosDef

Tactic:
refine ⟨hM, fun x hx => ?_⟩

Result:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.IsSymm
hMq : M.toQuadraticMap'.PosDef
x : n → ℝ
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ M *ᵥ x

Proof state:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.IsSymm
x : n → ℝ
hx : x ≠ 0
hMq : ∀ (x : n → ℝ), x ≠ 0 → 0 < x ⬝ᵥ M *ᵥ x
⊢ 0 < star x ⬝ᵥ M *ᵥ x

Tactic:
apply hMq x hx

Result:
no goals

Proof state:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.IsSymm
hMq : M.toQuadraticMap'.PosDef
x : n → ℝ
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ M *ᵥ x

Tactic:
simp only [toQuadraticMap', QuadraticMap.PosDef, LinearMap.BilinMap.toQuadraticMap_apply,
  toLinearMap₂'_apply'] at hMq

Result:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.IsSymm
x : n → ℝ
hx : x ≠ 0
hMq : ∀ (x : n → ℝ), x ≠ 0 → 0 < x ⬝ᵥ M *ᵥ x
⊢ 0 < star x ⬝ᵥ M *ᵥ x
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
@[simp]
lemma equiv_mk (L : C ⥤ D) [L.IsLocalization W] {X Y : C}
    [HasSmallLocalizedHom.{w} W X Y] (f : X ⟶ Y) :
    equiv.{w} W L (mk W f) = L.map f

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
inst✝ : HasSmallLocalizedHom W X Y
f : X ⟶ Y
⊢ (equiv W L) (mk W f) = L.map f

Tactic:
simp [equiv, mk]

Result:
no goals
-- Mathlib/Data/Int/Interval.lean
theorem card_fintype_Icc_of_le (h : a ≤ b + 1) : (Fintype.card (Set.Icc a b) : ℤ) = b + 1 - a

Proof state:
a b : ℤ
h : a ≤ b + 1
⊢ ↑(Fintype.card ↑(Set.Icc a b)) = b + 1 - a

Tactic:
rw [card_fintype_Icc, toNat_sub_of_le h]

Result:
no goals