harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fintype/Pi.lean
@[simp]
lemma piFinset_of_isEmpty [IsEmpty α] (s : ∀ a, Finset (γ a)) : piFinset s = univ :=
  eq_univ_of_forall fun _ ↦ by simp

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
γ : α → Type u_3
inst✝ : IsEmpty α
s : (a : α) → Finset (γ a)
x✝ : (a : α) → γ a
⊢ x✝ ∈ piFinset s

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem mem_of_nextOr_ne {xs : List α} {x d : α} (h : nextOr xs x d ≠ d) : x ∈ xs

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (z :: zs).nextOr x d ≠ d
hx : ¬x = y
⊢ x ∈ y :: z :: zs

Tactic:
simpa [hx] using IH h

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
x d : α
h : [].nextOr x d ≠ d
⊢ x ∈ []

Tactic:
simp at h

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
⊢ x ∈ y :: z :: zs

Tactic:
by_cases hx : x = y

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
hx : x = y
⊢ x ∈ y :: z :: zs

case neg
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
hx : ¬x = y
⊢ x ∈ y :: z :: zs

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h : xs.nextOr x d ≠ d
⊢ x ∈ xs

Tactic:
induction' xs with y ys IH

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
x d : α
h : [].nextOr x d ≠ d
⊢ x ∈ []

case cons
α : Type u_1
inst✝ : DecidableEq α
x d y : α
ys : List α
IH : ys.nextOr x d ≠ d → x ∈ ys
h : (y :: ys).nextOr x d ≠ d
⊢ x ∈ y :: ys

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
hx : ¬x = y
⊢ x ∈ y :: z :: zs

Tactic:
rw [nextOr_cons_of_ne _ _ _ _ hx] at h

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (z :: zs).nextOr x d ≠ d
hx : ¬x = y
⊢ x ∈ y :: z :: zs

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
x d y : α
ys : List α
IH : ys.nextOr x d ≠ d → x ∈ ys
h : (y :: ys).nextOr x d ≠ d
⊢ x ∈ y :: ys

Tactic:
rcases ys with - | ⟨z, zs⟩

Result:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d y : α
IH : [].nextOr x d ≠ d → x ∈ []
h : [y].nextOr x d ≠ d
⊢ x ∈ [y]

case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
⊢ x ∈ y :: z :: zs

Proof state:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d y : α
IH : [].nextOr x d ≠ d → x ∈ []
h : [y].nextOr x d ≠ d
⊢ x ∈ [y]

Tactic:
simp at h

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
hx : x = y
⊢ x ∈ y :: z :: zs

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem mem_factors_of_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) (hd : p ∣ a) :
    Associates.mk p ∈ factors (Associates.mk a)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
