harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivAt.clm_apply (hc : HasFDerivAt c c' x) (hu : HasFDerivAt u u' x) :
    HasFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
x : E
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
u : E → G
u' : E →L[𝕜] G
hc : HasFDerivAt c c' x
hu : HasFDerivAt u u' x
⊢ HasFDerivAt (fun y => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x

Tactic:
exact (isBoundedBilinearMap_apply.hasFDerivAt (c x, u x) :).comp x (hc.prod hu)

Result:
no goals
-- Mathlib/Logic/Function/Conjugate.lean
/-- If `f` semiconjugates `ga` to `gb` and `f'` is both a left and a right inverse of `f`,
then `f'` semiconjugates `gb` to `ga`. -/
lemma inverse_left {f' : β → α} (h : Semiconj f ga gb)
    (hf₁ : LeftInverse f' f) (hf₂ : RightInverse f' f) : Semiconj f' gb ga := fun x ↦ by
  rw [← hf₁.injective.eq_iff, h, hf₂, hf₂]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
f' : β → α
h : Semiconj f ga gb
hf₁ : LeftInverse f' f
hf₂ : RightInverse f' f
x : β
⊢ f' (gb x) = ga (f' x)

Tactic:
rw [← hf₁.injective.eq_iff, h, hf₂, hf₂]

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem ContinuousLinearMap.comp_cPolynomialOn {s : Set E} (g : F →L[𝕜] G)
    (h : CPolynomialOn 𝕜 f s) : CPolynomialOn 𝕜 (g ∘ f) s

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : CPolynomialOn 𝕜 f s
x : E
hx : x ∈ s
⊢ CPolynomialAt 𝕜 (⇑g ∘ f) x

Tactic:
rcases h x hx with ⟨p, n, r, hp⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : CPolynomialOn 𝕜 f s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
r : ℝ≥0∞
hp : HasFiniteFPowerSeriesOnBall f p x n r
⊢ CPolynomialAt 𝕜 (⇑g ∘ f) x

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : CPolynomialOn 𝕜 f s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
r : ℝ≥0∞
hp : HasFiniteFPowerSeriesOnBall f p x n r
⊢ CPolynomialAt 𝕜 (⇑g ∘ f) x

Tactic:
exact ⟨g.compFormalMultilinearSeries p, n, r, g.comp_hasFiniteFPowerSeriesOnBall hp⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : CPolynomialOn 𝕜 f s
⊢ CPolynomialOn 𝕜 (⇑g ∘ f) s

Tactic:
rintro x hx

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : CPolynomialOn 𝕜 f s
x : E
hx : x ∈ s
⊢ CPolynomialAt 𝕜 (⇑g ∘ f) x
-- Mathlib/SetTheory/Game/Basic.lean
theorem inv_eq_of_equiv_zero {x : PGame} (h : x ≈ 0) : x⁻¹ = 0

Proof state:
x : PGame
h : x ≈ 0
⊢ x⁻¹ = 0

Tactic:
exact if_pos h

Result:
no goals

Proof state:
x : PGame
h : x ≈ 0
⊢ x⁻¹ = 0

Tactic:
classical exact if_pos h

Result:
no goals
-- Mathlib/Data/Complex/FiniteDimensional.lean
theorem rank_real_complex'.{u} : Cardinal.lift.{u} (Module.rank ℝ ℂ) = 2

Proof state:
⊢ Cardinal.lift.{u, 0} (Module.rank ℝ ℂ) = 2

Tactic:
rw [← finrank_eq_rank, finrank_real_complex, Cardinal.lift_natCast, Nat.cast_ofNat]

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_apply_get_length (x : α) (xs : List α) :
    formPerm (x :: xs) ((x :: xs).get (Fin.mk xs.length (by simp))) = x :=
  formPerm_apply_getElem_length ..

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
⊢ xs.length < (x :: xs).length

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Prorepresentability.lean
/-- Equality of elements of `AutGalois F` can be checked on the projections on each pointed
Galois object. -/
lemma AutGalois.ext {f g : AutGalois F}
    (h : ∀ (A : PointedGaloisObject F), AutGalois.π F A f = AutGalois.π F A g) : f = g

Proof state:
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
f g : AutGalois F
h : ∀ (A : PointedGaloisObject F), (π F A) f = (π F A) g
⊢ f = g

Tactic:
ext A

Result:
case a.h
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
f g : AutGalois F
h : ∀ (A : PointedGaloisObject F), (π F A) f = (π F A) g
A : PointedGaloisObject F
⊢ ↑f A = ↑g A

Proof state:
case a.h
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
f g : AutGalois F
h : ∀ (A : PointedGaloisObject F), (π F A) f = (π F A) g
A : PointedGaloisObject F
⊢ ↑f A = ↑g A

Tactic:
exact h A

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Lemmas.lean
/-- If there is a multiplicative character of order `n` on `F`, then `#F ≡ 1 mod n`. -/
lemma orderOf_dvd_card_sub_one (χ : MulChar F R) : orderOf χ ∣ Fintype.card F - 1

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
⊢ orderOf χ ∣ Fintype.card F - 1

Tactic:
rw [← Fintype.card_units]

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
⊢ orderOf χ ∣ Fintype.card Fˣ

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
⊢ orderOf χ ∣ Fintype.card Fˣ

Tactic:
exact orderOf_dvd_of_pow_eq_one χ.pow_card_eq_one

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
⊢ orderOf χ ∣ Fintype.card F - 1

Tactic:
classical
rw [← Fintype.card_units]
exact orderOf_dvd_of_pow_eq_one χ.pow_card_eq_one

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem coeff_add_eq_right_of_lt (pn : p.natDegree < n) : (p + q).coeff n = q.coeff n

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p q : R[X]
pn : p.natDegree < n
⊢ (q + p).coeff n = q.coeff n

Tactic:
exact coeff_add_eq_left_of_lt pn

Result:
no goals

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p q : R[X]
pn : p.natDegree < n
⊢ (p + q).coeff n = q.coeff n

Tactic:
rw [add_comm]

Result:
R : Type u
n : ℕ
inst✝ : Semiring R
p q : R[X]
pn : p.natDegree < n
⊢ (q + p).coeff n = q.coeff n
-- Mathlib/Topology/Order/ScottTopology.lean
lemma dirSupClosed_iff_forall_sSup :
    DirSupClosed s ↔ ∀ ⦃d⦄, d.Nonempty → DirectedOn (· ≤ ·) d → d ⊆ s → sSup d ∈ s

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ DirSupClosed s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → d ⊆ s → sSup d ∈ s

Tactic:
simp [DirSupClosed, isLUB_iff_sSup_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insertMany_list_of_mem [LawfulBEq α] (h : m.1.WF)
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (m.insertMany l).1.get? k' = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ (m.insertMany l).val.get? k' = some (cast ⋯ v)

Tactic:
simp_to_model [insertMany] using List.getValueCast?_insertList_of_mem

Result:
no goals

Proof state:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'
-- Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
theorem isAddUnit_mul (hAB : A * B = 1) (i j k : n) (hij : i ≠ j) : IsAddUnit (A i k * B k j)

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
i j : n
hij : i ≠ j
⊢ ∀ (k : n), IsAddUnit (A i k * B k j)

Tactic:
rw [← IsAddUnit.sum_univ_iff, ← mul_apply, hAB, one_apply_ne hij]

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
i j : n
hij : i ≠ j
⊢ IsAddUnit 0

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
i j : n
hij : i ≠ j
⊢ IsAddUnit 0

Tactic:
exact isAddUnit_zero

Result:
no goals

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
i j k : n
hij : i ≠ j
⊢ IsAddUnit (A i k * B k j)

Tactic:
revert k

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
i j : n
hij : i ≠ j
⊢ ∀ (k : n), IsAddUnit (A i k * B k j)
-- Mathlib/RingTheory/Norm/Transitivity.lean
lemma det_mul_corner_pow :
    M.det * M k k ^ (Fintype.card m - 1) = M k k * (mulAuxMatBlock).det

Proof state:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ (M k k • 1).det * ((M * auxMat M k).toSquareBlock (fun x => x = k) False).det =
    M k k * ((M * auxMat M k).toSquareBlock (fun x => x = k) False).det

Tactic:
simp_rw [det_smul_of_tower, eq_iff_iff, iff_true, Fintype.card_unique,
  pow_one, det_one, smul_eq_mul, mul_one]

Result:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ M k k * ((M * auxMat M k).toSquareBlock (fun x => x = k) False).det =
    M k k * ((M * auxMat M k).toSquareBlock (fun x => x = k) False).det

Proof state:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ (M * auxMat M k).det = M k k * ((M * auxMat M k).toSquareBlock (fun x => x = k) False).det

Tactic:
rw [(mul_auxMat_blockTriangular M k).det_fintype, Fintype.prod_Prop, mul_auxMat_toSquareBlock_eq]

Result:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ (M k k • 1).det * ((M * auxMat M k).toSquareBlock (fun x => x = k) False).det =
    M k k * ((M * auxMat M k).toSquareBlock (fun x => x = k) False).det

Proof state:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ M.det * M k k ^ (Fintype.card m - 1) = (M * auxMat M k).det

Tactic:
simp [det_mul, (auxMat_blockTriangular M k).det_fintype,
  auxMat_toSquareBlock_ne, auxMat_toSquareBlock_eq]

Result:
no goals

Proof state:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ M k k * ((M * auxMat M k).toSquareBlock (fun x => x = k) False).det =
    M k k * ((M * auxMat M k).toSquareBlock (fun x => x = k) False).det

Tactic:
convert rfl

Result:
no goals

Proof state:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ M.det * M k k ^ (Fintype.card m - 1) = M k k * ((M * auxMat M k).toSquareBlock (fun x => x = k) False).det

Tactic:
trans (M * auxMat M k).det

Result:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ M.det * M k k ^ (Fintype.card m - 1) = (M * auxMat M k).det

S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ (M * auxMat M k).det = M k k * ((M * auxMat M k).toSquareBlock (fun x => x = k) False).det
-- Mathlib/Data/Finset/MulAntidiagonal.lean
theorem swap_mem_mulAntidiagonal :
    x.swap ∈ Finset.mulAntidiagonal hs ht a ↔ x ∈ Finset.mulAntidiagonal ht hs a

Proof state:
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
x : α × α
⊢ x.swap ∈ mulAntidiagonal hs ht a ↔ x ∈ mulAntidiagonal ht hs a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem take_range (m n : Nat) : take (range n) m = range (min m n)

Proof state:
m n : Nat
⊢ (range n).take m = range (min m n)

Tactic:
ext <;> simp

Result:
case h
m n i✝ : Nat
x✝ : i✝ < min m n
⊢ ((range n).extract 0 m)[i✝] = i✝

Proof state:
case h
m n i✝ : Nat
x✝ : i✝ < min m n
⊢ (range n)[0 + i✝] = i✝

Tactic:
simp

Result:
no goals

Proof state:
case h
m n i✝ : Nat
x✝ : i✝ < min m n
⊢ ((range n).extract 0 m)[i✝] = i✝

Tactic:
erw [getElem_extract]

Result:
case h
m n i✝ : Nat
x✝ : i✝ < min m n
⊢ (range n)[0 + i✝] = i✝
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem map_comp {f : α → β} {g : β → γ} (hf : UniformContinuous f) (hg : UniformContinuous g) :
    map g ∘ map f = map (g ∘ f) :=
  (map_unique (hg.comp hf) <| by simp only [Function.comp_def, map_mk, hf, hg]).symm

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
⊢ mk ∘ g ∘ f = (map g ∘ map f) ∘ mk

Tactic:
simp only [Function.comp_def, map_mk, hf, hg]

Result:
no goals
-- Mathlib/RingTheory/Ideal/IsPrincipal.lean
theorem associatesEquivIsPrincipal_mul (x y : Associates R) :
    (associatesEquivIsPrincipal R (x * y) : Ideal R) =
      (associatesEquivIsPrincipal R x) * (associatesEquivIsPrincipal R y)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x y : Associates R
⊢ ↑((associatesEquivIsPrincipal R) (x * y)) = ↑((associatesEquivIsPrincipal R) x) * ↑((associatesEquivIsPrincipal R) y)

Tactic:
rw [← quot_out x, ← quot_out y]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x y : Associates R
⊢ ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x) * Associates.mk (Quot.out y))) =
    ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x))) *
      ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out y)))

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
x y : Associates R
⊢ ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x) * Associates.mk (Quot.out y))) =
    ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out x))) *
      ↑((associatesEquivIsPrincipal R) (Associates.mk (Quot.out y)))

