harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/InvariantBasisNumber.lean
theorem card_le_of_injective' [StrongRankCondition R] {α β : Type*} [Fintype α] [Fintype β]
    (f : (α →₀ R) →ₗ[R] β →₀ R) (i : Injective f) : Fintype.card α ≤ Fintype.card β

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
let Q := (Finsupp.linearEquivFunOnFinite R R α).symm

Result:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
Q : (α → R) ≃ₗ[R] α →₀ R := (Finsupp.linearEquivFunOnFinite R R α).symm
⊢ Fintype.card α ≤ Fintype.card β

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
Q : (α → R) ≃ₗ[R] α →₀ R := (Finsupp.linearEquivFunOnFinite R R α).symm
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
exact
  card_le_of_injective R ((P.toLinearMap.comp f).comp Q.toLinearMap)
    ((P.injective.comp i).comp Q.injective)

Result:
no goals

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
let P := Finsupp.linearEquivFunOnFinite R R β

Result:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
⊢ Fintype.card α ≤ Fintype.card β
-- Mathlib/RingTheory/Noetherian/Orzech.lean
theorem IsNoetherian.subsingleton_of_prod_injective (f : M × N →ₗ[R] M)
    (i : Injective f) : Subsingleton N := .intro fun x y ↦ by
  have h := IsNoetherian.injective_of_surjective_of_injective f _ i LinearMap.fst_surjective
  simpa using h (show LinearMap.fst R M N (0, x) = LinearMap.fst R M N (0, y) from rfl)

Proof state:
R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
f : M × N →ₗ[R] M
i : Injective ⇑f
x y : N
⊢ x = y

Tactic:
have h := IsNoetherian.injective_of_surjective_of_injective f _ i LinearMap.fst_surjective

Result:
R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
f : M × N →ₗ[R] M
i : Injective ⇑f
x y : N
h : Injective ⇑(LinearMap.fst R M N)
⊢ x = y

Proof state:
R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
f : M × N →ₗ[R] M
i : Injective ⇑f
x y : N
h : Injective ⇑(LinearMap.fst R M N)
⊢ x = y

Tactic:
simpa using h (show LinearMap.fst R M N (0, x) = LinearMap.fst R M N (0, y) from rfl)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem continuous_cosh : Continuous cosh

Proof state:
⊢ Continuous fun z => (cexp z + cexp (-z)) / 2

Tactic:
continuity

Result:
no goals

Proof state:
⊢ Continuous cosh

Tactic:
change Continuous fun z => (exp z + exp (-z)) / 2

Result:
⊢ Continuous fun z => (cexp z + cexp (-z)) / 2
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
@[simp] lemma memberSubfamily_image_erase : (𝒜.image (erase · a)).memberSubfamily a = ∅

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ memberSubfamily a (image (fun x => x.erase a) 𝒜) = ∅