⊢ Associates.mk p ∈ ↑(factors' a)

Tactic:
exact mem_factorSet_some.mpr (mem_factors'_of_dvd ha0 hp hd)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
⊢ Associates.mk p ∈ (Associates.mk a).factors

Tactic:
rw [factors_mk _ ha0]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
hd : p ∣ a
⊢ Associates.mk p ∈ ↑(factors' a)
-- Mathlib/Data/PFun.lean
theorem prodMap_id_id : (PFun.id α).prodMap (PFun.id β) = PFun.id _ :=
  ext fun _ _ ↦ by simp [eq_comm]

Proof state:
α : Type u_1
β : Type u_2
x✝¹ x✝ : α × β
⊢ x✝ ∈ (PFun.id α).prodMap (PFun.id β) x✝¹ ↔ x✝ ∈ PFun.id (α × β) x✝¹

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
theorem pullback.congrHom_inv {X Y Z : C} {f₁ f₂ : X ⟶ Z} {g₁ g₂ : Y ⟶ Z} (h₁ : f₁ = f₂)
    (h₂ : g₁ = g₂) [HasPullback f₁ g₁] [HasPullback f₂ g₂] :
    (pullback.congrHom h₁ h₂).inv =
      pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) (by simp [h₁]) (by simp [h₂])

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ (congrHom h₁ h₂).inv = map f₂ g₂ f₁ g₁ (𝟙 X) (𝟙 Y) (𝟙 Z) ⋯ ⋯

Tactic:
ext <;> simp [Iso.inv_comp_eq]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ f₂ ≫ 𝟙 Z = 𝟙 X ≫ f₁

Tactic:
simp [h₁]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z : C
f₁ f₂ : X ⟶ Z
g₁ g₂ : Y ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst✝¹ : HasPullback f₁ g₁
inst✝ : HasPullback f₂ g₂
⊢ g₂ ≫ 𝟙 Z = 𝟙 Y ≫ g₁

Tactic:
simp [h₂]

Result:
no goals
-- Mathlib/Analysis/Convex/Integral.lean
theorem ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const [StrictConvexSpace ℝ E] (ht : μ t ≠ ∞)
    (h_le : ∀ᵐ x ∂μ.restrict t, ‖f x‖ ≤ C) :
    f =ᵐ[μ.restrict t] const α (⨍ x in t, f x ∂μ) ∨ ‖∫ x in t, f x ∂μ‖ < (μ t).toReal * C

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
t : Set α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
ht : μ t ≠ ⊤
h_le : ∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C
this : Fact (μ t < ⊤)
⊢ f =ᶠ[ae (μ.restrict t)] const α (⨍ (x : α) in t, f x ∂μ) ∨ ‖∫ (x : α) in t, f x ∂μ‖ < ((μ.restrict t) univ).toReal * C

Tactic:
exact ae_eq_const_or_norm_integral_lt_of_norm_le_const h_le

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
t : Set α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
ht : μ t ≠ ⊤
h_le : ∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C
⊢ f =ᶠ[ae (μ.restrict t)] const α (⨍ (x : α) in t, f x ∂μ) ∨ ‖∫ (x : α) in t, f x ∂μ‖ < (μ t).toReal * C

Tactic:
haveI := Fact.mk ht.lt_top

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
t : Set α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
ht : μ t ≠ ⊤
h_le : ∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C
this : Fact (μ t < ⊤)
⊢ f =ᶠ[ae (μ.restrict t)] const α (⨍ (x : α) in t, f x ∂μ) ∨ ‖∫ (x : α) in t, f x ∂μ‖ < (μ t).toReal * C

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
t : Set α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
ht : μ t ≠ ⊤
h_le : ∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C
this : Fact (μ t < ⊤)
⊢ f =ᶠ[ae (μ.restrict t)] const α (⨍ (x : α) in t, f x ∂μ) ∨ ‖∫ (x : α) in t, f x ∂μ‖ < (μ t).toReal * C

Tactic:
rw [← restrict_apply_univ]

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
t : Set α
f : α → E
C : ℝ
inst✝ : StrictConvexSpace ℝ E
ht : μ t ≠ ⊤
h_le : ∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C
this : Fact (μ t < ⊤)
⊢ f =ᶠ[ae (μ.restrict t)] const α (⨍ (x : α) in t, f x ∂μ) ∨ ‖∫ (x : α) in t, f x ∂μ‖ < ((μ.restrict t) univ).toReal * C
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forIn_map [Monad m] [LawfulMonad m]
    (l : List α) (g : α → β) (f : β → γ → m (ForInStep γ)) :
    forIn (l.map g) init f = forIn l init fun a y => f (g a) y

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
g : α → β
f : β → γ → m (ForInStep γ)
⊢ forIn (map g l) init f = forIn l init fun a y => f (g a) y

Tactic:
induction l generalizing init <;> simp_all

Result:
no goals
-- Mathlib/Logic/Equiv/Set.lean
lemma setOf_apply_symm_eq_image_setOf {α β} (e : α ≃ β) (p : α → Prop) :
    {b | p (e.symm b)} = e '' {a | p a}

Proof state:
α : Type u_1
β : Type u_2
e : α ≃ β
p : α → Prop
⊢ {b | p (e.symm b)} = ⇑e '' {a | p a}

Tactic:
rw [Equiv.image_eq_preimage, preimage_setOf_eq]

Result:
no goals
-- Mathlib/Algebra/CharP/Reduced.lean
theorem iterateFrobenius_inj : Function.Injective (iterateFrobenius R p n) := fun x y H ↦ by
  rw [← sub_eq_zero] at H ⊢
  simp_rw [iterateFrobenius_def, ← sub_pow_expChar_pow] at H
  exact IsReduced.eq_zero _ ⟨_, H⟩

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p n : ℕ
inst✝ : ExpChar R p
x y : R
H : (x - y) ^ p ^ n = 0
⊢ x - y = 0

Tactic:
exact IsReduced.eq_zero _ ⟨_, H⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p n : ℕ
inst✝ : ExpChar R p
x y : R
H : (iterateFrobenius R p n) x = (iterateFrobenius R p n) y
⊢ x = y

Tactic:
rw [← sub_eq_zero] at H ⊢

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p n : ℕ
inst✝ : ExpChar R p
x y : R
H : (iterateFrobenius R p n) x - (iterateFrobenius R p n) y = 0
⊢ x - y = 0

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p n : ℕ
inst✝ : ExpChar R p
x y : R
H : (iterateFrobenius R p n) x - (iterateFrobenius R p n) y = 0
⊢ x - y = 0

Tactic:
simp_rw [iterateFrobenius_def, ← sub_pow_expChar_pow] at H

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsReduced R
p n : ℕ
inst✝ : ExpChar R p
x y : R
H : (x - y) ^ p ^ n = 0
⊢ x - y = 0
-- Mathlib/Order/Hom/Lattice.lean
theorem cancel_left {g : LatticeHom β γ} {f₁ f₂ : LatticeHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => LatticeHom.ext fun a => hg <| by rw [← LatticeHom.comp_apply, h, LatticeHom.comp_apply],
    congr_arg _⟩

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
g : LatticeHom β γ
f₁ f₂ : LatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← LatticeHom.comp_apply, h, LatticeHom.comp_apply]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma pow_le_iff_le_log (hx : 0 < x) (hy : 0 < y) : x ^ n ≤ y ↔ n * log x ≤ log y

Proof state:
x y : ℝ
n : ℕ
hx : 0 < x
hy : 0 < y
⊢ x ^ n ≤ y ↔ ↑n * log x ≤ log y

Tactic:
rw [← rpow_le_iff_le_log hx hy, rpow_natCast]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem neg_coe_abs_toReal_of_sign_nonpos {θ : Angle} (h : θ.sign ≤ 0) : -↑|θ.toReal| = θ

Proof state:
case inr
θ : Angle
h : θ.sign = 0
⊢ -↑|θ.toReal| = θ

Tactic:
rw [sign_eq_zero_iff] at h

Result:
case inr
θ : Angle
h : θ = 0 ∨ θ = ↑π
⊢ -↑|θ.toReal| = θ

Proof state:
θ : Angle
h : θ.sign = -1 ∨ θ.sign = 0
⊢ -↑|θ.toReal| = θ

Tactic:
rcases h with (h | h)

Result:
case inl
θ : Angle
h : θ.sign = -1
⊢ -↑|θ.toReal| = θ

case inr
θ : Angle
h : θ.sign = 0
⊢ -↑|θ.toReal| = θ

Proof state:
case inr
θ : Angle
h : θ = 0 ∨ θ = ↑π
⊢ -↑|θ.toReal| = θ

Tactic:
rcases h with (rfl | rfl) <;> simp [abs_of_pos Real.pi_pos]

Result:
no goals

Proof state:
case inl
θ : Angle
h : θ.sign = -1
⊢ -↑|θ.toReal| = θ

Tactic:
rw [abs_of_neg (toReal_neg_iff_sign_neg.2 h), coe_neg, neg_neg, coe_toReal]

Result:
no goals

Proof state:
θ : Angle
h : θ.sign ≤ 0
⊢ -↑|θ.toReal| = θ

Tactic:
rw [SignType.nonpos_iff] at h

Result:
θ : Angle
h : θ.sign = -1 ∨ θ.sign = 0
⊢ -↑|θ.toReal| = θ
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
@[simp]
lemma map_swap {S : Type*} [Semiring S] (f : R →+* S) (i j : n) :
    (swap R i j).map f = swap S i j

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Semiring R
inst✝¹ : DecidableEq n
S : Type u_4
inst✝ : Semiring S
f : R →+* S
i j : n
⊢ (swap R i j).map ⇑f = swap S i j

Tactic:
simp [swap]

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem WellFoundedOn.union (hs : s.WellFoundedOn r) (ht : t.WellFoundedOn r) :
    (s ∪ t).WellFoundedOn r

Proof state:
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : s.WellFoundedOn r
ht : t.WellFoundedOn r
⊢ (s ∪ t).WellFoundedOn r

Tactic:
rw [wellFoundedOn_iff_no_descending_seq] at *

Result:
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
⊢ ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s ∪ t

Proof state:
case intro.inl
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
f : (fun x1 x2 => x1 > x2) ↪r r
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), f (g n) ∈ s
⊢ False

case intro.inr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
f : (fun x1 x2 => x1 > x2) ↪r r
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), f (g n) ∈ t
⊢ False