Tactic:
simp_rw [mk_mul_mk, associatesEquivIsPrincipal_apply, span_singleton_mul_span_singleton]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
protected lemma add_sub_assoc (hut : u ≤ t) : s + t - u = s + (t - u)

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
hut : u ≤ t
a : α
⊢ count a (s + t - u) = count a (s + (t - u))

Tactic:
simp [Nat.add_sub_assoc <| count_le_of_le _ hut]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
hut : u ≤ t
⊢ s + t - u = s + (t - u)

Tactic:
ext a

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
hut : u ≤ t
a : α
⊢ count a (s + t - u) = count a (s + (t - u))
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousOn.congr_mono (h : ContinuousOn f s) (h' : EqOn g f s₁) (h₁ : s₁ ⊆ s) :
    ContinuousOn g s₁

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
A : Tendsto f (𝓝[s₁] x) (𝓝 (f x))
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))

Tactic:
rw [← h' hx] at A

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
A : Tendsto f (𝓝[s₁] x) (𝓝 (g x))
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
⊢ ContinuousOn g s₁

Tactic:
intro x hx

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
⊢ ContinuousWithinAt g s₁ x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
A : ContinuousWithinAt f s₁ x
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))

Tactic:
unfold ContinuousWithinAt at A

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
A : Tendsto f (𝓝[s₁] x) (𝓝 (f x))
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
A : Tendsto f (𝓝[s₁] x) (𝓝 (g x))
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))

