harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Localization/FractionRing.lean
@[simp]
lemma fieldEquivOfAlgEquiv_refl :
    fieldEquivOfAlgEquiv FA FB FB (AlgEquiv.refl : B ≃ₐ[A] B) = AlgEquiv.refl

Proof state:
case h
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
FA : Type u_12
FB : Type u_13
inst✝⁹ : Field FA
inst✝⁸ : Field FB
inst✝⁷ : Algebra A FA
inst✝⁶ : Algebra B FB
inst✝⁵ : IsFractionRing A FA
inst✝⁴ : IsFractionRing B FB
inst✝³ : Algebra A FB
inst✝² : IsScalarTower A B FB
inst✝¹ : Algebra FA FB
inst✝ : IsScalarTower A FA FB
x : FB
⊢ (fieldEquivOfAlgEquiv FA FB FB AlgEquiv.refl) x = AlgEquiv.refl x

Tactic:
obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective (A := B) x

Result:
case h.intro.intro.intro
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
FA : Type u_12
FB : Type u_13
inst✝⁹ : Field FA
inst✝⁸ : Field FB
inst✝⁷ : Algebra A FA
inst✝⁶ : Algebra B FB
inst✝⁵ : IsFractionRing A FA
inst✝⁴ : IsFractionRing B FB
inst✝³ : Algebra A FB
inst✝² : IsScalarTower A B FB
inst✝¹ : Algebra FA FB
inst✝ : IsScalarTower A FA FB
x y : B
⊢ (fieldEquivOfAlgEquiv FA FB FB AlgEquiv.refl) ((algebraMap B FB) x / (algebraMap B FB) y) =
    AlgEquiv.refl ((algebraMap B FB) x / (algebraMap B FB) y)

Proof state:
case h.intro.intro.intro
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
FA : Type u_12
FB : Type u_13
inst✝⁹ : Field FA
inst✝⁸ : Field FB
inst✝⁷ : Algebra A FA
inst✝⁶ : Algebra B FB
inst✝⁵ : IsFractionRing A FA
inst✝⁴ : IsFractionRing B FB
inst✝³ : Algebra A FB
inst✝² : IsScalarTower A B FB
inst✝¹ : Algebra FA FB
inst✝ : IsScalarTower A FA FB
x y : B
⊢ (fieldEquivOfAlgEquiv FA FB FB AlgEquiv.refl) ((algebraMap B FB) x / (algebraMap B FB) y) =
    AlgEquiv.refl ((algebraMap B FB) x / (algebraMap B FB) y)

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
FA : Type u_12
FB : Type u_13
inst✝⁹ : Field FA
inst✝⁸ : Field FB
inst✝⁷ : Algebra A FA
inst✝⁶ : Algebra B FB
inst✝⁵ : IsFractionRing A FA
inst✝⁴ : IsFractionRing B FB
inst✝³ : Algebra A FB
inst✝² : IsScalarTower A B FB
inst✝¹ : Algebra FA FB
inst✝ : IsScalarTower A FA FB
⊢ fieldEquivOfAlgEquiv FA FB FB AlgEquiv.refl = AlgEquiv.refl

Tactic:
ext x

Result:
case h
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
FA : Type u_12
FB : Type u_13
inst✝⁹ : Field FA
inst✝⁸ : Field FB
inst✝⁷ : Algebra A FA
inst✝⁶ : Algebra B FB
inst✝⁵ : IsFractionRing A FA
inst✝⁴ : IsFractionRing B FB
inst✝³ : Algebra A FB
inst✝² : IsScalarTower A B FB
inst✝¹ : Algebra FA FB
inst✝ : IsScalarTower A FA FB
x : FB
⊢ (fieldEquivOfAlgEquiv FA FB FB AlgEquiv.refl) x = AlgEquiv.refl x
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem circumradius_eq_of_cospherical_subset {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ s)
    [Nonempty s] {n : ℕ} [FiniteDimensional ℝ s.direction] (hd : finrank ℝ s.direction = n)
    (hc : Cospherical ps) {sx₁ sx₂ : Simplex ℝ P n} (hsx₁ : Set.range sx₁.points ⊆ ps)
    (hsx₂ : Set.range sx₂.points ⊆ ps) : sx₁.circumradius = sx₂.circumradius

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
⊢ sx₁.circumradius = sx₂.circumradius

