harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Separable.lean
theorem separable_prod_X_sub_C_iff' {ι : Sort _} {f : ι → F} {s : Finset ι} :
    (∏ i ∈ s, (X - C (f i))).Separable ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y :=
  ⟨fun hfs _ hx _ hy hfxy => hfs.inj_of_prod_X_sub_C hx hy hfxy, fun H => by
    rw [← prod_attach]
    exact
      separable_prod'
        (fun x _hx y _hy hxy =>
          @pairwise_coprime_X_sub_C _ _ { x // x ∈ s } (fun x => f x)
            (fun x y hxy => Subtype.eq <| H x.1 x.2 y.1 y.2 hxy) _ _ hxy)
        fun _ _ => separable_X_sub_C⟩

Proof state:
F : Type u
inst✝ : Field F
ι : Type u_1
f : ι → F
s : Finset ι
H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
⊢ (∏ i ∈ s, (X - C (f i))).Separable

Tactic:
rw [← prod_attach]

Result:
F : Type u
inst✝ : Field F
ι : Type u_1
f : ι → F
s : Finset ι
H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
⊢ (∏ x ∈ s.attach, (X - C (f ↑x))).Separable

Proof state:
F : Type u
inst✝ : Field F
ι : Type u_1
f : ι → F
s : Finset ι
H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
⊢ (∏ x ∈ s.attach, (X - C (f ↑x))).Separable

Tactic:
exact
  separable_prod'
    (fun x _hx y _hy hxy =>
      @pairwise_coprime_X_sub_C _ _ { x // x ∈ s } (fun x => f x)
        (fun x y hxy => Subtype.eq <| H x.1 x.2 y.1 y.2 hxy) _ _ hxy)
    fun _ _ => separable_X_sub_C

Result:
no goals
-- Mathlib/Analysis/Complex/Periodic.lean
theorem eq_cuspFunction (hh : h ≠ 0) (hf : Periodic f h) (z : ℂ) :
    (cuspFunction h f) (𝕢 h z) = f z

Proof state:
case intro
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
this : cuspFunction h f (𝕢 h z) = f (invQParam h (𝕢 h z))
m : ℤ
hm : invQParam h (𝕢 h z) = z + ↑m * ↑h
⊢ cuspFunction h f (𝕢 h z) = f z

Tactic:
simpa only [this, hm] using hf.int_mul m z

Result:
no goals

Proof state:
case h
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
⊢ 𝕢 h z ≠ 0

Tactic:
exact exp_ne_zero _

Result:
no goals

Proof state:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
⊢ cuspFunction h f (𝕢 h z) = f z

Tactic:
have : (cuspFunction h f) (𝕢 h z) = f (invQParam h (𝕢 h z)) := by
  rw [cuspFunction, update_of_ne, comp_apply]
  exact exp_ne_zero _

Result:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
this : cuspFunction h f (𝕢 h z) = f (invQParam h (𝕢 h z))
⊢ cuspFunction h f (𝕢 h z) = f z

Proof state:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
⊢ cuspFunction h f (𝕢 h z) = f (invQParam h (𝕢 h z))

Tactic:
rw [cuspFunction, update_of_ne, comp_apply]

Result:
case h
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
⊢ 𝕢 h z ≠ 0

Proof state:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
this : cuspFunction h f (𝕢 h z) = f (invQParam h (𝕢 h z))
⊢ cuspFunction h f (𝕢 h z) = f z

Tactic:
obtain ⟨m, hm⟩ := qParam_left_inv_mod_period hh z

Result:
case intro
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
this : cuspFunction h f (𝕢 h z) = f (invQParam h (𝕢 h z))
m : ℤ
hm : invQParam h (𝕢 h z) = z + ↑m * ↑h
⊢ cuspFunction h f (𝕢 h z) = f z
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
lemma degrees_map_le [CommSemiring S] {f : R →+* S} : (map f p).degrees ≤ p.degrees

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
⊢ ((map f) p).degrees ≤ p.degrees

Tactic:
exact Finset.sup_mono <| support_map_subset ..

Result:
no goals

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
⊢ ((map f) p).degrees ≤ p.degrees

Tactic:
classical exact Finset.sup_mono <| support_map_subset ..

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem add_one_le_iff_of_not_isMax (hx : ¬ IsMax x) : x + 1 ≤ y ↔ x < y

Proof state:
α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hx : ¬IsMax x
⊢ x + 1 ≤ y ↔ x < y

Tactic:
rw [← succ_eq_add_one, succ_le_iff_of_not_isMax hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_eq_getEntry? [BEq α] {l : List ((_ : α) × β)} {a : α} :
    getValue? a l = (getEntry? a l).map (·.2)

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
a : α
⊢ getValue? a l = Option.map (fun x => x.snd) (getEntry? a l)

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : Type v
inst✝ : BEq α
a : α
⊢ getValue? a [] = Option.map (fun x => x.snd) (getEntry? a [])

case cons
α : Type u
β : Type v
inst✝ : BEq α
a k✝ : α
v✝ : β
tail✝ : List ((_ : α) × β)
a✝ : getValue? a tail✝ = Option.map (fun x => x.snd) (getEntry? a tail✝)
⊢ getValue? a (⟨k✝, v✝⟩ :: tail✝) = Option.map (fun x => x.snd) (getEntry? a (⟨k✝, v✝⟩ :: tail✝))

Proof state:
case true
α : Type u
β : Type v
inst✝ : BEq α
a k : α
v : β
l : List ((_ : α) × β)
ih : getValue? a l = Option.map (fun x => x.snd) (getEntry? a l)
h : (k == a) = true
⊢ getValue? a (⟨k, v⟩ :: l) = Option.map (fun x => x.snd) (getEntry? a (⟨k, v⟩ :: l))

Tactic:
rw [getEntry?_cons_of_true h, getValue?_cons_of_true h, Option.map_some']

Result:
no goals

Proof state:
case false
α : Type u
β : Type v
inst✝ : BEq α
a k : α
v : β
l : List ((_ : α) × β)
ih : getValue? a l = Option.map (fun x => x.snd) (getEntry? a l)
h : (k == a) = false
⊢ getValue? a (⟨k, v⟩ :: l) = Option.map (fun x => x.snd) (getEntry? a (⟨k, v⟩ :: l))

Tactic:
rw [getEntry?_cons_of_false h, getValue?_cons_of_false h, ih]

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
inst✝ : BEq α
a : α
⊢ getValue? a [] = Option.map (fun x => x.snd) (getEntry? a [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
a k : α
v : β
l : List ((_ : α) × β)
ih : getValue? a l = Option.map (fun x => x.snd) (getEntry? a l)
⊢ getValue? a (⟨k, v⟩ :: l) = Option.map (fun x => x.snd) (getEntry? a (⟨k, v⟩ :: l))

Tactic:
cases h : k == a

Result:
case false
α : Type u
β : Type v
inst✝ : BEq α
a k : α
v : β
l : List ((_ : α) × β)
ih : getValue? a l = Option.map (fun x => x.snd) (getEntry? a l)
h : (k == a) = false
⊢ getValue? a (⟨k, v⟩ :: l) = Option.map (fun x => x.snd) (getEntry? a (⟨k, v⟩ :: l))

case true
α : Type u
β : Type v
inst✝ : BEq α
a k : α
v : β
l : List ((_ : α) × β)
ih : getValue? a l = Option.map (fun x => x.snd) (getEntry? a l)
h : (k == a) = true
⊢ getValue? a (⟨k, v⟩ :: l) = Option.map (fun x => x.snd) (getEntry? a (⟨k, v⟩ :: l))
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem dist_eq_iff_eq_sinh :
    dist z w = r ↔ dist (z : ℂ) w / (2 * √(z.im * w.im)) = sinh (r / 2)

Proof state:
z w : ℍ
r : ℝ
⊢ dist z w = r ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) = sinh (r / 2)

Tactic:
rw [← div_left_inj' (two_ne_zero' ℝ), ← sinh_inj, sinh_half_dist]

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftPropOn_of_liftProp (mono : ∀ ⦃s x t⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x)
    (h : LiftProp P g) : LiftPropOn P g s

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropOn P g univ
⊢ LiftPropOn P g s

Tactic:
exact liftPropOn_mono mono h (subset_univ _)

Result:
no goals

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftProp P g
⊢ LiftPropOn P g s

Tactic:
rw [← liftPropOn_univ] at h

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
P : (H → H') → Set H → H → Prop
g : M → M'
s : Set M
mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x
h : LiftPropOn P g univ
⊢ LiftPropOn P g s
-- Mathlib/Computability/Primrec.lean
theorem of_graph {f : α → ℕ} (h₁ : PrimrecBounded f)
    (h₂ : PrimrecRel fun a b => f a = b) : Primrec f

Proof state:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → ℕ
h₂ : PrimrecRel fun a b => f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
n : α
⊢ Nat.findGreatest (fun b => f n = b) (g n) = f n

Tactic:
exact (Nat.findGreatest_spec (P := fun b => f n = b) (hg n) rfl).symm

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → ℕ
h₂ : PrimrecRel fun a b => f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
⊢ Primrec f

Tactic:
refine (nat_findGreatest pg h₂).of_eq fun n => ?_

Result:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → ℕ
h₂ : PrimrecRel fun a b => f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
n : α
⊢ Nat.findGreatest (fun b => f n = b) (g n) = f n

Proof state:
α : Type u_1
inst✝ : Primcodable α
f : α → ℕ
h₁ : PrimrecBounded f
h₂ : PrimrecRel fun a b => f a = b
⊢ Primrec f

Tactic:
rcases h₁ with ⟨g, pg, hg : ∀ x, f x ≤ g x⟩

Result:
case intro.intro
α : Type u_1
inst✝ : Primcodable α
f : α → ℕ
h₂ : PrimrecRel fun a b => f a = b
g : α → ℕ
pg : Primrec g
hg : ∀ (x : α), f x ≤ g x
⊢ Primrec f
-- Mathlib/Deprecated/Cardinal/PartENat.lean
theorem toPartENat_eq_top {c : Cardinal} :
    toPartENat c = ⊤ ↔ ℵ₀ ≤ c

Proof state:
c : Cardinal.{u_1}
⊢ ↑(toENat c) = PartENat.withTopEquiv.symm ⊤ ↔ PartENat.withTopEquiv.symm (toENat c) = PartENat.withTopEquiv.symm ⊤

Tactic:
simp

Result:
no goals

Proof state:
c : Cardinal.{u_1}
⊢ toPartENat c = ⊤ ↔ ℵ₀ ≤ c

Tactic:
rw [← partENatOfENat_toENat, ← PartENat.withTopEquiv_symm_top, ← toENat_eq_top,
  ← PartENat.withTopEquiv.symm.injective.eq_iff]

Result:
c : Cardinal.{u_1}
⊢ ↑(toENat c) = PartENat.withTopEquiv.symm ⊤ ↔ PartENat.withTopEquiv.symm (toENat c) = PartENat.withTopEquiv.symm ⊤
-- Mathlib/RingTheory/Generators.lean
@[simp]
lemma Hom.toExtensionHom_id : Hom.toExtensionHom (.id P) = .id _

Proof state:
case toRingHom.a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
x✝ : P.toExtension.Ring
⊢ (Hom.id P).toExtensionHom.toRingHom x✝ = (Extension.Hom.id P.toExtension).toRingHom x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
⊢ (Hom.id P).toExtensionHom = Extension.Hom.id P.toExtension

Tactic:
ext

Result:
case toRingHom.a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
x✝ : P.toExtension.Ring
⊢ (Hom.id P).toExtensionHom.toRingHom x✝ = (Extension.Hom.id P.toExtension).toRingHom x✝
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem iSup_restrict_spanningSets [SigmaFinite μ] (s : Set α) :
    ⨆ i, μ.restrict (spanningSets μ i) s = μ s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ ⨆ i, (μ.restrict (spanningSets μ i)) s = ⨆ i, (μ.restrict (spanningSets μ i)) (toMeasurable μ s)

Tactic:
simp_rw [restrict_apply' (measurableSet_spanningSets μ _), Set.inter_comm s,
  ← restrict_apply (measurableSet_spanningSets μ _), ← restrict_toMeasurable_of_sFinite s,
  restrict_apply (measurableSet_spanningSets μ _), Set.inter_comm _ (toMeasurable μ s)]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ ⨆ i, (μ.restrict (spanningSets μ i)) s = μ s

Tactic:
rw [← measure_toMeasurable s,
  ← iSup_restrict_spanningSets_of_measurableSet (measurableSet_toMeasurable _ _)]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
⊢ ⨆ i, (μ.restrict (spanningSets μ i)) s = ⨆ i, (μ.restrict (spanningSets μ i)) (toMeasurable μ s)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_false : (countP fun (_ : α) => false) = Function.const _ 0

Proof state:
case h
α : Type u_1
l : List α
⊢ countP (fun x => false) l = Function.const (List α) 0 l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
⊢ (countP fun x => false) = Function.const (List α) 0

Tactic:
funext l

Result:
case h
α : Type u_1
l : List α
⊢ countP (fun x => false) l = Function.const (List α) 0 l
-- Mathlib/RingTheory/Flat/Basic.lean
/--
Define the character module of `M` to be `M →+ ℚ ⧸ ℤ`.
The character module of `M` is an injective module if and only if
 `f ⊗ 𝟙 M` is injective for any linear map `f` in the same universe as `M`.
-/
lemma injective_characterModule_iff_rTensor_preserves_injective_linearMap :
    Module.Injective R (CharacterModule M) ↔
    ∀ ⦃N N' : Type v⦄ [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N']
      (f : N →ₗ[R] N'), Function.Injective f → Function.Injective (f.rTensor M)

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ ⦃X Y : Type v⦄ [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] [inst_2 : Module R X] [inst_3 : Module R Y]
      (f : X →ₗ[R] Y),
      Function.Injective ⇑f → ∀ (g : X →ₗ[R] CharacterModule M), ∃ h, ∀ (x : X) (x_1 : M), (h (f x)) x_1 = (g x) x_1) ↔
    ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'),
      Function.Injective ⇑f →
        ∀ (b : N →ₗ[R] CharacterModule M),
          ∃ a, ∀ (x : N) (x_1 : M), (((lcomp R (CharacterModule M) f) a) x) x_1 = (b x) x_1

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Injective R (CharacterModule M) ↔
    ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(rTensor M f)

Tactic:
simp_rw [injective_iff, rTensor_injective_iff_lcomp_surjective, Surjective, DFunLike.ext_iff]

Result:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ ⦃X Y : Type v⦄ [inst : AddCommGroup X] [inst_1 : AddCommGroup Y] [inst_2 : Module R X] [inst_3 : Module R Y]
      (f : X →ₗ[R] Y),
      Function.Injective ⇑f → ∀ (g : X →ₗ[R] CharacterModule M), ∃ h, ∀ (x : X) (x_1 : M), (h (f x)) x_1 = (g x) x_1) ↔
    ∀ ⦃N N' : Type v⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
      (f : N →ₗ[R] N'),
      Function.Injective ⇑f →
        ∀ (b : N →ₗ[R] CharacterModule M),
          ∃ a, ∀ (x : N) (x_1 : M), (((lcomp R (CharacterModule M) f) a) x) x_1 = (b x) x_1
-- Mathlib/Algebra/Star/Conjneg.lean
@[simp] lemma support_conjneg (f : G → R) : support (conjneg f) = -support f

Proof state:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
x✝ : G
⊢ x✝ ∈ support (conjneg f) ↔ x✝ ∈ -support f

Tactic:
simp [starRingEnd_apply]

Result:
no goals

Proof state:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
⊢ support (conjneg f) = -support f

Tactic:
ext

Result:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
x✝ : G
⊢ x✝ ∈ support (conjneg f) ↔ x✝ ∈ -support f
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_rpow_const (x : ℝ) (q : ℝ) (h : x ≠ 0 ∨ 0 ≤ q) :
    ContinuousAt (fun x : ℝ => x ^ q) x

Proof state:
x q : ℝ
h : (x ≠ 0 ∨ 0 < q) ∨ 0 = q
⊢ ContinuousAt (fun x => x ^ q) x

Tactic:
obtain h|rfl := h

Result:
case inl
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun x => x ^ q) x

case inr
x : ℝ
⊢ ContinuousAt (fun x => x ^ 0) x

Proof state:
case inr
x : ℝ
⊢ ContinuousAt (fun x => x ^ 0) x

Tactic:
simp_rw [rpow_zero]

Result:
case inr
x : ℝ
⊢ ContinuousAt (fun x => 1) x

Proof state:
x q : ℝ
h : x ≠ 0 ∨ 0 ≤ q
⊢ ContinuousAt (fun x => x ^ q) x

Tactic:
rw [le_iff_lt_or_eq, ← or_assoc] at h

Result:
x q : ℝ
h : (x ≠ 0 ∨ 0 < q) ∨ 0 = q
⊢ ContinuousAt (fun x => x ^ q) x

Proof state:
case inl
x q : ℝ
h : x ≠ 0 ∨ 0 < q
⊢ ContinuousAt (fun x => x ^ q) x

Tactic:
exact (continuousAt_rpow (x, q) h).comp₂ continuousAt_id continuousAt_const

Result:
no goals

Proof state:
case inr
x : ℝ
⊢ ContinuousAt (fun x => 1) x

Tactic:
exact continuousAt_const

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iUnion_Iic_of_not_bddAbove_range (hf : ¬ BddAbove (range f)) : ⋃ i, Iic (f i) = univ

Proof state:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
⊢ ⋃ i, Iic (f i) = univ

Tactic:
refine  Set.eq_univ_of_subset ?_ (iUnion_Iio_eq_univ_iff.mpr hf)

Result:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
⊢ ⋃ i, Iio (f i) ⊆ ⋃ i, Iic (f i)

Proof state:
case h
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
i✝ : ι
⊢ Iio (f i✝) ⊆ Iic (f i✝)

Tactic:
exact Iio_subset_Iic_self

Result:
no goals

Proof state:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
⊢ ⋃ i, Iio (f i) ⊆ ⋃ i, Iic (f i)

Tactic:
gcongr

Result:
case h
ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
hf : ¬BddAbove (range f)
i✝ : ι
⊢ Iio (f i✝) ⊆ Iic (f i✝)
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.left_ne_right_of_ne_right {x y z : P} (h : Wbtw R x y z) (hne : y ≠ z) : x ≠ z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : Wbtw R x y x
hne : y ≠ x
⊢ False

Tactic:
rw [wbtw_self_iff] at h

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : y = x
hne : y ≠ x
⊢ False

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
h : Wbtw R x y z
hne : y ≠ z
⊢ x ≠ z

Tactic:
rintro rfl

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : Wbtw R x y x
hne : y ≠ x
⊢ False

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
h : y = x
hne : y ≠ x
⊢ False

Tactic:
exact hne h

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/End.lean
lemma commute_id_right : Commute f LinearMap.id

Proof state:
R : Type u_9
M : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ Commute f LinearMap.id

Tactic:
ext

Result:
case h
R : Type u_9
M : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
x✝ : M
⊢ (f * LinearMap.id) x✝ = (LinearMap.id * f) x✝

Proof state:
case h
R : Type u_9
M : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
x✝ : M
⊢ (f * LinearMap.id) x✝ = (LinearMap.id * f) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem conj_eq_iff_real {z : K} : conj z = z ↔ ∃ r : ℝ, z = (r : K) :=
  calc
    _ ↔ ∃ r : ℝ, (r : K) = z := (is_real_TFAE z).out 0 1
    _ ↔ _

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (∃ r, ↑r = z) ↔ ∃ r, z = ↑r

Tactic:
simp only [eq_comm]

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem of_surjective (hRA : FiniteType R A) (f : A →ₐ[R] B) (hf : Surjective f) : FiniteType R B :=
  ⟨by
    convert hRA.1.map f
    simpa only [map_top f, @eq_comm _ ⊤, eq_top_iff, AlgHom.mem_range] using hf⟩

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
hRA : FiniteType R A
f : A →ₐ[R] B
hf : Surjective ⇑f
⊢ ⊤.FG

Tactic:
convert hRA.1.map f

Result:
case h.e'_6
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
hRA : FiniteType R A
f : A →ₐ[R] B
hf : Surjective ⇑f
⊢ ⊤ = Subalgebra.map f ⊤

Proof state:
case h.e'_6
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
hRA : FiniteType R A
f : A →ₐ[R] B
hf : Surjective ⇑f
⊢ ⊤ = Subalgebra.map f ⊤

Tactic:
simpa only [map_top f, @eq_comm _ ⊤, eq_top_iff, AlgHom.mem_range] using hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_push (a : α) (l) : countP p (l.push a) = countP p l + if p a then 1 else 0

Proof state:
α : Type u_1
p : α → Bool
a : α
l : Array α
⊢ countP p (l.push a) = countP p l + if p a = true then 1 else 0

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ countP p ({ toList := l }.push a) = countP p { toList := l } + if p a = true then 1 else 0

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ countP p ({ toList := l }.push a) = countP p { toList := l } + if p a = true then 1 else 0

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/CharP/Basic.lean
lemma intCast_injOn_Ico [IsRightCancelAdd R] : InjOn (Int.cast : ℤ → R) (Ico 0 p)

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
a b : ℕ
ha : a < p
hb : b < p
hab : ↑a = ↑b
⊢ a = b

Tactic:
exact natCast_injOn_Iio _ _ ha hb hab

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
b : ℤ
hb₀ : 0 ≤ b
hb : b < ↑p
a : ℕ
ha : ↑a < ↑p
hab : ↑↑a = ↑b
⊢ ↑a = b

Tactic:
lift b to ℕ using hb₀

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
a : ℕ
ha : ↑a < ↑p
b : ℕ
hb : ↑b < ↑p
hab : ↑↑a = ↑↑b
⊢ ↑a = ↑b

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
a : ℕ
ha : ↑a < ↑p
b : ℕ
hb : ↑b < ↑p
hab : ↑↑a = ↑↑b
⊢ ↑a = ↑b

Tactic:
norm_cast at *

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
a b : ℕ
ha : a < p
hb : b < p
hab : ↑a = ↑b
⊢ a = b

Proof state:
case intro.intro
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
a : ℤ
ha₀ : 0 ≤ a
ha : a < ↑p
b : ℤ
hb₀ : 0 ≤ b
hb : b < ↑p
hab : ↑a = ↑b
⊢ a = b

Tactic:
lift a to ℕ using ha₀

Result:
case intro.intro.intro
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
b : ℤ
hb₀ : 0 ≤ b
hb : b < ↑p
a : ℕ
ha : ↑a < ↑p
hab : ↑↑a = ↑b
⊢ ↑a = b

Proof state:
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
⊢ InjOn Int.cast (Ico 0 ↑p)

Tactic:
rintro a ⟨ha₀, ha⟩ b ⟨hb₀, hb⟩ hab

Result:
case intro.intro
R : Type u_1
inst✝² : AddGroupWithOne R
p : ℕ
inst✝¹ : CharP R p
inst✝ : IsRightCancelAdd R
a : ℤ
ha₀ : 0 ≤ a
ha : a < ↑p
b : ℤ
hb₀ : 0 ≤ b
hb : b < ↑p
hab : ↑a = ↑b
⊢ a = b