Tactic:
exacts [hs (g.dual.ltEmbedding.trans f) hg, ht (g.dual.ltEmbedding.trans f) hg]

Result:
no goals

Proof state:
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
⊢ ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s ∪ t

Tactic:
rintro f hf

Result:
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
f : (fun x1 x2 => x1 > x2) ↪r r
hf : ∀ (n : ℕ), f n ∈ s ∪ t
⊢ False

Proof state:
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
f : (fun x1 x2 => x1 > x2) ↪r r
hf : ∀ (n : ℕ), f n ∈ s ∪ t
⊢ False

Tactic:
rcases Nat.exists_subseq_of_forall_mem_union f hf with ⟨g, hg | hg⟩

Result:
case intro.inl
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
f : (fun x1 x2 => x1 > x2) ↪r r
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), f (g n) ∈ s
⊢ False

case intro.inr
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s
ht : ∀ (f : (fun x1 x2 => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ t
f : (fun x1 x2 => x1 > x2) ↪r r
hf : ∀ (n : ℕ), f n ∈ s ∪ t
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), f (g n) ∈ t
⊢ False
-- Mathlib/Analysis/Calculus/VectorField.lean
@[simp] lemma pullbackWithin_univ {f : E → F} {V : F → F} :
    pullbackWithin 𝕜 f V univ = pullback 𝕜 f V

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
V : F → F
⊢ pullbackWithin 𝕜 f V univ = pullback 𝕜 f V

Tactic:
ext x

Result:
case h
𝕜 : 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
V : F → F
x : E
⊢ pullbackWithin 𝕜 f V univ x = pullback 𝕜 f V x

Proof state:
case h
𝕜 : 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
V : F → F
x : E
⊢ pullbackWithin 𝕜 f V univ x = pullback 𝕜 f V x

Tactic:
simp [pullbackWithin, pullback]

Result:
no goals
-- Mathlib/Algebra/CharP/MixedCharZero.lean
theorem split_by_characteristic_localRing [IsLocalRing R]
    (h_pos : ∀ p : ℕ, IsPrimePow p → CharP R p → P) (h_equal : Algebra ℚ R → P)
    (h_mixed : ∀ p : ℕ, Nat.Prime p → MixedCharZero R p → P) : P

Proof state:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsLocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
p_ppow : IsPrimePow p
⊢ P

Tactic:
exact h_pos p p_ppow p_char

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsLocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ P

Tactic:
refine split_by_characteristic R ?_ h_equal h_mixed

Result:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsLocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ ∀ (p : ℕ), p ≠ 0 → CharP R p → P

Proof state:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsLocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
⊢ ∀ (p : ℕ), p ≠ 0 → CharP R p → P

Tactic:
intro p p_pos p_char

Result:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsLocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
⊢ P

Proof state:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsLocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
⊢ P

Tactic:
have p_ppow : IsPrimePow (p : ℕ) := or_iff_not_imp_left.mp (charP_zero_or_prime_power R p) p_pos

Result:
R : Type u_1
inst✝¹ : CommRing R
P : Prop
inst✝ : IsLocalRing R
h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P
h_equal : Algebra ℚ R → P
h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
p : ℕ
p_pos : p ≠ 0
p_char : CharP R p
p_ppow : IsPrimePow p
⊢ P
-- Mathlib/Tactic/Ring/Basic.lean
theorem cast_rat {n : ℤ} {d : ℕ} {R} [DivisionRing R] {a : R} :
    IsRat a n d → a = Rat.rawCast n d + 0
  | ⟨_, e⟩ => by simp [e, div_eq_mul_inv]

Proof state:
n : ℤ
d : ℕ
R : Type u_2
inst✝ : DivisionRing R
a : R
inv✝ : Invertible ↑d
e : a = ↑n * ⅟↑d
⊢ a = Rat.rawCast n d + 0

Tactic:
simp [e, div_eq_mul_inv]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem map_zero (f : α → β) : (0 : Measure α).map f = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
⊢ map f 0 = 0

Tactic:
by_cases hf : AEMeasurable f (0 : Measure α) <;> simp [map, hf]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem frontier_thickening_disjoint (A : Set α) :
    Pairwise (Disjoint on fun r : ℝ => frontier (thickening r A))

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
⊢ Pairwise (Disjoint on fun r => frontier (thickening r A))

Tactic:
refine (pairwise_disjoint_on _).2 fun r₁ r₂ hr => ?_

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))