Tactic:
exact A.congr' h'.eventuallyEq_nhdsWithin.symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))

Tactic:
have A := (h x (h₁ hx)).mono h₁

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
A : ContinuousWithinAt f s₁ x
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
⊢ ContinuousWithinAt g s₁ x

Tactic:
unfold ContinuousWithinAt

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem mem_disjUnion (H : Disjoint π₁.iUnion π₂.iUnion) :
    J ∈ π₁.disjUnion π₂ H ↔ J ∈ π₁ ∨ J ∈ π₂

Proof state:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
H : Disjoint π₁.iUnion π₂.iUnion
⊢ J ∈ π₁.disjUnion π₂ H ↔ J ∈ π₁ ∨ J ∈ π₂

Tactic:
exact Finset.mem_union

Result:
no goals

Proof state:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
H : Disjoint π₁.iUnion π₂.iUnion
⊢ J ∈ π₁.disjUnion π₂ H ↔ J ∈ π₁ ∨ J ∈ π₂

Tactic:
classical exact Finset.mem_union

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Comp.lean
theorem fderivWithin_comp_of_eq' {g : F → G} {t : Set F} {y : F}
    (hg : DifferentiableWithinAt 𝕜 g t y) (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t)
    (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) :
    fderivWithin 𝕜 (fun y ↦ g (f y)) s x
      = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s 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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
