harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Bisect.lean
theorem le_avg_left (h : a ≤ b) : a ≤ avg a b

Proof state:
a b : Nat
h : a ≤ b
⊢ a * 2 ≤ a + b

Tactic:
simp_arith [*]

Result:
no goals

Proof state:
a b : Nat
h : a ≤ b
⊢ a ≤ a.avg b

Tactic:
apply (Nat.le_div_iff_mul_le Nat.zero_lt_two).mpr

Result:
a b : Nat
h : a ≤ b
⊢ a * 2 ≤ a + b
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive]
protected lemma div_div_cancel_left (h : IsUnit a) : a / b / a = b⁻¹

Proof state:
α : Type u
inst✝ : DivisionCommMonoid α
a b : α
h : IsUnit a
⊢ a / b / a = b⁻¹

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, mul_right_comm, h.mul_inv_cancel, one_mul]

Result:
no goals
-- Mathlib/Topology/Algebra/UniformMulAction.lean
theorem UniformContinuous.div_const' {R β : Type*} [DivisionRing R] [UniformSpace R]
    [UniformContinuousConstSMul Rᵐᵒᵖ R] [UniformSpace β] {f : β → R}
    (hf : UniformContinuous f) (a : R) :
    UniformContinuous fun x ↦ f x / a

Proof state:
R : Type u_3
β : Type u_4
inst✝³ : DivisionRing R
inst✝² : UniformSpace R
inst✝¹ : UniformContinuousConstSMul Rᵐᵒᵖ R
inst✝ : UniformSpace β
f : β → R
hf : UniformContinuous f
a : R
⊢ UniformContinuous fun x => f x / a