Proof state:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : r₁ ≤ 0
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))

Tactic:
simp [thickening_of_nonpos h₁]

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))

Tactic:
rcases le_total r₁ 0 with h₁ | h₁

Result:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : r₁ ≤ 0
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))

case inr
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))

Proof state:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
h : ENNReal.ofReal r₁ = ENNReal.ofReal r₂
⊢ r₁ = r₂

Tactic:
apply_fun ENNReal.toReal at h

Result:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
h : (ENNReal.ofReal r₁).toReal = (ENNReal.ofReal r₂).toReal
⊢ r₁ = r₂

Proof state:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
h : (ENNReal.ofReal r₁).toReal = (ENNReal.ofReal r₂).toReal
⊢ r₁ = r₂

Tactic:
rwa [ENNReal.toReal_ofReal h₁, ENNReal.toReal_ofReal (h₁.trans hr.le)] at h

Result:
no goals

Proof state:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))

Tactic:
refine ((disjoint_singleton.2 fun h => hr.ne ?_).preimage _).mono (frontier_thickening_subset _)
  (frontier_thickening_subset _)

Result:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
h : ENNReal.ofReal r₁ = ENNReal.ofReal r₂
⊢ r₁ = r₂
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Tendsto.atTop_zsmul_const {f : α → ℤ} (hr : 0 < r) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x • r) l atTop

Proof state:
case intro
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ ↑n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Tactic:
exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (zsmul_le_zsmul_left hr.le ha)

Result:
no goals

Proof state:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Tactic:
obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr

Result:
case intro
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Proof state:
case intro
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Tactic:
replace hn : s ≤ (n : ℤ) • r := by simpa

Result:
case intro
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ ↑n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Proof state:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ s ≤ ↑n • r

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x • r) l atTop

Tactic:
refine tendsto_atTop.mpr fun s => ?_

Result:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r