harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem SameCycle.of_zpow {n : ℤ} : SameCycle (f ^ n) x y → SameCycle f x y := fun ⟨m, h⟩ =>
  ⟨n * m, by simp [zpow_mul, h]⟩

Proof state:
α : Type u_2
f : Perm α
x y : α
n : ℤ
x✝ : (f ^ n).SameCycle x y
m : ℤ
h : ((f ^ n) ^ m) x = y
⊢ (f ^ (n * m)) x = y

Tactic:
simp [zpow_mul, h]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem preimage_sInter {f : α → β} {s : Set (Set β)} : f ⁻¹' ⋂₀ s = ⋂ t ∈ s, f ⁻¹' t

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set (Set β)
⊢ f ⁻¹' ⋂₀ s = ⋂ t ∈ s, f ⁻¹' t

Tactic:
rw [sInter_eq_biInter, preimage_iInter₂]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem infinite_of_mem_nhds {X} [TopologicalSpace X] [T1Space X] (x : X) [hx : NeBot (𝓝[≠] x)]
    {s : Set X} (hs : s ∈ 𝓝 x) : Set.Infinite s

Proof state:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ 𝓝[≠] x = ⊥

Tactic:
rw [← isOpen_singleton_iff_punctured_nhds]

Result:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ IsOpen {x}

Proof state:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ IsOpen {x}

Tactic:
exact isOpen_singleton_of_finite_mem_nhds x hs hsf

Result:
no goals

Proof state:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
⊢ s.Infinite

Tactic:
refine fun hsf => hx.1 ?_

Result:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ 𝓝[≠] x = ⊥
-- Mathlib/RingTheory/Ideal/Maximal.lean
theorem isMaximal_iff {I : Ideal α} :
    I.IsMaximal ↔ (1 : α) ∉ I ∧ ∀ (J : Ideal α) (x), I ≤ J → x ∉ I → x ∈ J → (1 : α) ∈ J

Proof state:
α : Type u
inst✝ : Semiring α
I : Ideal α
⊢ I.IsMaximal ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
simp_rw [isMaximal_def, SetLike.isCoatom_iff, Ideal.ne_top_iff_one, ← Ideal.eq_top_iff_one]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem of_eq {v' : Valuation R Γ₀} (h : v = v') : v.IsEquiv v'

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ v.IsEquiv v

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v v' : Valuation R Γ₀
h : v = v'
⊢ v.IsEquiv v'

Tactic:
subst h

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ v.IsEquiv v
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem DirectedOn.sSup_inf_eq (h : DirectedOn (· ≤ ·) s) :
    sSup s ⊓ a = ⨆ b ∈ s, b ⊓ a

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ sSup s ⊓ a = ⨆ b ∈ s, b ⊓ a

Tactic:
simp_rw [inf_comm _ a, h.inf_sSup_eq]

Result:
no goals
-- Mathlib/Analysis/Convex/Intrinsic.lean
theorem intrinsicFrontier_empty : intrinsicFrontier 𝕜 (∅ : Set P) = ∅

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
⊢ intrinsicFrontier 𝕜 ∅ = ∅