x : E
s : Set E
g : F → G
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ fderivWithin 𝕜 (fun y => g (f y)) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)

Tactic:
exact fderivWithin_comp _ hg hf h hxs

Result:
no goals

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
x : E
s : Set E
g : F → G
t : Set F
y : F
hg : DifferentiableWithinAt 𝕜 g t y
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hy : f x = y
⊢ fderivWithin 𝕜 (fun y => g (f y)) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)

Tactic:
subst hy

Result:
𝕜 : 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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
x : E
s : Set E
g : F → G
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ fderivWithin 𝕜 (fun y => g (f y)) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem restrict_sInf_eq_sInf_restrict (m : Set (OuterMeasure α)) {s : Set α} (hm : m.Nonempty) :
    restrict s (sInf m) = sInf (restrict s '' m)

Proof state:
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
hm : m.Nonempty
⊢ (restrict s) (sInf m) = sInf (⇑(restrict s) '' m)

Tactic:
simp only [sInf_eq_iInf, restrict_biInf, hm, iInf_image]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
theorem isSheaf_coherent_iff_regular_and_extensive [Preregular C] [FinitaryPreExtensive C] :
    IsSheaf (coherentTopology C) F ↔
    IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
⊢ IsSheaf (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) F ↔
    IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F

Tactic:
exact isSheaf_sup (extensiveCoverage C) (regularCoverage C) F

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
⊢ IsSheaf (coherentTopology C) F ↔ IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F

Tactic:
rw [← extensive_regular_generate_coherent]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
⊢ IsSheaf (Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)) F ↔
    IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F