Tactic:
rcases exists_circumradius_eq_of_cospherical_subset h hd hc with ⟨r, hr⟩

Result:
case intro
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
⊢ sx₁.circumradius = sx₂.circumradius

Proof state:
case intro
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
⊢ sx₁.circumradius = sx₂.circumradius

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

Result:
no goals
-- Mathlib/RingTheory/Noetherian/Basic.lean
theorem isNoetherian_of_range_eq_ker [IsNoetherian R M] [IsNoetherian R P]
    (f : M →ₗ[R] N) (g : N →ₗ[R] P) (h : LinearMap.range f = LinearMap.ker g) :
    IsNoetherian R N :=
  isNoetherian_mk <|
    wellFounded_gt_exact_sequence
      (LinearMap.range f)
      (Submodule.map (f.ker.liftQ f le_rfl))
      (Submodule.comap (f.ker.liftQ f le_rfl))
      (Submodule.comap g.rangeRestrict) (Submodule.map g.rangeRestrict)
      (Submodule.gciMapComap <| LinearMap.ker_eq_bot.mp <| Submodule.ker_liftQ_eq_bot _ _ _ le_rfl)
      (Submodule.giMapComap g.surjective_rangeRestrict)
      (by simp [Submodule.map_comap_eq, inf_comm, Submodule.range_liftQ])
      (by simp [Submodule.comap_map_eq, h])

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : IsNoetherian R M
inst✝ : IsNoetherian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : LinearMap.range f = LinearMap.ker g
⊢ ∀ (a : Submodule R N),
    Submodule.map ((LinearMap.ker f).liftQ f ⋯) (Submodule.comap ((LinearMap.ker f).liftQ f ⋯) a) =
      a ⊓ LinearMap.range f

Tactic:
simp [Submodule.map_comap_eq, inf_comm, Submodule.range_liftQ]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
inst✝¹ : IsNoetherian R M
inst✝ : IsNoetherian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : LinearMap.range f = LinearMap.ker g
⊢ ∀ (a : Submodule R N), Submodule.comap g.rangeRestrict (Submodule.map g.rangeRestrict a) = a ⊔ LinearMap.range f