Tactic:
simp [intrinsicFrontier]

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma numeric_of_ih (ih' : ∀ a, ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) :
    (x₁ * y).Numeric ∧ (x₂ * y).Numeric

Proof state:
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
⊢ (x₁ * y).Numeric ∧ (x₂ * y).Numeric

Tactic:
constructor <;> refine ih' (Args.P1 _ _) (TransGen.single ?_)

Result:
case left
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
⊢ CutExpand IsOption (Args.P1 x₁ y).toMultiset (Args.P24 x₁ x₂ y).toMultiset

case right
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
⊢ CutExpand IsOption (Args.P1 x₂ y).toMultiset (Args.P24 x₁ x₂ y).toMultiset

Proof state:
case right
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
⊢ CutExpand IsOption (Args.P1 x₂ y).toMultiset (Args.P24 x₁ x₂ y).toMultiset

Tactic:
exact (cutExpand_add_right {x₂, y}).2 cutExpand_zero

Result:
no goals

Proof state:
case left
x₁ x₂ y : PGame
ih' : ∀ (a : Args), ArgsRel a (Args.P24 x₁ x₂ y) → P124 a
⊢ CutExpand IsOption (Args.P1 x₁ y).toMultiset (Args.P24 x₁ x₂ y).toMultiset

Tactic:
exact (cutExpand_add_right {y}).2 <| (cutExpand_add_left {x₁}).2 cutExpand_zero

Result:
no goals
-- Mathlib/Algebra/Group/Units/Hom.lean
theorem liftRight_inv_mul {f : M →* N} {g : M → Nˣ} (h : ∀ x, ↑(g x) = f x) (x) :
    ↑(liftRight f g h x)⁻¹ * f x = 1

Proof state:
M : Type u
N : Type v
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x : M
⊢ ↑((liftRight f g h) x)⁻¹ * f x = 1

Tactic:
rw [Units.inv_mul_eq_iff_eq_mul, mul_one, coe_liftRight]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma hasSum_int_evenKernel (a : ℝ) {t : ℝ} (ht : 0 < t) :
    HasSum (fun n : ℤ ↦ rexp (-π * (n + a) ^ 2 * t)) (evenKernel a t)

Proof state:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (-(↑π * (↑n + ↑a) ^ 2 * ↑t)) =
    cexp (-(↑π * ↑a ^ 2 * ↑t) + (2 * ↑π * I * ↑n * (↑a * I * ↑t) + ↑π * I * ↑n ^ 2 * (I * ↑t)))

Tactic:
ring_nf

Result:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (-(↑π * ↑n * ↑a * ↑t * 2) + (-(↑π * ↑n ^ 2 * ↑t) - ↑π * ↑a ^ 2 * ↑t)) =
    cexp (↑π * ↑n * ↑a * ↑t * I ^ 2 * 2 + (↑π * ↑n ^ 2 * ↑t * I ^ 2 - ↑π * ↑a ^ 2 * ↑t))

Proof state:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (-(↑π * (↑n + ↑a) ^ 2 * ↑t)) = cexp (-(↑π * ↑a ^ 2 * ↑t)) * jacobiTheta₂_term n (↑a * I * ↑t) (I * ↑t)

Tactic:
rw [jacobiTheta₂_term, ← Complex.exp_add]

Result:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (-(↑π * (↑n + ↑a) ^ 2 * ↑t)) =
    cexp (-(↑π * ↑a ^ 2 * ↑t) + (2 * ↑π * I * ↑n * (↑a * I * ↑t) + ↑π * I * ↑n ^ 2 * (I * ↑t)))

Proof state:
a t : ℝ
ht : 0 < t
this :
  ∀ (n : ℤ), cexp (-(↑π * (↑n + ↑a) ^ 2 * ↑t)) = cexp (-(↑π * ↑a ^ 2 * ↑t)) * jacobiTheta₂_term n (↑a * I * ↑t) (I * ↑t)
⊢ 0 < (I * ↑t).im

Tactic:
simpa

Result:
no goals

Proof state:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun x => ↑(rexp (-π * (↑x + a) ^ 2 * t))) (cexp (-↑π * ↑a ^ 2 * ↑t) * jacobiTheta₂ (↑a * I * ↑t) (I * ↑t))

Tactic:
have (n : ℤ) : cexp (-(π * (n + a) ^ 2 * t)) = cexp (-(π * a ^ 2 * t)) *
    jacobiTheta₂_term n (a * I * t) (I * t) := by
  rw [jacobiTheta₂_term, ← Complex.exp_add]
  ring_nf
  simp

Result:
a t : ℝ
ht : 0 < t
this :
  ∀ (n : ℤ), cexp (-(↑π * (↑n + ↑a) ^ 2 * ↑t)) = cexp (-(↑π * ↑a ^ 2 * ↑t)) * jacobiTheta₂_term n (↑a * I * ↑t) (I * ↑t)