Tactic:
simp [eq_empty_iff_forall_not_mem,
  (ne_of_mem_of_not_mem' (mem_insert_self _ _) (not_mem_erase _ _)).symm]

Result:
no goals
-- Mathlib/NumberTheory/EulerProduct/Basic.lean
/-- If `f` is multiplicative and summable, then its values at natural numbers `> 1`
have norm strictly less than `1`. -/
lemma Summable.norm_lt_one {F : Type*} [NormedField F] [CompleteSpace F] {f : ℕ →* F}
    (hsum : Summable f) {p : ℕ} (hp : 1 < p) :
    ‖f p‖ < 1

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
p : ℕ
hp : 1 < p
⊢ Summable fun n => f (p ^ n)

Tactic:
exact hsum.comp_injective <| Nat.pow_right_injective hp

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
p : ℕ
hp : 1 < p
⊢ Summable fun n => f p ^ n

Tactic:
simp_rw [← map_pow]

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
p : ℕ
hp : 1 < p
⊢ Summable fun n => f (p ^ n)

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
p : ℕ
hp : 1 < p
⊢ ‖f p‖ < 1

Tactic:
refine summable_geometric_iff_norm_lt_one.mp ?_

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
hsum : Summable ⇑f
p : ℕ
hp : 1 < p
⊢ Summable fun n => f p ^ n
-- Mathlib/Order/RelSeries.lean
@[simp] lemma head_snoc (p : RelSeries r) (newLast : α) (rel : r p.last newLast) :
    (p.snoc newLast rel).head = p.head

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
⊢ (p.snoc newLast rel).head = p.head

Tactic:
delta snoc

Result:
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
⊢ (p.append (singleton r newLast) rel).head = p.head

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
newLast : α
rel : r p.last newLast
⊢ (p.append (singleton r newLast) rel).head = p.head

Tactic:
rw [head_append]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem injOn_range (h : Semiconj f fa fb) (ha : Injective fa) (hf : InjOn f (range fa)) :
    InjOn fb (range f)

Proof state:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (fa '' univ)
⊢ InjOn fb (f '' univ)

Tactic:
exact h.injOn_image ha.injOn hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (range fa)
⊢ InjOn fb (range f)

Tactic:
rw [← image_univ] at *

Result:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (fa '' univ)
⊢ InjOn fb (f '' univ)
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem SameCycle.exists_pow_eq_of_mem_support_aux {f} [DecidableEq α] [Fintype α]
    [DecidableRel f.SameCycle] (h : SameCycle f x y) (hx : x ∈ f.support) :
    ∃ i < #(f.cycleOf x).support, (f ^ i) x = y

Proof state:
α : Type u_2
x y : α
f : Perm α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : f x ≠ x
⊢ y ∈ (f.cycleOf x).support

Tactic:
rwa [mem_support_cycleOf_iff'_aux hx]

Result:
no goals

Proof state:
α : Type u_2
x y : α
f : Perm α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : x ∈ f.support
⊢ ∃ i < #(f.cycleOf x).support, (f ^ i) x = y

Tactic:
rw [mem_support] at hx

Result:
α : Type u_2
x y : α
f : Perm α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : f x ≠ x
⊢ ∃ i < #(f.cycleOf x).support, (f ^ i) x = y

Proof state:
α : Type u_2
x y : α
f : Perm α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : f x ≠ x
⊢ ∃ i < #(f.cycleOf x).support, (f ^ i) x = y

Tactic:
exact Equiv.Perm.IsCycleOn.exists_pow_eq (b := y) (f.isCycleOn_support_cycleOf_aux x)
  (by rw [mem_support_cycleOf_iff'_aux hx]) (by rwa [mem_support_cycleOf_iff'_aux hx])

Result:
no goals

Proof state:
α : Type u_2
x y : α
f : Perm α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
hx : f x ≠ x
⊢ x ∈ (f.cycleOf x).support

Tactic:
rw [mem_support_cycleOf_iff'_aux hx]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/WithLp.lean
theorem differentiableWithinAt_piLp :
    DifferentiableWithinAt 𝕜 f t y ↔ ∀ i, DifferentiableWithinAt 𝕜 (fun x => f x i) t y

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
y : H
⊢ DifferentiableWithinAt 𝕜 f t y ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => f x i) t y

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiableWithinAt_iff,
  differentiableWithinAt_pi]

Result:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
y : H
⊢ (∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) t y) ↔
    ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => f x i) t y

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
y : H
⊢ (∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) t y) ↔
    ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => f x i) t y

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivWithinAt.clm_apply (hc : HasDerivWithinAt c c' s x)
    (hu : HasDerivWithinAt u u' s x) :
    HasDerivWithinAt (fun y => (c y) (u y)) (c' (u x) + c x u') s x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasDerivWithinAt c c' s x
hu : HasDerivWithinAt u u' s x
this : HasDerivWithinAt (fun y => (c y) (u y)) (((c x).comp (smulRight 1 u') + (smulRight 1 c').flip (u x)) 1) s x
⊢ HasDerivWithinAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') s x

Tactic:
rwa [add_apply, comp_apply, flip_apply, smulRight_apply, smulRight_apply, one_apply, one_smul,
  one_smul, add_comm] at this

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasDerivWithinAt c c' s x
hu : HasDerivWithinAt u u' s x
⊢ HasDerivWithinAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') s x

Tactic:
have := (hc.hasFDerivWithinAt.clm_apply hu.hasFDerivWithinAt).hasDerivWithinAt

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasDerivWithinAt c c' s x
hu : HasDerivWithinAt u u' s x
this : HasDerivWithinAt (fun y => (c y) (u y)) (((c x).comp (smulRight 1 u') + (smulRight 1 c').flip (u x)) 1) s x
⊢ HasDerivWithinAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') s x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem lt_of_getMsb?_eq_some (x : BitVec w) (i : Nat) : getMsb? x i = some b → i < w

Proof state:
w : Nat
b : Bool
x : BitVec w
i : Nat
⊢ x.getMsb? i = some b → i < w

Tactic:
if h : i < w then
  simp [h]
else
  simp [Nat.ge_of_not_lt h]

Result:
no goals

Proof state:
w : Nat
b : Bool
x : BitVec w
i : Nat
h : ¬i < w
⊢ x.getMsb? i = some b → i < w

Tactic:
simp [Nat.ge_of_not_lt h]

Result:
no goals

Proof state:
w : Nat
b : Bool
x : BitVec w
i : Nat
h : i < w
⊢ x.getMsb? i = some b → i < w

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem dite_prop_iff_or {Q : P → Prop} {R : ¬P → Prop} :
    dite P Q R ↔ (∃ p, Q p) ∨ (∃ p, R p)

Proof state:
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
⊢ dite P Q R ↔ (∃ p, Q p) ∨ ∃ p, R p

Tactic:
by_cases h : P <;> simp [h, exists_prop_of_false, exists_prop_of_true]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffWithinAt_insert_self :
    ContDiffWithinAt 𝕜 n f (insert x s) x ↔ ContDiffWithinAt 𝕜 n f s x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
⊢ ContDiffWithinAt 𝕜 n f (insert x s) x ↔ ContDiffWithinAt 𝕜 n f s x

Tactic:
match n with
| ω => simp [ContDiffWithinAt]
| (n : ℕ∞) => simp_rw [ContDiffWithinAt, insert_idem]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
⊢ ContDiffWithinAt 𝕜 ω f (insert x s) x ↔ ContDiffWithinAt 𝕜 ω f s x

Tactic:
simp [ContDiffWithinAt]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n✝ : WithTop ℕ∞
n : ℕ∞
⊢ ContDiffWithinAt 𝕜 (↑n) f (insert x s) x ↔ ContDiffWithinAt 𝕜 (↑n) f s x

Tactic:
simp_rw [ContDiffWithinAt, insert_idem]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem map_sub (f : M →SL[σ₁₂] M₂) (x y : M) : f (x - y) = f x - f y

Proof state:
R : Type u_1
inst✝⁷ : Ring R
R₂ : Type u_2
inst✝⁶ : Ring R₂
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommGroup M
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →SL[σ₁₂] M₂
x y : M
⊢ f (x - y) = f x - f y

Tactic:
exact map_sub f x y

Result:
no goals
-- Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
theorem image_mem_nhds (hf : ApproximatesLinearOn f f' s c) (f'symm : f'.NonlinearRightInverse)
    {x : E} (hs : s ∈ 𝓝 x) (hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹) : f '' s ∈ 𝓝 (f x)

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
hts : t ⊆ s
ht : IsOpen t
xt : x ∈ t
⊢ f '' s ∈ 𝓝 (f x)

Tactic:
have := IsOpen.mem_nhds ((hf.mono_set hts).open_image f'symm ht hc) (mem_image_of_mem _ xt)

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
hts : t ⊆ s
ht : IsOpen t
xt : x ∈ t
this : f '' t ∈ 𝓝 (f x)
⊢ f '' s ∈ 𝓝 (f x)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
⊢ f '' s ∈ 𝓝 (f x)

Tactic:
obtain ⟨t, hts, ht, xt⟩ : ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t := _root_.mem_nhds_iff.1 hs

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
hts : t ⊆ s
ht : IsOpen t
xt : x ∈ t
⊢ f '' s ∈ 𝓝 (f x)

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
hts : t ⊆ s
ht : IsOpen t
xt : x ∈ t
this : f '' t ∈ 𝓝 (f x)
⊢ f '' s ∈ 𝓝 (f x)

Tactic:
exact mem_of_superset this (image_subset _ hts)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toFin_ofBool (b : Bool) : (ofBool b).toFin = Fin.ofNat' 2 (b.toNat)

Proof state:
b : Bool
⊢ (ofBool b).toFin = Fin.ofNat' 2 b.toNat

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/SetTheory/Nimber/Field.lean
theorem two_zsmul (x : Nimber) : (2 : ℤ) • x = 0

Proof state:
x : Nimber
⊢ 2 • x = 0

Tactic:
rw [_root_.two_zsmul]

Result:
x : Nimber
⊢ x + x = 0

Proof state:
x : Nimber
⊢ x + x = 0

Tactic:
exact add_self x

Result:
no goals
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_sub (a b : α) : |a - b| ≤ |a| + |b|

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ |a - b| ≤ |a| + |b|

Tactic:
rw [sub_eq_add_neg, ← abs_neg b]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ |a + -b| ≤ |a| + |(-b)|

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ |a + -b| ≤ |a| + |(-b)|

Tactic:
exact abs_add a _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_singleton (a : α) (i : Nat) : #[a][i]? = if i = 0 then some a else none

Proof state:
α : Type u_1
a : α
i : Nat
⊢ #[a][i]? = if i = 0 then some a else none

Tactic:
simp [List.getElem?_singleton]

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

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

Tactic:
rw [Units.mul_inv_eq_iff_eq_mul, one_mul, coe_liftRight]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem exists_nonneg_right_iff_sameRay (hy : y ≠ 0) :
    (∃ r : R, 0 ≤ r ∧ x = r • y) ↔ SameRay R x y

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R x y

Tactic:
rw [SameRay.sameRay_comm]

Result:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R y x

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R y x

Tactic:
simp_rw [eq_comm (a := x)]

Result:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ r • y = x) ↔ SameRay R y x

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hy : y ≠ 0
⊢ (∃ r, 0 ≤ r ∧ r • y = x) ↔ SameRay R y x

Tactic:
exact exists_nonneg_left_iff_sameRay (R := R) hy

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/Banach.lean
theorem nonlinearRightInverseOfSurjective_nnnorm_pos (f : E →SL[σ] F)
    (hsurj : LinearMap.range f = ⊤) : 0 < (nonlinearRightInverseOfSurjective f hsurj).nnnorm

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →SL[σ] F
hsurj : LinearMap.range f = ⊤
⊢ 0 < (Classical.choose ⋯).nnnorm

Tactic:
exact Classical.choose_spec (exists_nonlinearRightInverse_of_surjective f hsurj)

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →SL[σ] F
hsurj : LinearMap.range f = ⊤
⊢ 0 < (f.nonlinearRightInverseOfSurjective hsurj).nnnorm

Tactic:
rw [nonlinearRightInverseOfSurjective]

Result:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →SL[σ] F
hsurj : LinearMap.range f = ⊤
⊢ 0 < (Classical.choose ⋯).nnnorm
-- Mathlib/Data/List/Iterate.lean
theorem take_iterate (f : α → α) (a : α) (m n : ℕ) :
    take m (iterate f a n) = iterate f a (min m n)

Proof state:
α : Type u_1
f : α → α
a : α
m n : ℕ
⊢ take m (iterate f a n) = iterate f a (m ⊓ n)

Tactic:
rw [← range_map_iterate, ← range_map_iterate, ← map_take, take_range]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
lemma shiftFunctorZero_inv_app_f (K : CochainComplex C ℤ) (n : ℤ) :
    ((CategoryTheory.shiftFunctorZero (CochainComplex C ℤ) ℤ).inv.app K).f n =
      (K.XIsoOfEq (by dsimp; rw [add_zero])).hom := rfl

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
n : ℤ
⊢ n = n + 0

Tactic:
rw [add_zero]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
n : ℤ
⊢ n = n + { as := 0 }.as

Tactic:
dsimp

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
n : ℤ
⊢ n = n + 0
-- Mathlib/Analysis/Convex/Intrinsic.lean
theorem intrinsicInterior_empty : intrinsicInterior 𝕜 (∅ : Set P) = ∅

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

Tactic:
simp [intrinsicInterior]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem tail_cons (a : α) (s) : tail (cons a s) = s

Proof state:
case mk
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ (cons a ⟨f, al⟩).tail = ⟨f, al⟩

Tactic:
apply Subtype.eq

Result:
case mk.a
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ ↑(cons a ⟨f, al⟩).tail = ↑⟨f, al⟩

Proof state:
α : Type u
a : α
s : Seq α
⊢ (cons a s).tail = s

Tactic:
obtain ⟨f, al⟩ := s

Result:
case mk
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ (cons a ⟨f, al⟩).tail = ⟨f, al⟩

Proof state:
case mk.a
α : Type u
a : α
f : Stream' (Option α)
al : f.IsSeq
⊢ ↑(cons a ⟨f, al⟩).tail = ↑⟨f, al⟩

Tactic:
dsimp [tail, cons]

Result:
no goals