Tactic:
simp [Submodule.comap_map_eq, h]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem map_hom_inv (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [IsIso f] :
    F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_mul_int_iff : Irrational (x * m) ↔ m ≠ 0 ∧ Irrational x

Proof state:
m : ℤ
x : ℝ
⊢ Irrational (x * ↑m) ↔ m ≠ 0 ∧ Irrational x

Tactic:
rw [← cast_intCast, irrational_mul_rat_iff, Int.cast_ne_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem id_whiskerLeft {X Y : C} (f : X ⟶ Y) :
    𝟙_ C ◁ f = (λ_ X).hom ≫ f ≫ (λ_ Y).inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ 𝟙_ C ◁ f = (λ_ X).hom ≫ f ≫ (λ_ Y).inv

Tactic:
rw [← assoc, ← leftUnitor_naturality]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ 𝟙_ C ◁ f = (𝟙_ C ◁ f ≫ (λ_ Y).hom) ≫ (λ_ Y).inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ 𝟙_ C ◁ f = (𝟙_ C ◁ f ≫ (λ_ Y).hom) ≫ (λ_ Y).inv

Tactic:
simp [id_tensorHom]

Result:
no goals
-- Mathlib/CategoryTheory/Simple.lean
theorem epi_of_nonzero_to_simple [HasEqualizers C] {X Y : C} [Simple Y] {f : X ⟶ Y} [HasImage f]
    (w : f ≠ 0) : Epi f

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
this : IsIso (image.ι f)
⊢ Epi (factorThruImage f ≫ image.ι f)

Tactic:
apply epi_comp

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
⊢ Epi f

Tactic:
rw [← image.fac f]

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
⊢ Epi (factorThruImage f ≫ image.ι f)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
⊢ Epi (factorThruImage f ≫ image.ι f)

Tactic:
haveI : IsIso (image.ι f) := isIso_of_mono_of_nonzero fun h => w (eq_zero_of_image_eq_zero h)

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
this : IsIso (image.ι f)
⊢ Epi (factorThruImage f ≫ image.ι f)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem forall_mem_filter {p : α → Bool} {l : Array α} {P : α → Prop} :
    (∀ (i) (_ : i ∈ l.filter p), P i) ↔ ∀ (j) (_ : j ∈ l), p j → P j

Proof state:
α : Type u_1
p : α → Bool
l : Array α
P : α → Prop
⊢ (∀ (i : α), i ∈ filter p l → P i) ↔ ∀ (j : α), j ∈ l → p j = true → P j

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem ite_self {α : Sort u} {c : Prop} {d : Decidable c} (a : α) : ite c a a = a

Proof state:
α : Sort u
c : Prop
d : Decidable c
a : α
⊢ ite c a a = a

Tactic:
cases d <;> rfl

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Defs.lean
theorem mul_eq_zero_iff_left (ha : a ≠ 0) : a * b = 0 ↔ b = 0

Proof state:
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
ha : a ≠ 0
⊢ a * b = 0 ↔ b = 0

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Period.lean
theorem period_eq_one_iff {m : M} {a : α} : period m a = 1 ↔ m • a = a :=
  ⟨fun eq_one => pow_one m ▸ eq_one ▸ pow_period_smul m a,
   fun fixed => le_antisymm
    (period_le_of_fixed one_pos (by simpa))
    (period_pos_of_fixed one_pos (by simpa))⟩

Proof state:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
fixed : m • a = a
⊢ m ^ 1 • a = a

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.ofBool_eq_if (b : Bool) : BitVec.ofBool b = bif b then 1#1 else 0#1

Proof state:
⊢ ∀ (b : Bool), BitVec.ofBool b = bif b then 1#1 else 0#1

Tactic:
decide

Result:
no goals

Proof state:
b : Bool
⊢ BitVec.ofBool b = bif b then 1#1 else 0#1

Tactic:
revert b

Result:
⊢ ∀ (b : Bool), BitVec.ofBool b = bif b then 1#1 else 0#1
-- Mathlib/Algebra/Order/BigOperators/GroupWithZero/Multiset.lean
theorem prod_map_lt_prod_map {ι : Type*} {s : Multiset ι} (hs : s ≠ 0)
    (f : ι → R) (g : ι → R) (h0 : ∀ i ∈ s, 0 < f i) (h : ∀ i ∈ s, f i < g i) :
    (map f s).prod < (map g s).prod

Proof state:
case a
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
f g : ι → R
a✝ : List ι
hs : ¬a✝ = []
h0 : ∀ i ∈ a✝, 0 < f i
h : ∀ i ∈ a✝, f i < g i
⊢ (List.map f a✝).prod < (List.map g a✝).prod

Tactic:
apply List.prod_map_lt_prod_map hs f g h0 h

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
f g : ι → R
a✝ : List ι
hs : ⟦a✝⟧ ≠ 0
h0 : ∀ i ∈ ⟦a✝⟧, 0 < f i
h : ∀ i ∈ ⟦a✝⟧, f i < g i
⊢ (map f ⟦a✝⟧).prod < (map g ⟦a✝⟧).prod

Tactic:
simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe, ne_eq, coe_eq_zero] at *

Result:
case a
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
f g : ι → R
a✝ : List ι
hs : ¬a✝ = []
h0 : ∀ i ∈ a✝, 0 < f i
h : ∀ i ∈ a✝, f i < g i
⊢ (List.map f a✝).prod < (List.map g a✝).prod

Proof state:
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
s : Multiset ι
hs : s ≠ 0
f g : ι → R
h0 : ∀ i ∈ s, 0 < f i
h : ∀ i ∈ s, f i < g i
⊢ (map f s).prod < (map g s).prod

Tactic:
cases s using Quotient.ind

Result:
case a
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
ι : Type u_2
f g : ι → R
a✝ : List ι
hs : ⟦a✝⟧ ≠ 0
h0 : ∀ i ∈ ⟦a✝⟧, 0 < f i
h : ∀ i ∈ ⟦a✝⟧, f i < g i
⊢ (map f ⟦a✝⟧).prod < (map g ⟦a✝⟧).prod
-- Mathlib/Data/Complex/Trigonometric.lean
theorem exp_im : (exp x).im = Real.exp x.re * Real.sin x.im

Proof state:
x : ℂ
⊢ (cexp x).im = Real.exp x.re * Real.sin x.im

Tactic:
rw [exp_eq_exp_re_mul_sin_add_cos]

Result:
x : ℂ
⊢ (cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)).im = Real.exp x.re * Real.sin x.im