⊢ HasSum (fun x => ↑(rexp (-π * (↑x + a) ^ 2 * t))) (cexp (-↑π * ↑a ^ 2 * ↑t) * jacobiTheta₂ (↑a * I * ↑t) (I * ↑t))

Proof state:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun n => rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t)

Tactic:
rw [← hasSum_ofReal, evenKernel_def]

Result:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun x => ↑(rexp (-π * (↑x + a) ^ 2 * t))) (cexp (-↑π * ↑a ^ 2 * ↑t) * jacobiTheta₂ (↑a * I * ↑t) (I * ↑t))

Proof state:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (-(↑π * ↑n * ↑a * ↑t * 2) + (-(↑π * ↑n ^ 2 * ↑t) - ↑π * ↑a ^ 2 * ↑t)) =
    cexp (↑π * ↑n * ↑a * ↑t * I ^ 2 * 2 + (↑π * ↑n ^ 2 * ↑t * I ^ 2 - ↑π * ↑a ^ 2 * ↑t))

Tactic:
simp

Result:
no goals

Proof state:
a t : ℝ
ht : 0 < t
this :
  ∀ (n : ℤ), cexp (-(↑π * (↑n + ↑a) ^ 2 * ↑t)) = cexp (-(↑π * ↑a ^ 2 * ↑t)) * jacobiTheta₂_term n (↑a * I * ↑t) (I * ↑t)
⊢ HasSum (fun x => ↑(rexp (-π * (↑x + a) ^ 2 * t))) (cexp (-↑π * ↑a ^ 2 * ↑t) * jacobiTheta₂ (↑a * I * ↑t) (I * ↑t))

Tactic:
simpa [this] using (hasSum_jacobiTheta₂_term _ (by simpa)).mul_left _

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_insert_le : (insert x s).einfsep ≤ ⨅ (y ∈ s) (_ : x ≠ y), edist x y

Proof state:
α : Type u_1
inst✝ : EDist α
x : α
s : Set α
⊢ (insert x s).einfsep ≤ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y

Tactic:
simp_rw [le_iInf_iff]

Result:
α : Type u_1
inst✝ : EDist α
x : α
s : Set α
⊢ ∀ i ∈ s, x ≠ i → (insert x s).einfsep ≤ edist x i

Proof state:
α : Type u_1
inst✝ : EDist α
x : α
s : Set α
⊢ ∀ i ∈ s, x ≠ i → (insert x s).einfsep ≤ edist x i

Tactic:
exact fun _ hy hxy => einfsep_le_edist_of_mem (mem_insert _ _) (mem_insert_of_mem _ hy) hxy

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma vanishingIdeal_mem_minimalPrimes {s : Set (PrimeSpectrum R)} :
    vanishingIdeal s ∈ minimalPrimes R ↔ closure s ∈ irreducibleComponents (PrimeSpectrum R)

Proof state:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s ∈ minimalPrimes R ↔ closure s ∈ irreducibleComponents (PrimeSpectrum R)

Tactic:
constructor

Result:
case mp
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s ∈ minimalPrimes R → closure s ∈ irreducibleComponents (PrimeSpectrum R)

case mpr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ closure s ∈ irreducibleComponents (PrimeSpectrum R) → vanishingIdeal s ∈ minimalPrimes R

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s ∈ minimalPrimes R → closure s ∈ irreducibleComponents (PrimeSpectrum R)

Tactic:
rw [← zeroLocus_minimalPrimes, ← zeroLocus_vanishingIdeal_eq_closure]

Result:
case mp
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s ∈ minimalPrimes R → zeroLocus ↑(vanishingIdeal s) ∈ zeroLocus ∘ SetLike.coe '' minimalPrimes R

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ closure s ∈ irreducibleComponents (PrimeSpectrum R) →
    vanishingIdeal (closure s) ∈ vanishingIdeal '' irreducibleComponents (PrimeSpectrum R)

Tactic:
exact Set.mem_image_of_mem _

Result:
no goals

Proof state:
case mpr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ closure s ∈ irreducibleComponents (PrimeSpectrum R) → vanishingIdeal s ∈ minimalPrimes R