Tactic:
simpa [div_eq_mul_inv] using hf.mul_const' a⁻¹

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_inj_right {f : α → β} {o o' : Option α} (w : ∀ x y, f x = f y → x = y) :
    o.map f = o'.map f ↔ o = o'

Proof state:
case some
α : Type u_1
β : Type u_2
f : α → β
o' : Option α
w : ∀ (x y : α), f x = f y → x = y
a : α
⊢ Option.map f (some a) = Option.map f o' ↔ some a = o'

Tactic:
cases o' with
| none => simp
| some a' => simpa using ⟨fun h => w _ _ h, fun h => congrArg f h⟩

Result:
no goals

Proof state:
case none
α : Type u_1
β : Type u_2
f : α → β
o' : Option α
w : ∀ (x y : α), f x = f y → x = y
⊢ Option.map f none = Option.map f o' ↔ none = o'

Tactic:
cases o' <;> simp

Result:
no goals

Proof state:
case some.none
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
a : α
⊢ Option.map f (some a) = Option.map f none ↔ some a = none

Tactic:
simp

Result:
no goals

Proof state:
case some.some
α : Type u_1
β : Type u_2
f : α → β
w : ∀ (x y : α), f x = f y → x = y
a a' : α
⊢ Option.map f (some a) = Option.map f (some a') ↔ some a = some a'

Tactic:
simpa using ⟨fun h => w _ _ h, fun h => congrArg f h⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
o o' : Option α
w : ∀ (x y : α), f x = f y → x = y
⊢ Option.map f o = Option.map f o' ↔ o = o'

Tactic:
cases o with
| none => cases o' <;> simp
| some a =>
  cases o' with
  | none => simp
  | some a' => simpa using ⟨fun h => w _ _ h, fun h => congrArg f h⟩

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem map_top_of_surjective (f : α → β) (hf : Surjective f) : map f ⊤ = ⊤

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ (map f) ⊤ = ⊤

Tactic:
rw [map_top, hf.range_eq, restrict_univ]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem map_id : map (id : M →ₗ[R] M) (id : N →ₗ[R] N) = .id

Proof state:
case H.h.h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ : M
x✝ : N
⊢ (((mk R M N).compr₂ (map LinearMap.id LinearMap.id)) x✝¹) x✝ = (((mk R M N).compr₂ LinearMap.id) x✝¹) x✝

Tactic:
simp only [mk_apply, id_coe, compr₂_apply, _root_.id, map_tmul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ map LinearMap.id LinearMap.id = LinearMap.id

Tactic:
ext

Result:
case H.h.h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝¹ : M
x✝ : N
⊢ (((mk R M N).compr₂ (map LinearMap.id LinearMap.id)) x✝¹) x✝ = (((mk R M N).compr₂ LinearMap.id) x✝¹) x✝
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem surjOn_logb' : SurjOn (logb b) (Iio 0) univ

Proof state:
case h.right
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ logb b (-b ^ x) = x

Tactic:
rw [logb_neg_eq_logb, logb_rpow b_pos b_ne_one]

Result:
no goals

Proof state:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ x ∈ logb b '' Iio 0

Tactic:
use -b ^ x

Result:
case h
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ -b ^ x ∈ Iio 0 ∧ logb b (-b ^ x) = x

Proof state:
case h
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ -b ^ x ∈ Iio 0 ∧ logb b (-b ^ x) = x

Tactic:
constructor

Result:
case h.left
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ -b ^ x ∈ Iio 0

case h.right
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ logb b (-b ^ x) = x

Proof state:
case h.left
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ -b ^ x ∈ Iio 0

Tactic:
simp only [Right.neg_neg_iff, Set.mem_Iio]

Result:
case h.left
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ 0 < b ^ x

Proof state:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
⊢ SurjOn (logb b) (Iio 0) univ

Tactic:
intro x _

Result:
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ x ∈ logb b '' Iio 0

Proof state:
case h.left
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ 0 < b ^ x

Tactic:
apply rpow_pos_of_pos b_pos

Result:
no goals
-- Mathlib/Condensed/Basic.lean
@[ext]
lemma hom_ext {X Y : Condensed.{u} C} (f g : X ⟶ Y) (h : ∀ S, f.val.app S = g.val.app S) :
    f = g

Proof state:
case h
C : Type w
inst✝ : Category.{v, w} C
X Y : Condensed C
f g : X ⟶ Y
h : ∀ (S : CompHausᵒᵖ), f.val.app S = g.val.app S
⊢ f.val = g.val

Tactic:
ext

Result:
case h.w.h
C : Type w
inst✝ : Category.{v, w} C
X Y : Condensed C
f g : X ⟶ Y
h : ∀ (S : CompHausᵒᵖ), f.val.app S = g.val.app S
x✝ : CompHausᵒᵖ
⊢ f.val.app x✝ = g.val.app x✝

Proof state:
C : Type w
inst✝ : Category.{v, w} C
X Y : Condensed C
f g : X ⟶ Y
h : ∀ (S : CompHausᵒᵖ), f.val.app S = g.val.app S
⊢ f = g

Tactic:
apply Sheaf.hom_ext

Result:
case h
C : Type w
inst✝ : Category.{v, w} C
X Y : Condensed C
f g : X ⟶ Y
h : ∀ (S : CompHausᵒᵖ), f.val.app S = g.val.app S
⊢ f.val = g.val

Proof state:
case h.w.h
C : Type w
inst✝ : Category.{v, w} C
X Y : Condensed C
f g : X ⟶ Y
h : ∀ (S : CompHausᵒᵖ), f.val.app S = g.val.app S
x✝ : CompHausᵒᵖ
⊢ f.val.app x✝ = g.val.app x✝

Tactic:
exact h _

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
/-- The support of a hamiltonian walk is the entire vertex set. -/
lemma IsHamiltonian.support_toFinset (hp : p.IsHamiltonian) : p.support.toFinset = Finset.univ

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
hp : p.IsHamiltonian
⊢ p.support.toFinset = univ

Tactic:
simp [eq_univ_iff_forall, hp]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Ring.lean
theorem of_zero_pow (a : A 0) : ∀ n : ℕ, of A 0 (a ^ n) = of A 0 a ^ n
  | 0 => by rw [pow_zero, pow_zero, DirectSum.of_zero_one]
  -- Porting note: Lean doesn't think this terminates if we only use `of_zero_pow` alone
  | n + 1 => by rw [pow_succ, pow_succ, of_zero_mul, of_zero_pow _ n]

Proof state:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
n : ℕ
⊢ (of A 0) (a ^ (n + 1)) = (of A 0) a ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ, of_zero_mul, of_zero_pow _ n]

Result:
no goals

Proof state:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
⊢ (of A 0) (a ^ 0) = (of A 0) a ^ 0

Tactic:
rw [pow_zero, pow_zero, DirectSum.of_zero_one]

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem constant_of_derivWithin_zero (hdiff : DifferentiableOn ℝ f (Icc a b))
    (hderiv : ∀ x ∈ Ico a b, derivWithin f (Icc a b) x = 0) : ∀ x ∈ Icc a b, f x = f a

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hdiff : DifferentiableOn ℝ f (Icc a b)
hderiv : ∀ x ∈ Ico a b, derivWithin f (Icc a b) x = 0
⊢ ∀ x ∈ Icc a b, f x = f a

Tactic:
have H : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ 0 := by
  simpa only [norm_le_zero_iff] using fun x hx => hderiv x hx

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hdiff : DifferentiableOn ℝ f (Icc a b)
hderiv : ∀ x ∈ Ico a b, derivWithin f (Icc a b) x = 0
H : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ 0
⊢ ∀ x ∈ Icc a b, f x = f a

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hdiff : DifferentiableOn ℝ f (Icc a b)
hderiv : ∀ x ∈ Ico a b, derivWithin f (Icc a b) x = 0
H : ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ 0
⊢ ∀ x ∈ Icc a b, f x = f a

Tactic:
simpa only [zero_mul, norm_le_zero_iff, sub_eq_zero] using fun x hx =>
  norm_image_sub_le_of_norm_deriv_le_segment hdiff H x hx

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
hdiff : DifferentiableOn ℝ f (Icc a b)
hderiv : ∀ x ∈ Ico a b, derivWithin f (Icc a b) x = 0
⊢ ∀ x ∈ Ico a b, ‖derivWithin f (Icc a b) x‖ ≤ 0

Tactic:
simpa only [norm_le_zero_iff] using fun x hx => hderiv x hx

Result:
no goals
-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
lemma limsup_add_le (h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u

Proof state:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > limsup v f
c : α
c_ab : c > a + b
⊢ ∀ᶠ (a : ι) in f, (u + v) a < c

Tactic:
filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v] with x a_x b_x

Result:
case h
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > limsup v f
c : α
c_ab : c > a + b
x : ι
a_x : u x < a
b_x : v x < b
⊢ (u + v) x < c

Proof state:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)
⊢ limsup (u + v) f ≤ limsup u f + limsup v f

Tactic:
have h' := isBoundedUnder_le_add h₂ h₄

Result:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)
⊢ limsup (u + v) f ≤ limsup u f + limsup v f
-- Mathlib/CategoryTheory/Shift/CommShift.lean
@[simp]
lemma isoAdd_inv_app {a b : A}
    (e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a)
    (e₂ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b) (X : C) :
      (CommShift.isoAdd e₁ e₂).inv.app X = (shiftFunctorAdd D a b).hom.app (F.obj X) ≫
        (shiftFunctor D b).map (e₁.inv.app X) ≫ e₂.inv.app ((shiftFunctor C a).obj X) ≫
        F.map ((shiftFunctorAdd C a b).inv.app X)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_7, u_1} C
