harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Gluing.lean
theorem open_image_open (i : D.J) (U : Opens (𝖣.U i)) : IsOpen (𝖣.ι i '' U)

Proof state:
D : GlueData
i : D.J
U : Opens ↑(D.U i)
⊢ IsOpen (⇑(ConcreteCategory.hom (D.ι i)) '' ↑U)

Tactic:
rw [isOpen_iff]

Result:
D : GlueData
i : D.J
U : Opens ↑(D.U i)
⊢ ∀ (i_1 : D.J), IsOpen (⇑(ConcreteCategory.hom (D.ι i_1)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' ↑U))

Proof state:
D : GlueData
i : D.J
U : Opens ↑(D.U i)
j : D.J
⊢ IsOpen (⇑(ConcreteCategory.hom (D.f j i)) '' (⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' ↑U))

Tactic:
apply (D.f_open _ _).isOpenMap

Result:
case a
D : GlueData
i : D.J
U : Opens ↑(D.U i)
j : D.J
⊢ IsOpen (⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' ↑U)

Proof state:
D : GlueData
i : D.J
U : Opens ↑(D.U i)
j : D.J
⊢ IsOpen (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' ↑U))

Tactic:
rw [preimage_image_eq_image]

Result:
D : GlueData
i : D.J
U : Opens ↑(D.U i)
j : D.J
⊢ IsOpen (⇑(ConcreteCategory.hom (D.f j i)) '' (⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' ↑U))

Proof state:
case a.a
D : GlueData
i : D.J
U : Opens ↑(D.U i)
j : D.J
⊢ IsOpen ↑U

Tactic:
exact U.isOpen

Result:
no goals

Proof state:
D : GlueData
i : D.J
U : Opens ↑(D.U i)
⊢ ∀ (i_1 : D.J), IsOpen (⇑(ConcreteCategory.hom (D.ι i_1)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' ↑U))

Tactic:
intro j

Result:
D : GlueData
i : D.J
U : Opens ↑(D.U i)
j : D.J
⊢ IsOpen (⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' (⇑(ConcreteCategory.hom (D.ι i)) '' ↑U))

Proof state:
case a
D : GlueData
i : D.J
U : Opens ↑(D.U i)
j : D.J
⊢ IsOpen (⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' ↑U)

Tactic:
apply (D.t j i ≫ D.f i j).hom.continuous_toFun.isOpen_preimage

Result:
case a.a
D : GlueData
i : D.J
U : Opens ↑(D.U i)
j : D.J
⊢ IsOpen ↑U
-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem intervalIntegrable₀ (h₁f : Function.Periodic f T) (hT : 0 < T)
    (h₂f : IntervalIntegrable f MeasureTheory.volume 0 T) (a₁ a₂ : ℝ) :
    IntervalIntegrable f MeasureTheory.volume a₁ a₂

Proof state:
case h₂f
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume 0 T
a₁ a₂ : ℝ
⊢ IntervalIntegrable f volume 0 (0 + T)

Tactic:
simpa

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume 0 T
a₁ a₂ : ℝ
⊢ IntervalIntegrable f volume a₁ a₂

Tactic:
apply h₁f.intervalIntegrable hT (t := 0)

Result:
case h₂f
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
T : ℝ
h₁f : Periodic f T
hT : 0 < T
h₂f : IntervalIntegrable f volume 0 T
a₁ a₂ : ℝ
⊢ IntervalIntegrable f volume 0 (0 + T)
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma preimage_inr_Icc_zero_one :
    ((↑) : A → A⁺¹) ⁻¹' Icc 0 1 = {x : A | 0 ≤ x} ∩ closedBall 0 1

Proof state:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ inr ⁻¹' Icc 0 1 = {x | 0 ≤ x} ∩ closedBall 0 1

Tactic:
ext

Result:
case h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x✝ : A
⊢ x✝ ∈ inr ⁻¹' Icc 0 1 ↔ x✝ ∈ {x | 0 ≤ x} ∩ closedBall 0 1

Proof state:
case h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x✝ : A
⊢ x✝ ∈ inr ⁻¹' Icc 0 1 ↔ x✝ ∈ {x | 0 ≤ x} ∩ closedBall 0 1

Tactic:
simp [- mem_Icc, inr_mem_Icc_iff_norm_le]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_eq_eLpNorm' (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) {f : α → ε} :
    eLpNorm f p μ = eLpNorm' f (ENNReal.toReal p) μ

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α → ε
⊢ eLpNorm f p μ = eLpNorm' f p.toReal μ

Tactic:
simp [eLpNorm, hp_ne_zero, hp_ne_top]

Result:
no goals
-- Mathlib/Topology/Order/LowerUpperTopology.lean
theorem isOpen_iff_generate_Ici_compl : IsOpen s ↔ GenerateOpen { t | ∃ a, (Ici a)ᶜ = t } s

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
⊢ IsOpen s ↔ GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
theorem freeGroupoidFunctor_id :
    freeGroupoidFunctor (Prefunctor.id V) = Functor.id (FreeGroupoid V)

Proof state:
V : Type u
inst✝ : Quiver V
⊢ freeGroupoidFunctor (𝟭q V) = 𝟭 (FreeGroupoid V)

Tactic:
dsimp only [freeGroupoidFunctor]

Result:
V : Type u
inst✝ : Quiver V
⊢ lift (𝟭q V ⋙q of V) = 𝟭 (FreeGroupoid V)

Proof state:
case hΦ
V : Type u
inst✝ : Quiver V
⊢ of V ⋙q (𝟭 (FreeGroupoid V)).toPrefunctor = 𝟭q V ⋙q of V

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
inst✝ : Quiver V
⊢ lift (𝟭q V ⋙q of V) = 𝟭 (FreeGroupoid V)

Tactic:
symm

Result:
V : Type u
inst✝ : Quiver V
⊢ 𝟭 (FreeGroupoid V) = lift (𝟭q V ⋙q of V)

Proof state:
V : Type u
inst✝ : Quiver V
⊢ 𝟭 (FreeGroupoid V) = lift (𝟭q V ⋙q of V)

Tactic:
apply lift_unique

Result:
case hΦ
V : Type u
inst✝ : Quiver V
⊢ of V ⋙q (𝟭 (FreeGroupoid V)).toPrefunctor = 𝟭q V ⋙q of V
-- Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
theorem optimalGHDist_mem_candidatesB : optimalGHDist X Y ∈ candidatesB X Y

Proof state:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ GromovHausdorff.optimalGHDist X Y ∈ GromovHausdorff.candidatesB X Y

Tactic:
cases Classical.choose_spec (exists_minimizer X Y)

Result:
case intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
left✝ : Classical.choose ⋯ ∈ GromovHausdorff.candidatesB X Y
right✝ : ∀ g ∈ GromovHausdorff.candidatesB X Y, HD (Classical.choose ⋯) ≤ HD g
⊢ GromovHausdorff.optimalGHDist X Y ∈ GromovHausdorff.candidatesB X Y

Proof state:
case intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
left✝ : Classical.choose ⋯ ∈ GromovHausdorff.candidatesB X Y
right✝ : ∀ g ∈ GromovHausdorff.candidatesB X Y, HD (Classical.choose ⋯) ≤ HD g
⊢ GromovHausdorff.optimalGHDist X Y ∈ GromovHausdorff.candidatesB X Y

Tactic:
assumption

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
lemma le_max_left (a b : α) : a ≤ max a b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a ≤ max a b

Tactic:
if h : a ≤ b
then simpa [max_def, if_pos h] using h
else simp [max_def, if_neg h, le_refl]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ a ≤ max a b

Tactic:
simpa [max_def, if_pos h] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ a ≤ max a b

Tactic:
simp [max_def, if_neg h, le_refl]

Result:
no goals
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem range_inl_eq_ker_rightHom : (inl : N →* N ⋊[φ] G).range = rightHom.ker :=
  le_antisymm (fun _ ↦ by simp +contextual [MonoidHom.mem_ker, eq_comm])
    fun x hx ↦ ⟨x.left, by ext <;> simp_all [MonoidHom.mem_ker]⟩

Proof state:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x : N ⋊[φ] G
hx : x ∈ rightHom.ker
⊢ inl x.left = x

Tactic:
ext <;> simp_all [MonoidHom.mem_ker]

Result:
no goals

Proof state:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x✝ : N ⋊[φ] G
⊢ x✝ ∈ inl.range → x✝ ∈ rightHom.ker

Tactic:
simp +contextual [MonoidHom.mem_ker, eq_comm]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean
theorem adjoin_iff_disjoint [Nontrivial A] {s t : Set ι} :
    (AlgebraicIndependent (adjoin R (x '' s)) fun i : t ↦ x i) ↔ Disjoint s t

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s t : Set ι
ind : AlgebraicIndependent ↥(adjoin R (x '' s)) fun i => x ↑i
ndisj : ¬Disjoint s t
i : ι
hs : i ∈ s
ht : i ∈ t
⊢ False

Tactic:
refine ind.transcendental ⟨i, ht⟩ (isAlgebraic_algebraMap (⟨_, subset_adjoin ?_⟩ : adjoin R _))

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s t : Set ι
ind : AlgebraicIndependent ↥(adjoin R (x '' s)) fun i => x ↑i
ndisj : ¬Disjoint s t
i : ι
hs : i ∈ s
ht : i ∈ t
⊢ x ↑⟨i, ht⟩ ∈ x '' s

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s t : Set ι
ind : AlgebraicIndependent ↥(adjoin R (x '' s)) fun i => x ↑i
ndisj : ¬Disjoint s t
⊢ False

Tactic:
have ⟨i, hs, ht⟩ := Set.not_disjoint_iff.mp ndisj

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s t : Set ι
ind : AlgebraicIndependent ↥(adjoin R (x '' s)) fun i => x ↑i
ndisj : ¬Disjoint s t
i : ι
hs : i ∈ s
ht : i ∈ t
⊢ False

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s t : Set ι
ind : AlgebraicIndependent ↥(adjoin R (x '' s)) fun i => x ↑i
ndisj : ¬Disjoint s t
i : ι
hs : i ∈ s
ht : i ∈ t
⊢ x ↑⟨i, ht⟩ ∈ x '' s

Tactic:
exact ⟨i, hs, rfl⟩

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s t : Set ι
⊢ (AlgebraicIndependent ↥(adjoin R (x '' s)) fun i => x ↑i) ↔ Disjoint s t

Tactic:
refine ⟨fun ind ↦ of_not_not fun ndisj ↦ ?_, adjoin_of_disjoint hx⟩

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s t : Set ι
ind : AlgebraicIndependent ↥(adjoin R (x '' s)) fun i => x ↑i
ndisj : ¬Disjoint s t
⊢ False
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_le (n : ℕ) (h : coeff R n φ ≠ 0) : order φ ≤ n

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff R n) φ ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑n

Tactic:
simpa using ⟨n, le_rfl, h⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff R n) φ ≠ 0
⊢ φ.order ≤ ↑n

Tactic:
rw [order, dif_neg]

Result:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff R n) φ ≠ 0
⊢ ↑(Nat.find ⋯) ≤ ↑n

case hnc
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff R n) φ ≠ 0
⊢ ¬φ = 0

Proof state:
case hnc
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : (coeff R n) φ ≠ 0
⊢ ¬φ = 0

Tactic:
exact exists_coeff_ne_zero_iff_ne_zero.mp ⟨n, h⟩

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma succAbove_castPred_of_lt (p i : Fin (n + 1)) (h : i < p)
    (hi := Fin.ne_of_lt <| Nat.lt_of_lt_of_le h p.le_last) : succAbove p (i.castPred hi) = i

Proof state:
n : ℕ
p i : Fin (n + 1)
h : i < p
hi : optParam (i ≠ last n) ⋯
⊢ p.succAbove (i.castPred hi) = i

Tactic:
rw [succAbove_of_castSucc_lt _ _ (castSucc_castPred _ _ ▸ h), castSucc_castPred]

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.nhds_hasBasis {b : Set (Set α)} (hb : IsTopologicalBasis b) {a : α} :
    (𝓝 a).HasBasis (fun t : Set α => t ∈ b ∧ a ∈ t) fun t => t :=
  ⟨fun s => hb.mem_nhds_iff.trans <| by simp only [and_assoc]⟩

Proof state:
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
a : α
s : Set α
⊢ (∃ t ∈ b, a ∈ t ∧ t ⊆ s) ↔ ∃ i, (i ∈ b ∧ a ∈ i) ∧ i ⊆ s

Tactic:
simp only [and_assoc]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem hsum_equiv (e : α ≃ β) (s : SummableFamily Γ R α) : (Equiv e s).hsum = s.hsum

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
g : Γ
⊢ (Equiv e s).hsum.coeff g = s.hsum.coeff g

Tactic:
simp only [coeff_hsum, Equiv_toFun]

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
g : Γ
⊢ ∑ᶠ (i : β), (s (e.symm i)).coeff g = ∑ᶠ (i : α), (s i).coeff g

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
g : Γ
⊢ ∑ᶠ (i : β), (s (e.symm i)).coeff g = ∑ᶠ (i : α), (s i).coeff g

Tactic:
exact finsum_eq_of_bijective e.symm (Equiv.bijective e.symm) fun x => rfl

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
⊢ (Equiv e s).hsum = s.hsum

Tactic:
ext g

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
g : Γ
⊢ (Equiv e s).hsum.coeff g = s.hsum.coeff g
-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
lemma norm_fourierSMulRight_le (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) :
    ‖fourierSMulRight L f v‖ ≤ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖ := calc
  ‖fourierSMulRight L f v‖ = (2 * π) * ‖L v‖ * ‖f v‖ := norm_fourierSMulRight _ _ _
  _ ≤ (2 * π) * (‖L‖ * ‖v‖) * ‖f v‖

Proof state:
case h.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
⊢ ‖L v‖ ≤ ‖L‖ * ‖v‖

Tactic:
exact L.le_opNorm _

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
⊢ 2 * π * (‖L‖ * ‖v‖) * ‖f v‖ = 2 * π * ‖L‖ * ‖v‖ * ‖f v‖

Tactic:
ring

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
⊢ 2 * π * ‖L v‖ * ‖f v‖ ≤ 2 * π * (‖L‖ * ‖v‖) * ‖f v‖

Tactic:
gcongr

Result:
case h.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
⊢ ‖L v‖ ≤ ‖L‖ * ‖v‖
-- Mathlib/Algebra/Order/Sub/Basic.lean
theorem tsub_add_cancel_iff_le : b - a + a = b ↔ a ≤ b

Proof state:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ b - a + a = b ↔ a ≤ b

Tactic:
rw [add_comm]

Result:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a + (b - a) = b ↔ a ≤ b

Proof state:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a + (b - a) = b ↔ a ≤ b

Tactic:
exact add_tsub_cancel_iff_le

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem addSubmonoid_smul_bot (S : AddSubmonoid R) : S • (⊥ : AddSubmonoid A) = ⊥ :=
  eq_bot_iff.2 <| smul_le.2 fun m _ n hn => by
    rw [AddSubmonoid.mem_bot] at hn ⊢; rw [hn, smul_zero]

Proof state:
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
S : AddSubmonoid R
m : R
x✝ : m ∈ S
n : A
hn : n ∈ ⊥
⊢ m • n ∈ ⊥

Tactic:
rw [AddSubmonoid.mem_bot] at hn ⊢

Result:
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
S : AddSubmonoid R
m : R
x✝ : m ∈ S
n : A
hn : n = 0
⊢ m • n = 0

Proof state:
R : Type u_4
A : Type u_5
inst✝² : AddMonoid A
inst✝¹ : AddMonoid R
inst✝ : DistribSMul R A
S : AddSubmonoid R
m : R
x✝ : m ∈ S
n : A
hn : n = 0
⊢ m • n = 0

Tactic:
rw [hn, smul_zero]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem add_zero (n : ZNum) : n + 0 = n

Proof state:
n : ZNum
⊢ n + 0 = n

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/GroupTheory/Perm/ClosureSwap.lean
theorem surjective_of_isSwap_of_isPretransitive [Finite α] (S : Set G)
    (hS1 : ∀ σ ∈ S, Perm.IsSwap (MulAction.toPermHom G α σ)) (hS2 : Subgroup.closure S = ⊤)
    [h : MulAction.IsPretransitive G α] : Function.Surjective (MulAction.toPermHom G α)

Proof state:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : DecidableEq α
inst✝ : Finite α
S : Set G
hS1 : ∀ σ ∈ S, ((toPermHom G α) σ).IsSwap
hS2 : closure S = ⊤
h : IsPretransitive G α
this : IsPretransitive (↥(toPermHom G α).range) α
⊢ (toPermHom G α).range = ⊤

Tactic:
rw [MonoidHom.range_eq_map, ← hS2, MonoidHom.map_closure] at this ⊢

Result:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : DecidableEq α
inst✝ : Finite α
S : Set G
hS1 : ∀ σ ∈ S, ((toPermHom G α) σ).IsSwap
hS2 : closure S = ⊤
h : IsPretransitive G α
this : IsPretransitive (↥(closure (⇑(toPermHom G α) '' S))) α
⊢ closure (⇑(toPermHom G α) '' S) = ⊤

Proof state:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : DecidableEq α
inst✝ : Finite α
S : Set G
hS1 : ∀ σ ∈ S, ((toPermHom G α) σ).IsSwap
hS2 : closure S = ⊤
h : IsPretransitive G α
⊢ Function.Surjective ⇑(toPermHom G α)

Tactic:
rw [← MonoidHom.range_eq_top]

Result:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : DecidableEq α
inst✝ : Finite α
S : Set G
hS1 : ∀ σ ∈ S, ((toPermHom G α) σ).IsSwap
hS2 : closure S = ⊤
h : IsPretransitive G α
⊢ (toPermHom G α).range = ⊤

Proof state:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : DecidableEq α
inst✝ : Finite α
S : Set G
hS1 : ∀ σ ∈ S, ((toPermHom G α) σ).IsSwap
hS2 : closure S = ⊤
h : IsPretransitive G α
⊢ (toPermHom G α).range = ⊤

Tactic:
have := MulAction.IsPretransitive.of_compHom (α := α) (MulAction.toPermHom G α).rangeRestrict

Result:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : DecidableEq α
inst✝ : Finite α
S : Set G
hS1 : ∀ σ ∈ S, ((toPermHom G α) σ).IsSwap
hS2 : closure S = ⊤
h : IsPretransitive G α
this : IsPretransitive (↥(toPermHom G α).range) α
⊢ (toPermHom G α).range = ⊤

Proof state:
G : Type u_1
α : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : DecidableEq α
inst✝ : Finite α
S : Set G
hS1 : ∀ σ ∈ S, ((toPermHom G α) σ).IsSwap
hS2 : closure S = ⊤
h : IsPretransitive G α
this : IsPretransitive (↥(closure (⇑(toPermHom G α) '' S))) α
⊢ closure (⇑(toPermHom G α) '' S) = ⊤

Tactic:
exact closure_of_isSwap_of_isPretransitive (Set.forall_mem_image.2 hS1)

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem forall_imp_iff_exists_imp {α : Sort*} {p : α → Prop} {b : Prop} [ha : Nonempty α] :
    (∀ x, p x) → b ↔ ∃ x, p x → b

Proof state:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b

Tactic:
let ⟨a⟩ := ha

Result:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
a : α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b

Proof state:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
a : α
h : (∀ (x : α), p x) → b
h' : ∀ (x : α), ¬(p x → b)
⊢ False

Tactic:
exact if hb : b then h' a fun _ ↦ hb else hb <| h fun x ↦ (_root_.not_imp.1 (h' x)).1

Result:
no goals

Proof state:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
a : α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b

Tactic:
refine ⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩

Result:
α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
a : α
h : (∀ (x : α), p x) → b
h' : ∀ (x : α), ¬(p x → b)
⊢ False
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem det_of_lowerTriangular [LinearOrder m] (M : Matrix m m R) (h : M.BlockTriangular toDual) :
    M.det = ∏ i : m, M i i

Proof state:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : LinearOrder m
M : Matrix m m R
h : M.BlockTriangular ⇑toDual
⊢ M.det = ∏ i : m, M i i

Tactic:
rw [← det_transpose]

Result:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : LinearOrder m
M : Matrix m m R
h : M.BlockTriangular ⇑toDual
⊢ Mᵀ.det = ∏ i : m, M i i

Proof state:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : LinearOrder m
M : Matrix m m R
h : M.BlockTriangular ⇑toDual
⊢ Mᵀ.det = ∏ i : m, M i i

Tactic:
exact det_of_upperTriangular h.transpose

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem cylinder_eq_res (x : ℕ → α) (n : ℕ) :
    cylinder x n = { y | res y n = res x n }

Proof state:
α : Type u_2
x : ℕ → α
n : ℕ
⊢ cylinder x n = {y | res y n = res x n}

Tactic:
ext y

Result:
case h
α : Type u_2
x : ℕ → α
n : ℕ
y : ℕ → α
⊢ y ∈ cylinder x n ↔ y ∈ {y | res y n = res x n}

Proof state:
case h
α : Type u_2
x : ℕ → α
n : ℕ
y : ℕ → α
⊢ y ∈ cylinder x n ↔ y ∈ {y | res y n = res x n}

Tactic:
dsimp [cylinder]

Result:
case h
α : Type u_2
x : ℕ → α
n : ℕ
y : ℕ → α
⊢ (∀ i < n, y i = x i) ↔ res y n = res x n

Proof state:
case h
α : Type u_2
x : ℕ → α
n : ℕ
y : ℕ → α
⊢ (∀ i < n, y i = x i) ↔ res y n = res x n

Tactic:
rw [res_eq_res]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem one_lt_rpow_of_pos_of_lt_one_of_neg (hx1 : 0 < x) (hx2 : x < 1) (hz : z < 0) :
    1 < x ^ z

Proof state:
case h.e'_3
x z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ 1 = x ^ 0

Tactic:
exact (rpow_zero x).symm

Result:
no goals

Proof state:
x z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ 1 < x ^ z

Tactic:
convert rpow_lt_rpow_of_exponent_gt hx1 hx2 hz

Result:
case h.e'_3
x z : ℝ
hx1 : 0 < x
hx2 : x < 1
hz : z < 0
⊢ 1 = x ^ 0
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem measurableSet_region_between_oc (hf : Measurable f) (hg : Measurable g)
    (hs : MeasurableSet s) :
    MeasurableSet { p : α × ℝ | p.fst ∈ s ∧ p.snd ∈ Ioc (f p.fst) (g p.fst) }

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet ({a | a.1 ∈ s} ∩ {a | a.2 ∈ {a_1 | f a.1 < a_1} ∩ {a_1 | a_1 ≤ g a.1}})

Tactic:
refine
  MeasurableSet.inter ?_
    ((measurableSet_lt (hf.comp measurable_fst) measurable_snd).inter
      (measurableSet_le measurable_snd (hg.comp measurable_fst)))

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {a | a.1 ∈ s}

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ioc (f p.1) (g p.1)}

Tactic:
dsimp only [regionBetween, Ioc, mem_setOf_eq, setOf_and]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet ({a | a.1 ∈ s} ∩ {a | a.2 ∈ {a_1 | f a.1 < a_1} ∩ {a_1 | a_1 ≤ g a.1}})

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ MeasurableSet {a | a.1 ∈ s}

Tactic:
exact measurable_fst hs

Result:
no goals