Tactic:
rw [← vanishingIdeal_irreducibleComponents, ← vanishingIdeal_closure]

Result:
case mpr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ closure s ∈ irreducibleComponents (PrimeSpectrum R) →
    vanishingIdeal (closure s) ∈ vanishingIdeal '' irreducibleComponents (PrimeSpectrum R)

Proof state:
case mp
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s ∈ minimalPrimes R → zeroLocus ↑(vanishingIdeal s) ∈ zeroLocus ∘ SetLike.coe '' minimalPrimes R

Tactic:
exact Set.mem_image_of_mem _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem zeroExtend_congr (n : Nat) (w : Nat) (x x' : BitVec w) (h1 : x = x') :
    BitVec.zeroExtend n x' = BitVec.zeroExtend n x

Proof state:
n w : Nat
x x' : BitVec w
h1 : x = x'
⊢ BitVec.zeroExtend n x' = BitVec.zeroExtend n x

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem _root_.Algebra.adjoin_eq_range (s : Set S₁) :
    Algebra.adjoin R s = (MvPolynomial.aeval ((↑) : s → S₁)).range

Proof state:
R : Type u
S₁ : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
s : Set S₁
⊢ Algebra.adjoin R s = (aeval Subtype.val).range

Tactic:
rw [← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe]

Result:
no goals
-- Mathlib/Analysis/Convex/Mul.lean
lemma ConcaveOn.smul_convexOn [OrderedSMul 𝕜 E] (hf : ConcaveOn 𝕜 s f) (hg : ConvexOn 𝕜 s g)
    (hf₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ f x) (hg₀ : ∀ ⦃x⦄, x ∈ s → g x ≤ 0) (hfg : MonovaryOn f g s) :
    ConvexOn 𝕜 s (f • g)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0
hfg : MonovaryOn f g s
⊢ ConcaveOn 𝕜 s (f • -g)

Tactic:
exact hf.smul' hg.neg hf₀ (fun x hx ↦ neg_nonneg.2 <| hg₀ hx) hfg.neg_right

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0
hfg : MonovaryOn f g s
⊢ ConvexOn 𝕜 s (f • g)

Tactic:
rw [← neg_concaveOn_iff, ← smul_neg]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0
hfg : MonovaryOn f g s
⊢ ConcaveOn 𝕜 s (f • -g)
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValNat_dvd_iff (n : ℕ) [hp : Fact p.Prime] (a : ℕ) :
    p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a

Proof state:
p n : ℕ
hp : Fact (Nat.Prime p)
a : ℕ
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Result:
case inl
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ p ^ n ∣ 0 ↔ 0 = 0 ∨ n ≤ padicValNat p 0

case inr
p n : ℕ
hp : Fact (Nat.Prime p)
a : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a

Proof state:
case inl
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ p ^ n ∣ 0 ↔ 0 = 0 ∨ n ≤ padicValNat p 0

Tactic:
exact iff_of_true (dvd_zero _) (Or.inl rfl)

Result:
no goals

Proof state:
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
a : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a

Tactic:
rw [padicValNat_dvd_iff_le ha, or_iff_right ha]

Result:
no goals
-- Mathlib/Order/SuccPred/InitialSeg.lean
theorem isSuccLimit_apply_iff (f : α ≤i β) : IsSuccLimit (f a) ↔ IsSuccLimit a

Proof state:
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ IsSuccLimit (f a) ↔ IsSuccLimit a

Tactic:
simp [IsSuccLimit]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
theorem isLinearMap_smul {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] (c : R) :
    IsLinearMap R fun z : M ↦ c • z

Proof state:
R : Type u_14
M : Type u_15
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
⊢ ∀ (c_1 : R) (x : M), c • c_1 • x = c_1 • c • x

Tactic:
intro _ _

Result:
R : Type u_14
M : Type u_15
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c c✝ : R
x✝ : M
⊢ c • c✝ • x✝ = c✝ • c • x✝

Proof state:
R : Type u_14
M : Type u_15
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c c✝ : R
x✝ : M
⊢ c • c✝ • x✝ = c✝ • c • x✝