Proof state:
x : ℂ
⊢ (cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)).im = Real.exp x.re * Real.sin x.im

Tactic:
simp [exp_ofReal_re, sin_ofReal_re]

Result:
no goals
-- Mathlib/Dynamics/FixedPoints/Topology.lean
theorem isFixedPt_of_tendsto_iterate {x y : α} (hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y))
    (hf : ContinuousAt f y) : IsFixedPt f y

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : α → α
x y : α
hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ Tendsto (fun n => (f ∘ f^[n]) x) atTop (𝓝 (f y))

Tactic:
exact hf.tendsto.comp hy

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : α → α
x y : α
hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ Tendsto (fun n => f^[n + 1] x) atTop (𝓝 (f y))

Tactic:
simp only [iterate_succ' f]

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : α → α
x y : α
hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ Tendsto (fun n => (f ∘ f^[n]) x) atTop (𝓝 (f y))

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : α → α
x y : α
hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ IsFixedPt f y

Tactic:
refine tendsto_nhds_unique ((tendsto_add_atTop_iff_nat 1).1 ?_) hy

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : α → α
x y : α
hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ Tendsto (fun n => f^[n + 1] x) atTop (𝓝 (f y))
-- Mathlib/Topology/PartialHomeomorph.lean
theorem continuousAt_iff_continuousAt_comp_right {f : Y → Z} {x : Y} (h : x ∈ e.target) :
    ContinuousAt f x ↔ ContinuousAt (f ∘ e) (e.symm x)

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Y → Z
x : Y
h : x ∈ e.target
⊢ ContinuousAt f x ↔ ContinuousAt (f ∘ ↑e) (↑e.symm x)

Tactic:
rw [← continuousWithinAt_univ, e.continuousWithinAt_iff_continuousWithinAt_comp_right h,
  preimage_univ, continuousWithinAt_univ]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem aeval_C [Algebra R R'] (x : R') (n : ℤ) : aeval x (C R n) = (C R' n).eval x

Proof state:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R'
n : ℤ
⊢ (aeval x) (C R n) = eval x (C R' n)

Tactic:
rw [aeval_def, eval₂_eq_eval_map, map_C]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
@[simp] lemma toCircle_zero : toCircle 0 = 1

Proof state:
⊢ toCircle 0 = 1

Tactic:
rw [← coe_zero, toCircle_coe, Circle.exp_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem quasiMeasurePreserving_snd : QuasiMeasurePreserving Prod.snd (μ.prod ν) ν

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set β
hs : MeasurableSet s
h2s : ν s = 0
⊢ (map Prod.snd (μ.prod ν)) s = 0

Tactic:
rw [map_apply measurable_snd hs, ← univ_prod, prod_prod, h2s, mul_zero]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
⊢ QuasiMeasurePreserving Prod.snd (μ.prod ν) ν

Tactic:
refine ⟨measurable_snd, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set β
hs : MeasurableSet s
h2s : ν s = 0
⊢ (map Prod.snd (μ.prod ν)) s = 0
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem nonempty_Ioo [DenselyOrdered α] : (Ioo a b).Nonempty ↔ a < b

Proof state:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
⊢ (Ioo a b).Nonempty ↔ a < b

Tactic:
rw [← coe_nonempty, coe_Ioo, Set.nonempty_Ioo]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma RightHomologyData.homologyIso_inv_comp_homologyι (h : S.RightHomologyData) :
    h.homologyIso.inv ≫ S.homologyι = h.ι ≫ h.opcyclesIso.inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ h.homologyIso.inv ≫ S.homologyι = h.ι ≫ h.opcyclesIso.inv

Tactic:
dsimp only [homologyι, homologyIso]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ (S.rightHomologyIso.symm ≪≫ h.rightHomologyIso).inv ≫ S.rightHomologyIso.inv ≫ S.rightHomologyι =
    h.ι ≫ h.opcyclesIso.inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.RightHomologyData
⊢ (S.rightHomologyIso.symm ≪≫ h.rightHomologyIso).inv ≫ S.rightHomologyIso.inv ≫ S.rightHomologyι =
    h.ι ≫ h.opcyclesIso.inv

Tactic:
simp only [Iso.trans_inv, Iso.symm_inv, assoc, Iso.hom_inv_id_assoc,
  rightHomologyIso_inv_comp_rightHomologyι]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem tensorRightHomEquiv_naturality {X Y Y' Z Z' : C} [ExactPairing Y Y'] (f : X ⊗ Y ⟶ Z)
    (g : Z ⟶ Z') :
    (tensorRightHomEquiv X Y Y' Z') (f ≫ g) = (tensorRightHomEquiv X Y Y' Z) f ≫ g ▷ Y'

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z Z' : C
inst✝ : ExactPairing Y Y'
f : X ⊗ Y ⟶ Z
g : Z ⟶ Z'
⊢ (tensorRightHomEquiv X Y Y' Z') (f ≫ g) = (tensorRightHomEquiv X Y Y' Z) f ≫ g ▷ Y'

Tactic:
simp [tensorRightHomEquiv]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extChartAt_source_mem_nhds' {x x' : M} (h : x' ∈ (extChartAt I x).source) :
    (extChartAt I x).source ∈ 𝓝 x' :=
  extend_source_mem_nhds _ <| by rwa [← extChartAt_source I]

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x x' : M
h : x' ∈ (extChartAt I x).source
⊢ x' ∈ (chartAt H x).source

Tactic:
rwa [← extChartAt_source I]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem ssubset_toFinset {s : Finset α} [Fintype t] : s ⊂ t.toFinset ↔ ↑s ⊂ t

Proof state:
α : Type u_1
t : Set α
s : Finset α
inst✝ : Fintype ↑t
⊢ s ⊂ t.toFinset ↔ ↑s ⊂ t

Tactic:
rw [← Finset.coe_ssubset, coe_toFinset]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem freeOn_dual_eq : (freeOn E)✶ = loopyOn E

Proof state:
α : Type u_1
E : Set α
⊢ (freeOn E)✶ = loopyOn E

Tactic:
rw [freeOn, dual_dual]

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem coe_comp_toNNReal_comp {ι : Type*} {f : ι → ℝ≥0∞} (hf : ∀ x, f x ≠ ∞) :
    (fun (x : ℝ≥0) => (x : ℝ≥0∞)) ∘ ENNReal.toNNReal ∘ f = f

Proof state:
case h
ι : Type u_2
f : ι → ℝ≥0∞
hf : ∀ (x : ι), f x ≠ ⊤
x : ι
⊢ ((fun x => ↑x) ∘ ENNReal.toNNReal ∘ f) x = f x

Tactic:
simp [coe_toNNReal (hf x)]

Result:
no goals

Proof state:
ι : Type u_2
f : ι → ℝ≥0∞
hf : ∀ (x : ι), f x ≠ ⊤
⊢ (fun x => ↑x) ∘ ENNReal.toNNReal ∘ f = f

Tactic:
ext x

Result:
case h
ι : Type u_2
f : ι → ℝ≥0∞
hf : ∀ (x : ι), f x ≠ ⊤
x : ι
⊢ ((fun x => ↑x) ∘ ENNReal.toNNReal ∘ f) x = f x
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem offsetOfPos_of_valid (l r) : offsetOfPos ⟨l ++ r⟩ ⟨utf8Len l⟩ = l.length

Proof state:
l r : List Char
⊢ { data := l ++ r }.offsetOfPos { byteIdx := utf8Len l } = l.length

Tactic:
simpa using offsetOfPosAux_of_valid [] l r 0

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem le_of_add_le_add_right {a b c : Nat} : a + b ≤ c + b → a ≤ c

Proof state:
a b c : Nat
⊢ b + a ≤ b + c → a ≤ c

Tactic:
apply Nat.le_of_add_le_add_left

Result:
no goals

Proof state:
a b c : Nat
⊢ a + b ≤ c + b → a ≤ c

Tactic:
rw [Nat.add_comm _ b, Nat.add_comm _ b]

Result:
a b c : Nat
⊢ b + a ≤ b + c → a ≤ c
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem mul_annihilator (I : Ideal R) : I * annihilator I = ⊥

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I * annihilator I = ⊥

Tactic:
rw [mul_comm, annihilator_mul]

Result:
no goals
-- Mathlib/Data/Set/Finite/Lattice.lean
theorem finite_biUnion {ι : Type*} (s : Set ι) [Finite s] (t : ι → Set α)
    (H : ∀ i ∈ s, Finite (t i)) : Finite (⋃ x ∈ s, t x)

Proof state:
α : Type u
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ i ∈ s, Finite ↑(t i)
⊢ Finite ↑(⋃ x, t ↑x)

Tactic:
haveI : ∀ i : s, Finite (t i) := fun i => H i i.property

Result:
α : Type u
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ i ∈ s, Finite ↑(t i)
this : ∀ (i : ↑s), Finite ↑(t ↑i)
⊢ Finite ↑(⋃ x, t ↑x)

Proof state:
α : Type u
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ i ∈ s, Finite ↑(t i)
⊢ Finite ↑(⋃ x ∈ s, t x)

Tactic:
rw [biUnion_eq_iUnion]

Result:
α : Type u
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ i ∈ s, Finite ↑(t i)
⊢ Finite ↑(⋃ x, t ↑x)

Proof state:
α : Type u
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ i ∈ s, Finite ↑(t i)
this : ∀ (i : ↑s), Finite ↑(t ↑i)
⊢ Finite ↑(⋃ x, t ↑x)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Order/CompleteLattice/SetLike.lean
@[simp] lemma setLike_mem_inf : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Proof state:
X : Type u_1
L : Sublattice (Set X)
S T : ↥L
x : X
⊢ x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Tactic:
simp [← mem_subtype]

Result:
no goals
-- Mathlib/Analysis/Complex/Hadamard.lean
lemma eventuallyle (z : ℂ) (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1))
    (hd : DiffContOnCl ℂ f (verticalStrip 0 1)) (hz : z ∈ verticalStrip 0 1) :
    (fun _ : ℝ ↦ ‖f z‖) ≤ᶠ[𝓝[>] 0]
    (fun ε ↦ ‖((ε + sSupNormIm f 0) ^ (1 - z) * (ε + sSupNormIm f 1) ^ z : ℂ)‖)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
f : ℂ → E
inst✝ : NormedSpace ℂ E
z : ℂ
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hz : z ∈ verticalStrip 0 1
⊢ (fun x => ‖f z‖) ≤ᶠ[𝓝[>] 0] fun ε => ‖(↑ε + ↑(sSupNormIm f 0)) ^ (1 - z) * (↑ε + ↑(sSupNormIm f 1)) ^ z‖

Tactic:
filter_upwards [self_mem_nhdsWithin] with ε (hε : 0 < ε) using
  norm_le_interpStrip_of_mem_verticalClosedStrip_eps f ε hε z hB hd
    (mem_of_mem_of_subset hz (preimage_mono Ioo_subset_Icc_self))

Result:
no goals