inst✝³ : Category.{u_6, u_2} D
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
X : C
⊢ (isoAdd e₁ e₂).inv.app X =
    (shiftFunctorAdd D a b).hom.app (F.obj X) ≫
      (shiftFunctor D b).map (e₁.inv.app X) ≫
        e₂.inv.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X)

Tactic:
simp only [isoAdd, isoAdd'_inv_app, shiftFunctorAdd'_eq_shiftFunctorAdd]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem AnalyticSet.iInter [hι : Nonempty ι] [Countable ι] [T2Space α] {s : ι → Set α}
    (hs : ∀ n, AnalyticSet (s n)) : AnalyticSet (⋂ n, s n)

Proof state:
case h₂
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed t
this : PolishSpace ↑t
F : ↑t → α := fun x => f i₀ (↑x i₀)
F_cont : Continuous F
y : α
hy : y ∈ ⋂ n, s n
A : ∀ (n : ι), ∃ x, f n x = y
⊢ y ∈ range F

Tactic:
choose x hx using A

Result:
case h₂
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed t
this : PolishSpace ↑t
F : ↑t → α := fun x => f i₀ (↑x i₀)
F_cont : Continuous F
y : α
hy : y ∈ ⋂ n, s n
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
⊢ y ∈ range F

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed t
this : PolishSpace ↑t
F : ↑t → α := fun x => f i₀ (↑x i₀)
F_cont : Continuous F
y : α
hy : y ∈ ⋂ n, s n
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
⊢ x ∈ t

Tactic:
refine mem_iInter.2 fun n => ?_