Tactic:
simp only [smul_smul, mul_comm]

Result:
no goals

Proof state:
R : Type u_14
M : Type u_15
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
⊢ IsLinearMap R fun z => c • z

Tactic:
refine IsLinearMap.mk (smul_add c) ?_

Result:
R : Type u_14
M : Type u_15
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
⊢ ∀ (c_1 : R) (x : M), c • c_1 • x = c_1 • c • x
-- Mathlib/Data/ENNReal/Inv.lean
/-- See `ENNReal.mul_inv_cancel_left'` for a stronger version. -/
protected lemma mul_inv_cancel_left (ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * (a⁻¹ * b) = b :=
  ENNReal.mul_inv_cancel_left' (by simp [ha₀]) (by simp [ha])

Proof state:
a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a = ⊤ → b = 0

Tactic:
simp [ha]

Result:
no goals

Proof state:
a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a = 0 → b = 0

Tactic:
simp [ha₀]

Result:
no goals
-- Mathlib/Analysis/Quaternion.lean
theorem normSq_eq_norm_mul_self (a : ℍ) : normSq a = ‖a‖ * ‖a‖

Proof state:
a : ℍ
⊢ normSq a = ‖a‖ * ‖a‖

Tactic:
rw [← inner_self, real_inner_self_eq_norm_mul_norm]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
theorem rTensorOne'_tmul (y : R) (m : M) :
    M.rTensorOne' (m ⊗ₜ[R] algebraMap R _ y) = y • m := Subtype.val_injective <| by
  simp_rw [rTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul]
  rw [Algebra.smul_def, Algebra.commutes]
  exact mulMap_tmul M _ _ _

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
y : R
m : ↥M
⊢ (M.mulMap (Subalgebra.toSubmodule ⊥)) (m ⊗ₜ[R] (algebraMap R ↥⊥) y) = y • ↑m

Tactic:
rw [Algebra.smul_def, Algebra.commutes]

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
y : R
m : ↥M
⊢ (M.mulMap (Subalgebra.toSubmodule ⊥)) (m ⊗ₜ[R] (algebraMap R ↥⊥) y) = ↑m * (algebraMap R S) y

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
y : R
m : ↥M
⊢ ↑(M.rTensorOne' (m ⊗ₜ[R] (algebraMap R ↥⊥) y)) = ↑(y • m)

Tactic:
simp_rw [rTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
  LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul]

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
y : R
m : ↥M
⊢ (M.mulMap (Subalgebra.toSubmodule ⊥)) (m ⊗ₜ[R] (algebraMap R ↥⊥) y) = y • ↑m

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M : Submodule R S
y : R
m : ↥M
⊢ (M.mulMap (Subalgebra.toSubmodule ⊥)) (m ⊗ₜ[R] (algebraMap R ↥⊥) y) = ↑m * (algebraMap R S) y

Tactic:
exact mulMap_tmul M _ _ _

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_equiv_eq_zero_iff_ne : #(α ≃ β) = 0 ↔ #α ≠ #β

Proof state:
α β : Type u
⊢ #(α ≃ β) = 0 ↔ #α ≠ #β

Tactic:
rw [mk_equiv_eq_zero_iff_lift_ne, lift_id, lift_id]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem join_ret (s : WSeq α) : join (ret s) ~ʷ s

Proof state:
α : Type u
s : WSeq α
⊢ (ret s).join ~ʷ s

Tactic:
simpa [ret] using think_equiv _

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.pre_eq (s : ColimitCocone (E ⋙ F)) (t : ColimitCocone F) :
    colimit.pre F E =
      (colimit.isoColimitCocone s).hom ≫
        s.isColimit.desc (t.cocone.whisker E) ≫ (colimit.isoColimitCocone t).inv

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
s : ColimitCocone (E ⋙ F)
t : ColimitCocone F
⊢ pre F E = (isoColimitCocone s).hom ≫ s.isColimit.desc (Cocone.whisker E t.cocone) ≫ (isoColimitCocone t).inv

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
@[simp]
lemma changeLevel_self : changeLevel (dvd_refl n) χ = χ

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ (changeLevel ⋯) χ = χ

Tactic:
simp [changeLevel, ZMod.unitsMap]

Result:
no goals
-- Mathlib/LinearAlgebra/SModEq.lean
theorem zero : x ≡ 0 [SMOD U] ↔ x ∈ U

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Submodule R M
x : M
⊢ x ≡ 0 [SMOD U] ↔ x ∈ U

Tactic:
rw [SModEq.def, Submodule.Quotient.eq, sub_zero]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma bot_mul_of_neg {x : EReal} (h : x < 0) : ⊥ * x = ⊤

Proof state:
x : EReal
h : x < 0
⊢ ⊥ * x = ⊤

Tactic:
rw [EReal.mul_comm]

Result:
x : EReal
h : x < 0
⊢ x * ⊥ = ⊤

Proof state:
x : EReal
h : x < 0
⊢ x * ⊥ = ⊤

Tactic:
exact mul_bot_of_neg h

Result:
no goals
-- Mathlib/Topology/Category/CompHausLike/Basic.lean
theorem epi_of_surjective {X Y : CompHausLike.{u} P} (f : X ⟶ Y) (hf : Function.Surjective f) :
    Epi f

Proof state:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ Epi f

Tactic:
rw [← CategoryTheory.epi_iff_surjective] at hf

Result:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Epi ⇑(ConcreteCategory.hom f)
⊢ Epi f

Proof state:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Epi ⇑(ConcreteCategory.hom f)
⊢ Epi f

Tactic:
exact (forget (CompHausLike P)).epi_of_epi_map hf

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma lift_f_snd_v (p q : ℤ) (hpq : p + 0 = q) :
    (lift φ α β eq).f p ≫ (snd φ).v p q hpq = β.v p q hpq

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
q : ℤ
hpq : q + 0 = q
⊢ (lift φ α β eq).f q ≫ (snd φ).v q q hpq = β.v q q hpq

Tactic:
simp [lift]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 0 = q
⊢ (lift φ α β eq).f p ≫ (snd φ).v p q hpq = β.v p q hpq

Tactic:
obtain rfl : q = p := by omega

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
q : ℤ
hpq : q + 0 = q
⊢ (lift φ α β eq).f q ≫ (snd φ).v q q hpq = β.v q q hpq

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 0 = q
⊢ q = p

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem acc_iff_cluster (x : X) (F : Filter X) : AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)

Tactic:
rw [AccPt, nhdsWithin, ClusterPt, inf_assoc]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem bddAbove_range_comp {ι : Type u} {f : ι → Cardinal.{v}} (hf : BddAbove (range f))
    (g : Cardinal.{v} → Cardinal.{max v w}) : BddAbove (range (g ∘ f))

Proof state:
ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (g '' range f)

Tactic:
exact bddAbove_image g hf

Result:
no goals

Proof state:
ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (range (g ∘ f))

Tactic:
rw [range_comp]

Result:
ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (g '' range f)
-- Mathlib/Algebra/Order/Ring/Basic.lean
theorem map_sub_swap (x y : R) : f (x - y) = f (y - x)

Proof state:
M : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : MulLeftMono M
f : R →* M
x y : R
⊢ f (x - y) = f (y - x)

Tactic:
rw [← map_neg, neg_sub]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem empty_eq {xs : Vector α 0} : #v[] = xs ↔ xs = #v[]

Proof state:
α : Type u_1
xs : Vector α 0
⊢ { toArray := #[], size_toArray := ⋯ } = xs ↔ xs = { toArray := #[], size_toArray := ⋯ }

Tactic:
cases xs

Result:
case mk
α : Type u_1
toArray✝ : Array α
size_toArray✝ : toArray✝.size = 0
⊢ { toArray := #[], size_toArray := ⋯ } = { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } = { toArray := #[], size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
toArray✝ : Array α
size_toArray✝ : toArray✝.size = 0
⊢ { toArray := #[], size_toArray := ⋯ } = { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } = { toArray := #[], size_toArray := ⋯ }

Tactic:
simp

Result:
no goals