harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_sub_of_nonempty (hs : s.Nonempty) (ht : t.Nonempty) :
    IsVonNBounded 𝕜 (s - t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : IsTopologicalAddGroup E
s t : Set E
hs : s.Nonempty
ht : t.Nonempty
⊢ IsVonNBounded 𝕜 (s - t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Tactic:
simp [sub_eq_add_neg, isVonNBounded_add_of_nonempty, hs, ht]

Result:
no goals
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fib_add_two_sub_fib_add_one {n : ℕ} : fib (n + 2) - fib (n + 1) = fib n

Proof state:
n : ℕ
⊢ fib (n + 2) - fib (n + 1) = fib n

Tactic:
rw [fib_add_two, add_tsub_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem Monic.ne_zero {R : Type*} [Semiring R] [Nontrivial R] {p : R[X]} (hp : p.Monic) :
    p ≠ 0

Proof state:
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p.Monic
⊢ p ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hp : Monic 0
⊢ False

Proof state:
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
hp : Monic 0
⊢ False

Tactic:
simp [Monic] at hp

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem IsUniformInducing.uniformEquicontinuousOn_iff {F : ι → β → α} {S : Set β} {u : α → γ}
    (hu : IsUniformInducing u) :
    UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((u ∘ ·) ∘ F) S

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
S : Set β
u : α → γ
hu : IsUniformInducing u
this : IsUniformInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ UniformContinuousOn ((⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun) ∘ ⇑ofFun ∘ swap F) S ↔
    UniformContinuousOn (⇑ofFun ∘ swap ((fun x => u ∘ x) ∘ F)) S

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
S : Set β
u : α → γ
hu : IsUniformInducing u
this : IsUniformInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((fun x => u ∘ x) ∘ F) S

Tactic:
simp only [uniformEquicontinuousOn_iff_uniformContinuousOn, this.uniformContinuousOn_iff]

Result:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
S : Set β
u : α → γ
hu : IsUniformInducing u
this : IsUniformInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ UniformContinuousOn ((⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun) ∘ ⇑ofFun ∘ swap F) S ↔
    UniformContinuousOn (⇑ofFun ∘ swap ((fun x => u ∘ x) ∘ F)) S

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
S : Set β
u : α → γ
hu : IsUniformInducing u
⊢ UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((fun x => u ∘ x) ∘ F) S

Tactic:
have := UniformFun.postcomp_isUniformInducing (α := ι) hu

Result:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
S : Set β
u : α → γ
hu : IsUniformInducing u
this : IsUniformInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((fun x => u ∘ x) ∘ F) S
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem smul_closedBall'' : a • closedBall b r = closedBall (a • b) r

Proof state:
case h
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
x✝ : E
⊢ x✝ ∈ a • closedBall b r ↔ x✝ ∈ closedBall (a • b) r

Tactic:
simp [mem_closedBall, Set.mem_smul_set, dist_eq_norm_div, div_eq_inv_mul, ←
  eq_inv_mul_iff_mul_eq, mul_assoc]

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a • closedBall b r = closedBall (a • b) r

Tactic:
ext

Result:
case h
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
x✝ : E
⊢ x✝ ∈ a • closedBall b r ↔ x✝ ∈ closedBall (a • b) r
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- The `n`-smooth numbers agree with the `primesBelow n`-factored numbers. -/
lemma smmoothNumbers_eq_factoredNumbers_primesBelow (n : ℕ) :
    smoothNumbers n = factoredNumbers n.primesBelow

Proof state:
n m : ℕ
hm : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ Finset.range n
⊢ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ n.primesBelow

Tactic:
exact fun p hp hp' ↦ mem_primesBelow.mpr ⟨Finset.mem_range.mp <| hm p hp hp', hp⟩

Result:
no goals

Proof state:
n : ℕ
⊢ factoredNumbers (Finset.range n) = factoredNumbers n.primesBelow

Tactic:
refine Set.Subset.antisymm (fun m hm ↦ ?_) <| factoredNumbers_mono Finset.mem_of_mem_filter

Result:
n m : ℕ
hm : m ∈ factoredNumbers (Finset.range n)
⊢ m ∈ factoredNumbers n.primesBelow

Proof state:
n m : ℕ
hm : m ∈ factoredNumbers (Finset.range n)
⊢ m ∈ factoredNumbers n.primesBelow

Tactic:
simp_rw [mem_factoredNumbers'] at hm ⊢

Result:
n m : ℕ
hm : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ Finset.range n
⊢ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ n.primesBelow

Proof state:
n : ℕ
⊢ n.smoothNumbers = factoredNumbers n.primesBelow

Tactic:
rw [smoothNumbers_eq_factoredNumbers]

Result:
n : ℕ
⊢ factoredNumbers (Finset.range n) = factoredNumbers n.primesBelow
-- Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean
lemma shiftShortComplexFunctorIso_zero_add_hom_app (a : ℤ) (K : CochainComplex C ℤ) :
    (shiftShortComplexFunctorIso C 0 a a (zero_add a)).hom.app K =
      (shortComplexFunctor C (ComplexShape.up ℤ) a).map
        ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
a : ℤ
K : CochainComplex C ℤ
⊢ (shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K =
    (shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)

Tactic:
ext <;> dsimp <;> simp [one_smul, shiftFunctorZero_hom_app_f]

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
lemma dens_image [Fintype β] [DecidableEq β] {f : α → β} (hf : Bijective f) (s : Finset α) :
    (s.image f).dens = s.dens

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : DecidableEq β
f : α → β
hf : Bijective f
s : Finset α
⊢ (image f s).dens = s.dens

Tactic:
simpa [map_eq_image, -dens_map_equiv] using dens_map_equiv (.ofBijective f hf)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
theorem log_mul_self_monotoneOn : MonotoneOn (fun x : ℝ => log x * x) { x | 1 ≤ x }

Proof state:
x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
⊢ log x * x ≤ log y * y

Tactic:
have y_pos : 0 < y := lt_of_lt_of_le zero_lt_one hey

Result:
x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
y_pos : 0 < y
⊢ log x * x ≤ log y * y

Proof state:
x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
y_pos : 0 < y
⊢ log x * x ≤ log y * y

Tactic:
gcongr

Result:
case b0
x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
y_pos : 0 < y
⊢ 0 ≤ log y

Proof state:
case b0
x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
y_pos : 0 < y
⊢ 0 ≤ log y

Tactic:
rwa [le_log_iff_exp_le y_pos, Real.exp_zero]

Result:
no goals

Proof state:
⊢ MonotoneOn (fun x => log x * x) {x | 1 ≤ x}

Tactic:
simp only [MonotoneOn, mem_setOf_eq]

Result:
⊢ ∀ ⦃a : ℝ⦄, 1 ≤ a → ∀ ⦃b : ℝ⦄, 1 ≤ b → a ≤ b → log a * a ≤ log b * b

Proof state:
⊢ ∀ ⦃a : ℝ⦄, 1 ≤ a → ∀ ⦃b : ℝ⦄, 1 ≤ b → a ≤ b → log a * a ≤ log b * b

Tactic:
intro x hex y hey hxy

Result:
x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
⊢ log x * x ≤ log y * y
-- Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean
theorem mem_basis_iff {f : MvPowerSeries σ R} {Jd : TwoSidedIdeal R × (σ →₀ ℕ)} :
    f ∈ basis σ R Jd ↔ ∀ e ≤ Jd.2, coeff R e f ∈ Jd.1

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
f : MvPowerSeries σ R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
⊢ f ∈ basis σ R Jd ↔ ∀ e ≤ Jd.2, (coeff R e) f ∈ Jd.1

Tactic:
simp [basis]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem isBounded_Icc [Finite ι] (I : Box ι) : Bornology.IsBounded (Box.Icc I)

Proof state:
ι : Type u_1
inst✝ : Finite ι
I : Box ι
⊢ Bornology.IsBounded (Box.Icc I)

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_1
inst✝ : Finite ι
I : Box ι
val✝ : Fintype ι
⊢ Bornology.IsBounded (Box.Icc I)

Proof state:
case intro
ι : Type u_1
inst✝ : Finite ι
I : Box ι
val✝ : Fintype ι
⊢ Bornology.IsBounded (Box.Icc I)

Tactic:
exact Metric.isBounded_Icc _ _

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_mul {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) : x ^ (y * z) = (x ^ y) ^ z

Proof state:
x : ℝ
hx : 0 ≤ x
y z : ℝ
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
rw [← Complex.ofReal_inj, Complex.ofReal_cpow (rpow_nonneg hx _),
    Complex.ofReal_cpow hx, Complex.ofReal_mul, Complex.cpow_mul, Complex.ofReal_cpow hx] <;>
  simp only [(Complex.ofReal_mul _ _).symm, (Complex.ofReal_log hx).symm, Complex.ofReal_im,
    neg_lt_zero, pi_pos, le_of_lt pi_pos]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem adjoin_empty : adjoin R (∅ : Set A) = ⊥ :=
  show adjoin R ⊥ = ⊥ by
    apply GaloisConnection.l_bot
    exact Algebra.gc

Proof state:
case gc
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ GaloisConnection (adjoin R) ?u

case u
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ Subalgebra R A → Set A

Tactic:
exact Algebra.gc

Result:
no goals

Proof state:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ adjoin R ⊥ = ⊥

Tactic:
apply GaloisConnection.l_bot

Result:
case gc
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ GaloisConnection (adjoin R) ?u

case u
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ Subalgebra R A → Set A
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem hom_f_injective {C₁ C₂ : HomologicalComplex V c} :
    Function.Injective fun f : Hom C₁ C₂ => f.f

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
⊢ Function.Injective fun f => f.f

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem diagonal_mul_diagonal [Fintype n] [DecidableEq n] (d₁ d₂ : n → α) :
    diagonal d₁ * diagonal d₂ = diagonal fun i => d₁ i * d₂ i

Proof state:
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
⊢ diagonal d₁ * diagonal d₂ = diagonal fun i => d₁ i * d₂ i

Tactic:
ext i j

Result:
case a
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ * diagonal d₂) i j = diagonal (fun i => d₁ i * d₂ i) i j

Proof state:
case a
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
i j : n
⊢ (diagonal d₁ * diagonal d₂) i j = diagonal (fun i => d₁ i * d₂ i) i j

Tactic:
by_cases h : i = j <;>
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem _root_.Char.utf8Size_pos (c : Char) : 0 < c.utf8Size

Proof state:
case hneg.hneg.hneg
c : Char
a✝² : ¬c.val ≤ UInt32.ofNatCore 127 Char.utf8Size.proof_1
a✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 Char.utf8Size.proof_2
a✝ : ¬c.val ≤ UInt32.ofNatCore 65535 Char.utf8Size.proof_3
⊢ 0 < 4

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem pos_iff_ne_zero' [NeZero n] (a : Fin n) : 0 < a ↔ a ≠ 0

Proof state:
n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ 0 < a ↔ a ≠ 0

Tactic:
rw [← val_pos_iff, Nat.pos_iff_ne_zero, val_ne_zero_iff]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem restrict_mono {s t : Set α} (h : s ⊆ t) {m m' : OuterMeasure α} (hm : m ≤ m') :
    restrict s m ≤ restrict t m' := fun u => by
  simp only [restrict_apply]
  exact (hm _).trans (m'.mono <| inter_subset_inter_right _ h)

Proof state:
α : Type u_1
s t : Set α
h : s ⊆ t
m m' : OuterMeasure α
hm : m ≤ m'
u : Set α
⊢ m (u ∩ s) ≤ m' (u ∩ t)

Tactic:
exact (hm _).trans (m'.mono <| inter_subset_inter_right _ h)

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
h : s ⊆ t
m m' : OuterMeasure α
hm : m ≤ m'
u : Set α
⊢ ((restrict s) m) u ≤ ((restrict t) m') u

Tactic:
simp only [restrict_apply]

Result:
α : Type u_1
s t : Set α
h : s ⊆ t
m m' : OuterMeasure α
hm : m ≤ m'
u : Set α
⊢ m (u ∩ s) ≤ m' (u ∩ t)
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
    (a * b).factorization = a.factorization + b.factorization

Proof state:
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (a * b).factorization p = (a.factorization + b.factorization) p

Tactic:
simp only [add_apply, ← primeFactorsList_count_eq,
  perm_iff_count.mp (perm_primeFactorsList_mul ha hb) p, count_append]

Result:
no goals

Proof state:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a * b).factorization = a.factorization + b.factorization

Tactic:
ext p

Result:
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ (a * b).factorization p = (a.factorization + b.factorization) p
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Integral.lean
lemma cfcₙL_integral (a : A) (f : X → C(quasispectrum 𝕜 a, 𝕜)₀) (hf₁ : Integrable f μ)
    (ha : p a

Proof state:
X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : RCLike 𝕜
inst✝⁸ : MeasurableSpace X
μ : Measure X
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : CompleteSpace A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : NormedSpace ℝ A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalContinuousFunctionalCalculus 𝕜 p
a : A
f : X → C(↑(quasispectrum 𝕜 a), 𝕜)₀
hf₁ : Integrable f μ
ha : autoParam (p a) _auto✝
⊢ ∫ (x : X), (cfcₙL ha) (f x) ∂μ = (cfcₙL ha) (∫ (x : X), f x ∂μ)

Tactic:
rw [ContinuousLinearMap.integral_comp_comm _ hf₁]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem rightDistributor_hom_comp_biproduct_π {J : Type} [Fintype J] (f : J → C) (X : C) (j : J) :
    (rightDistributor f X).hom ≫ biproduct.π _ j = biproduct.π _ j ▷ X

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ (rightDistributor f X).hom ≫ biproduct.π (fun j => f j ⊗ X) j = biproduct.π f j ▷ X

Tactic:
simp [rightDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ (rightDistributor f X).hom ≫ biproduct.π (fun j => f j ⊗ X) j = biproduct.π f j ▷ X

Tactic:
classical
simp [rightDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem tangentBundle_model_space_coe_chartAt (p : TangentBundle I H) :
    ⇑(chartAt (ModelProd H E) p) = TotalSpace.toProd H E

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
⊢ ↑(TotalSpace.toProd H E).toPartialEquiv = ⇑(TotalSpace.toProd H E)

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
⊢ ↑(chartAt (ModelProd H E) p) = ⇑(TotalSpace.toProd H E)

Tactic:
rw [← PartialHomeomorph.coe_coe, tangentBundle_model_space_chartAt]

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
⊢ ↑(TotalSpace.toProd H E).toPartialEquiv = ⇑(TotalSpace.toProd H E)
-- Mathlib/AlgebraicGeometry/RationalMap.lean
/-- A partial map from a reduced scheme to a separated scheme is equivalent to a morphism
if and only if it is equal to the restriction of the morphism. -/
lemma equiv_toPartialMap_iff_of_isSeparated [X.Over S] [Y.Over S] [IsReduced X]
    [IsSeparated (Y ↘ S)] {f : X.PartialMap Y} {g : X ⟶ Y}
    [f.IsOver S] [g.IsOver S] : f.equiv g.toPartialMap ↔
      f.hom = f.domain.ι ≫ g

Proof state:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst✝¹ : IsOver S f
inst✝ : Hom.IsOver g S
⊢ X.homOfLE ⋯ ≫ f.hom = (f.domain ⊓ ⊤).ι ≫ g ↔ (X.isoOfEq ⋯).hom ≫ f.hom = (f.domain ⊓ ⊤).ι ≫ g

Tactic:
rfl

Result:
no goals

Proof state:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst✝¹ : IsOver S f
inst✝ : Hom.IsOver g S
⊢ f.equiv (Hom.toPartialMap g) ↔ f.hom = f.domain.ι ≫ g

Tactic:
rw [equiv_iff_of_isSeparated (S := S), ← cancel_epi (X.isoOfEq (inf_top_eq f.domain)).hom]

Result:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst✝¹ : IsOver S f
inst✝ : Hom.IsOver g S
⊢ (f.restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom =
      ((Hom.toPartialMap g).restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom ↔
    (X.isoOfEq ⋯).hom ≫ f.hom = (X.isoOfEq ⋯).hom ≫ f.domain.ι ≫ g

Proof state:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst✝¹ : IsOver S f
inst✝ : Hom.IsOver g S
⊢ (f.restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom =
      ((Hom.toPartialMap g).restrict (f.domain ⊓ (Hom.toPartialMap g).domain) ⋯ ⋯).hom ↔
    (X.isoOfEq ⋯).hom ≫ f.hom = (X.isoOfEq ⋯).hom ≫ f.domain.ι ≫ g

Tactic:
simp

Result:
X Y S : Scheme
inst✝⁵ : X.Over S
inst✝⁴ : Y.Over S
inst✝³ : IsReduced X
inst✝² : IsSeparated (Y ↘ S)
f : X.PartialMap Y
g : X ⟶ Y
inst✝¹ : IsOver S f
inst✝ : Hom.IsOver g S
⊢ X.homOfLE ⋯ ≫ f.hom = (f.domain ⊓ ⊤).ι ≫ g ↔ (X.isoOfEq ⋯).hom ≫ f.hom = (f.domain ⊓ ⊤).ι ≫ g
-- Mathlib/NumberTheory/Divisors.lean
/-- This lemma justifies its existence from its utility in crystallographic root system theory. -/
lemma mul_mem_one_two_three_iff {a b : ℤ} :
    a * b ∈ ({1, 2, 3} : Set ℤ) ↔ (a, b) ∈ ({
      (1, 1), (-1, -1),
      (1, 2), (2, 1), (-1, -2), (-2, -1),
      (1, 3), (3, 1), (-1, -3), (-3, -1)} : Set (ℤ × ℤ))

Proof state:
a b : ℤ
⊢ (a, b) ∈ divisorsAntidiag 1 ∨ (a, b) ∈ divisorsAntidiag 2 ∨ (a, b) ∈ divisorsAntidiag 3 ↔
    (a, b) = (1, 1) ∨
      (a, b) = (-1, -1) ∨
        (a, b) = (1, 2) ∨
          (a, b) = (2, 1) ∨
            (a, b) = (-1, -2) ∨
              (a, b) = (-2, -1) ∨ (a, b) = (1, 3) ∨ (a, b) = (3, 1) ∨ (a, b) = (-1, -3) ∨ (a, b) = (-3, -1)

Tactic:
aesop

Result:
no goals

Proof state:
a b : ℤ
⊢ a * b ∈ {1, 2, 3} ↔
    (a, b) ∈ {(1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}

Tactic:
simp only [← Int.prodMk_mem_divisorsAntidiag, Set.mem_insert_iff, Set.mem_singleton_iff, ne_eq,
  one_ne_zero, not_false_eq_true, OfNat.ofNat_ne_zero]

Result:
a b : ℤ
⊢ (a, b) ∈ divisorsAntidiag 1 ∨ (a, b) ∈ divisorsAntidiag 2 ∨ (a, b) ∈ divisorsAntidiag 3 ↔
    (a, b) = (1, 1) ∨
      (a, b) = (-1, -1) ∨
        (a, b) = (1, 2) ∨
          (a, b) = (2, 1) ∨
            (a, b) = (-1, -2) ∨
              (a, b) = (-2, -1) ∨ (a, b) = (1, 3) ∨ (a, b) = (3, 1) ∨ (a, b) = (-1, -3) ∨ (a, b) = (-3, -1)
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem differentiableOn_of_locally_differentiableOn
    (h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)) :
    DifferentiableOn 𝕜 f s

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
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
xs : x ∈ s
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
rcases h x xs with ⟨t, t_open, xt, ht⟩

Result:
case intro.intro.intro
𝕜 : 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
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
xs : x ∈ s
t : Set E
t_open : IsOpen t
xt : x ∈ t
ht : DifferentiableOn 𝕜 f (s ∩ t)
⊢ DifferentiableWithinAt 𝕜 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
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
⊢ DifferentiableOn 𝕜 f s

Tactic:
intro x xs

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
f : E → F
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
xs : x ∈ s
⊢ DifferentiableWithinAt 𝕜 f s x

Proof state:
case intro.intro.intro
𝕜 : 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
s : Set E
h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
xs : x ∈ s
t : Set E
t_open : IsOpen t
xt : x ∈ t
ht : DifferentiableOn 𝕜 f (s ∩ t)
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
exact (differentiableWithinAt_inter (IsOpen.mem_nhds t_open xt)).1 (ht x ⟨xs, xt⟩)

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem sameCycle_apply_right : SameCycle f x (f y) ↔ SameCycle f x y

Proof state:
α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle x (f y) ↔ f.SameCycle x y

Tactic:
rw [sameCycle_comm, sameCycle_apply_left, sameCycle_comm]

Result:
no goals
-- Mathlib/Data/List/Destutter.lean
theorem destutter'_is_chain : ∀ l : List α, ∀ {a b}, R a b → (l.destutter' R b).Chain R a
  | [], _, _, h => chain_singleton.mpr h
  | c :: l, a, b, h => by
    rw [destutter']
    split_ifs with hbc
    · rw [chain_cons]
      exact ⟨h, destutter'_is_chain l hbc⟩
    · exact destutter'_is_chain l h

Proof state:
case neg
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
c : α
l : List α
a b : α
h : R a b
hbc : ¬R b c
⊢ Chain R a (destutter' R b l)

Tactic:
exact destutter'_is_chain l h

Result:
no goals

Proof state:
case pos
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
c : α
l : List α
a b : α
h : R a b
hbc : R b c
⊢ R a b ∧ Chain R b (destutter' R c l)

Tactic:
exact ⟨h, destutter'_is_chain l hbc⟩

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
c : α
l : List α
a b : α
h : R a b
⊢ Chain R a (destutter' R b (c :: l))

Tactic:
rw [destutter']

Result:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
c : α
l : List α
a b : α
h : R a b
⊢ Chain R a (if R b c then b :: destutter' R c l else destutter' R b l)

Proof state:
case pos
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
c : α
l : List α
a b : α
h : R a b
hbc : R b c
⊢ Chain R a (b :: destutter' R c l)

Tactic:
rw [chain_cons]

Result:
case pos
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
c : α
l : List α
a b : α
h : R a b
hbc : R b c
⊢ R a b ∧ Chain R b (destutter' R c l)

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
c : α
l : List α
a b : α
h : R a b
⊢ Chain R a (if R b c then b :: destutter' R c l else destutter' R b l)

Tactic:
split_ifs with hbc

Result:
case pos
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
c : α
l : List α
a b : α
h : R a b
hbc : R b c
⊢ Chain R a (b :: destutter' R c l)

case neg
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
c : α
l : List α
a b : α
h : R a b
hbc : ¬R b c
⊢ Chain R a (destutter' R b l)