harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.inner_left_finsupp {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι →₀ 𝕜) (i : ι) :
    ⟪linearCombination 𝕜 v l, v i⟫ = conj (l i)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
i : ι
⊢ inner ((linearCombination 𝕜 v) l) (v i) = (starRingEnd 𝕜) (l i)

Tactic:
rw [← inner_conj_symm, hv.inner_right_finsupp]

Result:
no goals
-- Mathlib/Order/Hom/Bounded.lean
theorem cancel_left {g : BoundedOrderHom β γ} {f₁ f₂ : BoundedOrderHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h =>
    BoundedOrderHom.ext fun a =>
      hg <| by rw [← BoundedOrderHom.comp_apply, h, BoundedOrderHom.comp_apply],
    congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

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

Result:
no goals
-- Mathlib/FieldTheory/IsSepClosed.lean
theorem exists_eval₂_eq_zero [IsSepClosed K] (f : k →+* K)
    (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.Separable) :
    ∃ x, p.eval₂ f x = 0 :=
  let ⟨x, hx⟩ := exists_root (p.map f) (by rwa [degree_map_eq_of_injective f.injective])
    (Separable.map hsep)
  ⟨x, by rwa [eval₂_eq_eval_map, ← IsRoot]⟩

Proof state:
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed K
f : k →+* K
p : k[X]
hp : p.degree ≠ 0
hsep : p.Separable
x : K
hx : (map f p).IsRoot x
⊢ eval₂ f x p = 0

Tactic:
rwa [eval₂_eq_eval_map, ← IsRoot]

Result:
no goals

Proof state:
k : Type u
inst✝² : Field k
K : Type v
inst✝¹ : Field K
inst✝ : IsSepClosed K
f : k →+* K
p : k[X]
hp : p.degree ≠ 0
hsep : p.Separable
⊢ (map f p).degree ≠ 0

Tactic:
rwa [degree_map_eq_of_injective f.injective]

Result:
no goals
-- Mathlib/Data/Finset/Sigma.lean
theorem mk_mem_sigmaLift (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (i : ι) (a : α i) (b : β i)
    (x : γ i) : (⟨i, x⟩ : Sigma γ) ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔ x ∈ f a b

Proof state:
case intro.intro.refl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
hx : x ∈ f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd
⊢ x ∈ f a b

Tactic:
exact hx

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ (∃ a_1 ∈ f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd, (Embedding.sigmaMk ⟨i, b⟩.fst) a_1 = ⟨i, x⟩) ↔ x ∈ f a b

Tactic:
refine ⟨?_, fun hx => ⟨_, hx, rfl⟩⟩

Result:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ (∃ a_1 ∈ f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd, (Embedding.sigmaMk ⟨i, b⟩.fst) a_1 = ⟨i, x⟩) → x ∈ f a b

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ (∃ a_1 ∈ f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd, (Embedding.sigmaMk ⟨i, b⟩.fst) a_1 = ⟨i, x⟩) → x ∈ f a b

Tactic:
rintro ⟨x, hx, _, rfl⟩

Result:
case intro.intro.refl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
hx : x ∈ f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd
⊢ x ∈ f a b

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ ⟨i, x⟩ ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔ x ∈ f a b

Tactic:
rw [sigmaLift, dif_pos rfl, mem_map]

Result:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ (∃ a_1 ∈ f (⋯ ▸ ⟨i, a⟩.snd) ⟨i, b⟩.snd, (Embedding.sigmaMk ⟨i, b⟩.fst) a_1 = ⟨i, x⟩) ↔ x ∈ f a b
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_le_pow_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : 1 ≤ a ^ n ↔ 1 ≤ a

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : LinearOrder M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
a : M₀
n : ℕ
ha : 0 ≤ a
hn : n ≠ 0
⊢ 1 ≤ a ^ n ↔ 1 ≤ a

Tactic:
simpa only [one_pow] using pow_le_pow_iff_left₀ zero_le_one ha hn

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Cast.lean
lemma cast_le_neg_one_of_neg (h : a < 0) : (a : R) ≤ -1

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℤ
h : a < 0
⊢ a ≤ -1

Tactic:
exact Int.le_sub_one_of_lt h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℤ
h : a < 0
⊢ ↑a ≤ -1

Tactic:
rw [← Int.cast_one, ← Int.cast_neg, cast_le]

Result:
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℤ
h : a < 0
⊢ a ≤ -1
-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem eventually_filterAt_integrableOn (x : α) {f : α → E} (hf : LocallyIntegrable f μ) :
    ∀ᶠ a in v.filterAt x, IntegrableOn f a μ

Proof state:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝ : NormedAddCommGroup E
x : α
f : α → E
hf : LocallyIntegrable f μ
⊢ ∀ᶠ (a : Set α) in v.filterAt x, IntegrableOn f a μ

Tactic:
rcases hf x with ⟨w, w_nhds, hw⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝ : NormedAddCommGroup E
x : α
f : α → E
hf : LocallyIntegrable f μ
w : Set α
w_nhds : w ∈ 𝓝 x
hw : IntegrableOn f w μ
⊢ ∀ᶠ (a : Set α) in v.filterAt x, IntegrableOn f a μ

Proof state:
case h
α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝ : NormedAddCommGroup E
x : α
f : α → E
hf : LocallyIntegrable f μ
w : Set α
w_nhds : w ∈ 𝓝 x
hw : IntegrableOn f w μ
a : Set α
ha : a ⊆ w
⊢ IntegrableOn f a μ

Tactic:
exact hw.mono_set ha

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝ : NormedAddCommGroup E
x : α
f : α → E
hf : LocallyIntegrable f μ
w : Set α
w_nhds : w ∈ 𝓝 x
hw : IntegrableOn f w μ
⊢ ∀ᶠ (a : Set α) in v.filterAt x, IntegrableOn f a μ

Tactic:
filter_upwards [v.eventually_filterAt_subset_of_nhds w_nhds] with a ha

Result:
case h
α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
E : Type u_2
inst✝ : NormedAddCommGroup E
x : α
f : α → E
hf : LocallyIntegrable f μ
w : Set α
w_nhds : w ∈ 𝓝 x
hw : IntegrableOn f w μ
a : Set α
ha : a ⊆ w
⊢ IntegrableOn f a μ
-- Mathlib/Tactic/NormNum/Eq.lean
theorem Rat.invOf_denom_swap [Ring α] (n₁ n₂ : ℤ) (a₁ a₂ : α)
    [Invertible a₁] [Invertible a₂] : n₁ * ⅟a₁ = n₂ * ⅟a₂ ↔ n₁ * a₂ = n₂ * a₁

Proof state:
α : Type u_1
inst✝² : Ring α
n₁ n₂ : ℤ
a₁ a₂ : α
inst✝¹ : Invertible a₁
inst✝ : Invertible a₂
⊢ ↑n₁ * ⅟a₁ = ↑n₂ * ⅟a₂ ↔ ↑n₁ * a₂ = ↑n₂ * a₁

Tactic:
rw [mul_invOf_eq_iff_eq_mul_right, ← Int.commute_cast, mul_assoc,
  ← mul_left_eq_iff_eq_invOf_mul, Int.commute_cast]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
lemma Topology.IsInducing.generalizingMap (hf : IsInducing f)
    (h : StableUnderGeneralization (range f)) : GeneralizingMap f

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (Set.range f)
⊢ GeneralizingMap f

Tactic:
intros x y e

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (Set.range f)
x : X
y : Y
e : y ⤳ f x
⊢ ∃ a', (fun x1 x2 => x1 ⤳ x2) a' x ∧ f a' = y

Proof state:
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (Set.range f)
x y : X
e : f y ⤳ f x
⊢ ∃ a', (fun x1 x2 => x1 ⤳ x2) a' x ∧ f a' = f y

Tactic:
exact ⟨_, hf.specializes_iff.mp e, rfl⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (Set.range f)
x : X
y : Y
e : y ⤳ f x
⊢ ∃ a', (fun x1 x2 => x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
obtain ⟨y, rfl⟩ := h e ⟨x, rfl⟩

Result:
case intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (Set.range f)
x y : X
e : f y ⤳ f x
⊢ ∃ a', (fun x1 x2 => x1 ⤳ x2) a' x ∧ f a' = f y
-- Mathlib/Data/Fintype/Order.lean
theorem Finite.bddBelow_range [IsDirected α (· ≥ ·)] (f : β → α) : BddBelow (Set.range f)

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝³ : Finite β
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≥ x2
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
a : α
ha : a ∈ Set.range f
⊢ M ≤ a

Tactic:
obtain ⟨b, rfl⟩ := ha

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Finite β
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≥ x2
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
b : β
⊢ M ≤ f b

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝³ : Finite β
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≥ x2
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
⊢ BddBelow (Set.range f)

Tactic:
refine ⟨M, fun a ha => ?_⟩

Result:
case intro
α : Type u_1
β : Type u_2
inst✝³ : Finite β
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≥ x2
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
a : α
ha : a ∈ Set.range f
⊢ M ≤ a

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Finite β
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≥ x2
f : β → α
⊢ BddBelow (Set.range f)

Tactic:
obtain ⟨M, hM⟩ := Finite.exists_ge f

Result:
case intro
α : Type u_1
β : Type u_2
inst✝³ : Finite β
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≥ x2
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
⊢ BddBelow (Set.range f)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝³ : Finite β
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≥ x2
f : β → α
M : α
hM : ∀ (i : β), M ≤ f i
b : β
⊢ M ≤ f b

Tactic:
exact hM b

Result:
no goals
-- Mathlib/Probability/IdentDistrib.lean
theorem integrable_snd [NormedAddCommGroup γ] [BorelSpace γ] (h : IdentDistrib f g μ ν)
    (hf : Integrable f μ) : Integrable g ν

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : MemLp f 1 μ
⊢ MemLp g 1 ν

Tactic:
exact h.memLp_snd hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : Integrable f μ
⊢ Integrable g ν

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
g : β → γ
inst✝¹ : NormedAddCommGroup γ
inst✝ : BorelSpace γ
h : IdentDistrib f g μ ν
hf : MemLp f 1 μ
⊢ MemLp g 1 ν
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
lemma degree_map_le : degree (p.map f) ≤ degree p

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
⊢ (map f p).coeff m = 0

Tactic:
simp [hm m le_rfl]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ (map f p).degree ≤ p.degree

Tactic:
refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
m : ℕ
hm : p.degree < ↑m
⊢ (map f p).coeff m = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
m : ℕ
hm : p.degree < ↑m
⊢ (map f p).coeff m = 0

Tactic:
rw [degree_lt_iff_coeff_zero] at hm

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
⊢ (map f p).coeff m = 0
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
/-- See `MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card`
for a version that assumes `n ≤ #R`. -/
lemma eq_zero_of_forall_eval_eq_zero [Infinite R] {F : MvPolynomial σ R} {n : ℕ}
    (hF : F.IsHomogeneous n) (h : ∀ r : σ → R, eval r F = 0) : F = 0

Proof state:
R : Type u_5
σ : Type u_6
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
F : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = 0
⊢ F = 0

Tactic:
apply eq_zero_of_forall_eval_eq_zero_of_le_card hF h

Result:
R : Type u_5
σ : Type u_6
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
F : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = 0
⊢ ↑n ≤ #R

Proof state:
R : Type u_5
σ : Type u_6
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
F : MvPolynomial σ R
n : ℕ
hF : F.IsHomogeneous n
h : ∀ (r : σ → R), (eval r) F = 0
⊢ ↑n ≤ #R

Tactic:
exact (Cardinal.nat_lt_aleph0 _).le.trans <| Cardinal.infinite_iff.mp ‹Infinite R›

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem image_frontier (h : X ≃ₜ Y) (s : Set X) : h '' frontier s = frontier (h '' s)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set X
⊢ ⇑h '' frontier s = frontier (⇑h '' s)

Tactic:
rw [← preimage_symm, preimage_frontier]

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
lemma Nat.cast_ringChar : (ringChar R : R) = 0

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
⊢ ↑(ringChar R) = 0

Tactic:
rw [ringChar.spec]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem dist_partial_sum (u : ℕ → α) (n : ℕ) :
    dist (∑ k ∈ range (n + 1), u k) (∑ k ∈ range n, u k) = ‖u n‖

Proof state:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
u : ℕ → α
n : ℕ
⊢ dist (∑ k ∈ Finset.range (n + 1), u k) (∑ k ∈ Finset.range n, u k) = ‖u n‖

Tactic:
simp [dist_eq_norm, sum_range_succ]

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
theorem inv_mulShift (ψ : AddChar R M) : ψ⁻¹ = mulShift ψ (-1)

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ ψ⁻¹ x✝ = (ψ.mulShift (-1)) x✝

Tactic:
rw [inv_apply, mulShift_apply, neg_mul, one_mul]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
⊢ ψ⁻¹ = ψ.mulShift (-1)

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ ψ⁻¹ x✝ = (ψ.mulShift (-1)) x✝
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_mk_eq_emultiplicity {a b : α} :
    emultiplicity (Associates.mk a) (Associates.mk b) = emultiplicity a b

Proof state:
α : Type u_1
inst✝ : CommMonoid α
a b : α
⊢ emultiplicity (Associates.mk a) (Associates.mk b) = emultiplicity a b

Tactic:
simp [emultiplicity_eq_emultiplicity_iff, ← Associates.mk_pow, Associates.mk_dvd_mk]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem aleph0_mul_nat {n : ℕ} (hn : n ≠ 0) : ℵ₀ * n = ℵ₀

Proof state:
n : ℕ
hn : n ≠ 0
⊢ ℵ₀ * ↑n = ℵ₀

Tactic:
rw [mul_comm, nat_mul_aleph0 hn]

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem isClosed_setOf_map_mul [Mul M₁] [Mul M₂] [ContinuousMul M₂] :
    IsClosed { f : M₁ → M₂ | ∀ x y, f (x * y) = f x * f y }

Proof state:
M₁ : Type u_6
M₂ : Type u_7
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
x y : M₁
⊢ Continuous fun x_1 => x_1 x * x_1 y

Tactic:
continuity

Result:
no goals

Proof state:
M₁ : Type u_6
M₂ : Type u_7
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
⊢ IsClosed (⋂ i, ⋂ i_1, {x | x (i * i_1) = x i * x i_1})

Tactic:
exact
  isClosed_iInter fun x =>
    isClosed_iInter fun y =>
      isClosed_eq (continuous_apply _)
        (by continuity)

Result:
no goals

Proof state:
M₁ : Type u_6
M₂ : Type u_7
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
⊢ IsClosed {f | ∀ (x y : M₁), f (x * y) = f x * f y}

Tactic:
simp only [setOf_forall]

Result:
M₁ : Type u_6
M₂ : Type u_7
inst✝⁴ : TopologicalSpace M₂
inst✝³ : T2Space M₂
inst✝² : Mul M₁
inst✝¹ : Mul M₂
inst✝ : ContinuousMul M₂
⊢ IsClosed (⋂ i, ⋂ i_1, {x | x (i * i_1) = x i * x i_1})
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem frontier_Ioc [NoMaxOrder α] {a b : α} (h : a < b) : frontier (Ioc a b) = {a, b}

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
h : a < b
⊢ frontier (Ioc a b) = {a, b}

Tactic:
rw [frontier, closure_Ioc h.ne, interior_Ioc, Icc_diff_Ioo_same h.le]

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem isPath_cons' {xs : Path F} {a} {f : F.B a → M F} {i : F.B a} :
    IsPath (⟨a, i⟩ :: xs) (M.mk ⟨a, f⟩) → IsPath xs (f i)

Proof state:
F : PFunctor.{u}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
x : F.M
h : M.mk ⟨a, f⟩ = x
⊢ IsPath (⟨a, i⟩ :: xs) x → IsPath xs (f i)

Tactic:
rintro (_ | ⟨_, _, _, _, rfl, hp⟩)

Result:
case cons
F : PFunctor.{u}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
f✝ : F.B a → F.M
hp : IsPath xs (f✝ i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a, f✝⟩
⊢ IsPath xs (f i)

Proof state:
case cons
F : PFunctor.{u}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
f✝ : F.B a → F.M
hp : IsPath xs (f✝ i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a, f✝⟩
⊢ IsPath xs (f i)

Tactic:
cases mk_inj h

Result:
case cons.refl
F : PFunctor.{u}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
hp : IsPath xs (f i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a, f⟩
⊢ IsPath xs (f i)

Proof state:
F : PFunctor.{u}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
⊢ IsPath (⟨a, i⟩ :: xs) (M.mk ⟨a, f⟩) → IsPath xs (f i)

Tactic:
generalize h : M.mk ⟨a, f⟩ = x

Result:
F : PFunctor.{u}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
x : F.M
h : M.mk ⟨a, f⟩ = x
⊢ IsPath (⟨a, i⟩ :: xs) x → IsPath xs (f i)

Proof state:
case cons.refl
F : PFunctor.{u}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
hp : IsPath xs (f i)
h : M.mk ⟨a, f⟩ = M.mk ⟨a, f⟩
⊢ IsPath xs (f i)

Tactic:
exact hp

Result:
no goals
-- Mathlib/Analysis/Complex/Periodic.lean
theorem eventually_differentiableAt_cuspFunction_nhds_ne_zero (hh : 0 < h) (hf : Periodic f h)
    (h_hol : ∀ᶠ z in I∞, DifferentiableAt ℂ f z) :
    ∀ᶠ q in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) q

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ f (invQParam h x) → DifferentiableAt ℂ (cuspFunction h f) x

Tactic:
refine eventually_nhdsWithin_of_forall (fun q hq h_diff ↦ ?_)

Result:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
q : ℂ
hq : q ∈ {0}ᶜ
h_diff : DifferentiableAt ℂ f (invQParam h q)
⊢ DifferentiableAt ℂ (cuspFunction h f) q

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
q : ℂ
hq : q ∈ {0}ᶜ
h_diff : DifferentiableAt ℂ f (invQParam h q)
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h (invQParam h q))

Tactic:
exact differentiableAt_cuspFunction hh.ne' hf h_diff

Result:
no goals

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
q : ℂ
hq : q ∈ {0}ᶜ
h_diff : DifferentiableAt ℂ f (invQParam h q)
⊢ DifferentiableAt ℂ (cuspFunction h f) q

Tactic:
rw [← qParam_right_inv hh.ne' hq]

Result:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
q : ℂ
hq : q ∈ {0}ᶜ
h_diff : DifferentiableAt ℂ f (invQParam h q)
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h (invQParam h q))

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
⊢ ∀ᶠ (q : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) q

Tactic:
refine ((invQParam_tendsto hh).eventually h_hol).mp ?_

Result:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f ↑h
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ f (invQParam h x) → DifferentiableAt ℂ (cuspFunction h f) x
-- Mathlib/Algebra/DirectSum/Basic.lean
theorem IsInternal.addSubmonoid_iSup_eq_top {M : Type*} [DecidableEq ι] [AddCommMonoid M]
    (A : ι → AddSubmonoid M) (h : IsInternal A) : iSup A = ⊤

Proof state:
ι : Type v
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ Surjective ⇑(DFinsupp.sumAddHom fun i => (A i).subtype)

Tactic:
exact Function.Bijective.surjective h

Result:
no goals

Proof state:
ι : Type v
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ iSup A = ⊤

Tactic:
rw [AddSubmonoid.iSup_eq_mrange_dfinsupp_sumAddHom, AddMonoidHom.mrange_eq_top]

Result:
ι : Type v
M : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
A : ι → AddSubmonoid M
h : IsInternal A
⊢ Surjective ⇑(DFinsupp.sumAddHom fun i => (A i).subtype)
-- Mathlib/Order/Interval/Set/OrdConnected.lean
theorem image_Ico (e : α ↪o β) (he : OrdConnected (range e)) (x y : α) :
    e '' Ico x y = Ico (e x) (e y)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Ico x y = Ico (e x) (e y)

Tactic:
rw [← e.preimage_Ico, image_preimage_eq_inter_range,
  inter_eq_left.2 <| Ico_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_updateFinset' [DecidableEq δ] {s : Finset δ} :
    Measurable (fun p : (Π i, π i) × (Π i : s, π i) ↦ updateFinset p.1 s p.2)

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : DecidableEq δ
s : Finset δ
⊢ Measurable fun p => updateFinset p.1 s p.2

Tactic:
simp only [updateFinset, measurable_pi_iff]

Result:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : DecidableEq δ
s : Finset δ
⊢ ∀ (a : δ), Measurable fun x => if hi : a ∈ s then x.2 ⟨a, hi⟩ else x.1 a

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
⊢ Measurable fun x => if hi : i ∈ s then x.2 ⟨i, hi⟩ else x.1 i

Tactic:
by_cases h : i ∈ s <;> simp [h, Measurable.eval, measurable_fst, measurable_snd]

Result:
no goals

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : DecidableEq δ
s : Finset δ
⊢ ∀ (a : δ), Measurable fun x => if hi : a ∈ s then x.2 ⟨a, hi⟩ else x.1 a

Tactic:
intro i

Result:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : DecidableEq δ
s : Finset δ
i : δ
⊢ Measurable fun x => if hi : i ∈ s then x.2 ⟨i, hi⟩ else x.1 i
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem support_finSuccEquiv_nonempty {f : MvPolynomial (Fin (n + 1)) R} (h : f ≠ 0) :
    (finSuccEquiv R n f).support.Nonempty

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
h : f ≠ 0
⊢ ((finSuccEquiv R n) f).support.Nonempty

Tactic:
rwa [Polynomial.support_nonempty, EmbeddingLike.map_ne_zero_iff]

Result:
no goals