Result:
α : Type u_1
ι : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Countable ι
inst✝ : T2Space α
s : ι → Set α
hs : ∀ (n : ι), AnalyticSet (s n)
i₀ : ι
β : ι → Type
hβ : (n : ι) → TopologicalSpace (β n)
h'β : ∀ (n : ι), PolishSpace (β n)
f : (n : ι) → β n → α
f_cont : ∀ (n : ι), Continuous (f n)
f_range : ∀ (n : ι), range (f n) = s n
γ : Type u_2 := (n : ι) → β n
t : Set γ := ⋂ n, {x | f n (x n) = f i₀ (x i₀)}
t_closed : IsClosed t
this : PolishSpace ↑t
F : ↑t → α := fun x => f i₀ (↑x i₀)
F_cont : Continuous F
y : α
hy : y ∈ ⋂ n, s n
x : (n : ι) → β n
hx : ∀ (n : ι), f n (x n) = y
n : ι
⊢ x ∈ {x | f n (x n) = f i₀ (x i₀)}
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isBounded_iff_subset_smul_closedBall {s : Set E} :
    Bornology.IsBounded s ↔ ∃ a : 𝕜, s ⊆ a • Metric.closedBall (0 : E) 1

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.closedBall 0 1) → Bornology.IsVonNBounded 𝕜 s

Tactic:
rintro ⟨a, ha⟩

Result:
case mpr.intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
a : 𝕜
ha : s ⊆ a • Metric.closedBall 0 1
⊢ Bornology.IsVonNBounded 𝕜 s

Proof state:
case mp
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.ball 0 1) → ∃ a, s ⊆ a • Metric.closedBall 0 1

Tactic:
exact Exists.imp fun a ha => ha.trans <| Set.smul_set_mono <| Metric.ball_subset_closedBall

Result:
no goals

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.closedBall 0 1) → Bornology.IsBounded s

Tactic:
rw [← isVonNBounded_iff 𝕜]

Result:
case mpr
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.closedBall 0 1) → Bornology.IsVonNBounded 𝕜 s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ ∃ a, s ⊆ a • Metric.closedBall 0 1

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s → ∃ a, s ⊆ a • Metric.closedBall 0 1

case mpr
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.closedBall 0 1) → Bornology.IsBounded s

Proof state:
case mpr.intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
a : 𝕜
ha : s ⊆ a • Metric.closedBall 0 1
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
exact ((isVonNBounded_closedBall 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha

Result:
no goals

Proof state:
case mp
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s → ∃ a, s ⊆ a • Metric.closedBall 0 1

Tactic:
rw [isBounded_iff_subset_smul_ball 𝕜]

Result:
case mp
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.ball 0 1) → ∃ a, s ⊆ a • Metric.closedBall 0 1
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem isBlock_subtypeVal {C : SubMulAction G X} {B : Set C} :
    IsBlock G (Subtype.val '' B : Set X) ↔ IsBlock G B

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g₁ g₂ : G
⊢ g₁ • Subtype.val '' B ≠ g₂ • Subtype.val '' B → Disjoint (g₁ • Subtype.val '' B) (g₂ • Subtype.val '' B) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)

Tactic:
rw [← SubMulAction.inclusion.coe_eq, ← image_smul_set, ← image_smul_set, ne_eq,
  Set.image_eq_image C.inclusion_injective, disjoint_image_iff C.inclusion_injective]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
⊢ IsBlock G (Subtype.val '' B) ↔ IsBlock G B

Tactic:
refine forall₂_congr fun g₁ g₂ ↦ ?_

Result:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
C : SubMulAction G X
B : Set ↥C
g₁ g₂ : G
⊢ g₁ • Subtype.val '' B ≠ g₂ • Subtype.val '' B → Disjoint (g₁ • Subtype.val '' B) (g₂ • Subtype.val '' B) ↔
    g₁ • B ≠ g₂ • B → Disjoint (g₁ • B) (g₂ • B)
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem inv_inv {x : tsze R M} (hx : fst x ≠ 0) : x⁻¹⁻¹ = x :=
  -- adapted from `Matrix.nonsing_inv_nonsing_inv`
  calc
    x⁻¹⁻¹ = 1 * x⁻¹⁻¹

Proof state:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹⁻¹ = 1 * x⁻¹⁻¹

Tactic:
rw [one_mul]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
⊢ 1 * x⁻¹⁻¹ = x * x⁻¹ * x⁻¹⁻¹

Tactic:
rw [TrivSqZeroExt.mul_inv_cancel hx]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
⊢ x.fst⁻¹ ≠ 0

Tactic:
apply inv_ne_zero hx

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹.fst ≠ 0

Tactic:
rw [fst_inv]

Result:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
⊢ x.fst⁻¹ ≠ 0

Proof state:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
⊢ x * x⁻¹ * x⁻¹⁻¹ = x

Tactic:
rw [mul_assoc, TrivSqZeroExt.mul_inv_cancel, mul_one]

Result:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹.fst ≠ 0