harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/TMToPartrec.lean
theorem trStmts₁_supports {S q} (H₁ : (q : Λ').Supports S) (HS₁ : trStmts₁ q ⊆ S) :
    Supports (trStmts₁ q) S

Proof state:
case succ.intro
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
h₂ : unrev q ∈ S ∧ ∀ a ∈ trStmts₁ q, a ∈ S
⊢ Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S

Tactic:
refine supports_insert.2 ⟨⟨fun _ => h₁, fun _ => h₂.1, fun _ => h₂.1⟩, ?_⟩

Result:
case succ.intro
S : Finset Λ'
W : ∀ {q : Λ'}, q ∈ trStmts₁ q
q : Λ'
q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S
H₁ : Λ'.Supports S q.succ
HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S
h₁ : q.succ ∈ S
h₂ : unrev q ∈ S ∧ ∀ a ∈ trStmts₁ q, a ∈ S
⊢ Supports (insert (unrev q) (trStmts₁ q)) S
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
/-- `t` is in the shadow of `𝒜` iff we can add an element to it so that the resulting finset is in
`𝒜`. -/
lemma mem_shadow_iff_insert_mem : t ∈ ∂ 𝒜 ↔ ∃ a ∉ t, insert a t ∈ 𝒜

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ (∃ s ∈ 𝒜, ∃ a ∉ t, insert a t = s) ↔ ∃ a ∉ t, insert a t ∈ 𝒜

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂ 𝒜 ↔ ∃ a ∉ t, insert a t ∈ 𝒜

Tactic:
simp_rw [mem_shadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ (∃ s ∈ 𝒜, ∃ a ∉ t, insert a t = s) ↔ ∃ a ∉ t, insert a t ∈ 𝒜
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem sub_eq_sub_min (n m : Nat) : n - m = n - min n m

Proof state:
n m : Nat
⊢ n - m = n - min n m

Tactic:
cases Nat.le_total n m with
| inl h => rw [Nat.min_eq_left h, Nat.sub_eq_zero_of_le h, Nat.sub_self]
| inr h => rw [Nat.min_eq_right h]

Result:
no goals

Proof state:
case inl
n m : Nat
h : n ≤ m
⊢ n - m = n - min n m

Tactic:
rw [Nat.min_eq_left h, Nat.sub_eq_zero_of_le h, Nat.sub_self]

Result:
no goals

Proof state:
case inr
n m : Nat
h : m ≤ n
⊢ n - m = n - min n m

Tactic:
rw [Nat.min_eq_right h]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem finSuccEquiv_coeff_coeff (m : Fin n →₀ ℕ) (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ) :
    coeff m (Polynomial.coeff (finSuccEquiv R n f) i) = coeff (m.cons i) f

Proof state:
case h1
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ coeff m (((finSuccEquiv R n) ((monomial j) r)).coeff i) = coeff (cons i m) ((monomial j) r)

Tactic:
simp only [finSuccEquiv_apply, coe_eval₂Hom, eval₂_monomial, RingHom.coe_comp, Finsupp.prod_pow,
  Polynomial.coeff_C_mul, coeff_C_mul, coeff_monomial, Fin.prod_univ_succ, Fin.cases_zero,
  Fin.cases_succ, ← map_prod, ← RingHom.map_pow, Function.comp_apply]

Result:
case h1
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r * coeff m ((Polynomial.X ^ j 0 * Polynomial.C (∏ x : Fin n, X x ^ j x.succ)).coeff i) =
    if j = cons i m then r else 0

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (j 0) m
⊢ m ≠ j.tail

Tactic:
rintro rfl

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ cons (j 0) j.tail
⊢ False
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_comm (f : M → N) (x y : M) : polar f x y = polar f y x

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ polar f x y = polar f y x

Tactic:
rw [polar, polar, add_comm, sub_sub, sub_sub, add_comm (f x) (f y)]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
theorem posSemidef_lapMatrix [LinearOrderedField R] [StarRing R]
    [TrivialStar R] : PosSemidef (G.lapMatrix R)

Proof state:
V : Type u_1
R : Type u_2
inst✝⁵ : Fintype V
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : LinearOrderedField R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
⊢ (lapMatrix R G).PosSemidef

Tactic:
constructor

Result:
case left
V : Type u_1
R : Type u_2
inst✝⁵ : Fintype V
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : LinearOrderedField R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
⊢ (lapMatrix R G).IsHermitian

case right
V : Type u_1
R : Type u_2
inst✝⁵ : Fintype V
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : LinearOrderedField R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
⊢ ∀ (x : V → R), 0 ≤ star x ⬝ᵥ lapMatrix R G *ᵥ x

Proof state:
case right
V : Type u_1
R : Type u_2
inst✝⁵ : Fintype V
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : LinearOrderedField R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
⊢ ∀ (x : V → R), 0 ≤ star x ⬝ᵥ lapMatrix R G *ᵥ x

Tactic:
intro x

Result:
case right
V : Type u_1
R : Type u_2
inst✝⁵ : Fintype V
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : LinearOrderedField R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
x : V → R
⊢ 0 ≤ star x ⬝ᵥ lapMatrix R G *ᵥ x

Proof state:
case left
V : Type u_1
R : Type u_2
inst✝⁵ : Fintype V
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : LinearOrderedField R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
⊢ (lapMatrix R G).IsHermitian

Tactic:
rw [IsHermitian, conjTranspose_eq_transpose_of_trivial, isSymm_lapMatrix]

Result:
no goals

Proof state:
case right
V : Type u_1
R : Type u_2
inst✝⁵ : Fintype V
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : LinearOrderedField R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
x : V → R
⊢ 0 ≤ (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Tactic:
positivity

Result:
no goals

Proof state:
case right
V : Type u_1
R : Type u_2
inst✝⁵ : Fintype V
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : LinearOrderedField R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
x : V → R
⊢ 0 ≤ star x ⬝ᵥ lapMatrix R G *ᵥ x

Tactic:
rw [star_trivial, ← toLinearMap₂'_apply', lapMatrix_toLinearMap₂']

Result:
case right
V : Type u_1
R : Type u_2
inst✝⁵ : Fintype V
G : SimpleGraph V
inst✝⁴ : DecidableRel G.Adj
inst✝³ : DecidableEq V
inst✝² : LinearOrderedField R
inst✝¹ : StarRing R
inst✝ : TrivialStar R
x : V → R
⊢ 0 ≤ (∑ i : V, ∑ j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem _root_.QuadraticMap.toQuadraticMap_polarBilin (Q : QuadraticMap R M N) :
    toQuadraticMap (polarBilin Q) = 2 • Q :=
  QuadraticMap.ext fun x => (polar_self _ x).trans <| by simp

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ 2 • Q x = (2 • Q) x

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.tendsto_nhds (hp : WithSeminorms p) (u : F → E) {f : Filter F} (y₀ : E) :
    Filter.Tendsto u f (𝓝 y₀) ↔ ∀ i ε, 0 < ε → ∀ᶠ x in f, p i (u x - y₀) < ε

Proof state:
𝕜 : Type u_1
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
⊢ (∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (s.sup p) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i) (u x - y₀) < ε

Tactic:
exact
  ⟨fun h i => by simpa only [Finset.sup_singleton] using h {i}, fun h s ε hε =>
    (s.eventually_all.2 fun i _ => h i ε hε).mono fun _ => finset_sup_apply_lt hε⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
⊢ Tendsto u f (𝓝 y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i) (u x - y₀) < ε

Tactic:
rw [hp.tendsto_nhds' u y₀]

Result:
𝕜 : Type u_1
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
⊢ (∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (s.sup p) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i) (u x - y₀) < ε

Proof state:
𝕜 : Type u_1
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
h : ∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (s.sup p) (u x - y₀) < ε
i : ι
⊢ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (p i) (u x - y₀) < ε

Tactic:
simpa only [Finset.sup_singleton] using h {i}

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_map [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    {f : (a : α) → β a → δ a} (h : Raw.WFImp m.1) : Raw.WFImp (m.map f).1

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → δ a
h : Raw.WFImp m.val
⊢ Raw.WFImp (map f m).val

Tactic:
rw [map_eq_mapₘ]

Result:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → δ a
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.mapₘ f).val

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
f : (a : α) → β a → δ a
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.mapₘ f).val

Tactic:
exact wfImp_mapₘ h

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem toSpanSingleton_zero : toSpanSingleton R M 0 = 0

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ toSpanSingleton R M 0 = 0

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (toSpanSingleton R M 0) 1 = 0 1

Proof state:
case h
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (toSpanSingleton R M 0) 1 = 0 1

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem isAtom_of_map_bot_of_image [OrderBot α] [OrderBot β] (f : β ↪o α) (hbot : f ⊥ = ⊥) {b : β}
    (hb : IsAtom (f b)) : IsAtom b

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
f : β ↪o α
hbot : f ⊥ = ⊥
b : β
hb : IsAtom (f b)
⊢ IsAtom b

Tactic:
simp only [← bot_covBy_iff] at hb ⊢

Result:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
f : β ↪o α
hbot : f ⊥ = ⊥
b : β
hb : ⊥ ⋖ f b
⊢ ⊥ ⋖ b

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
f : β ↪o α
hbot : f ⊥ = ⊥
b : β
hb : ⊥ ⋖ f b
⊢ ⊥ ⋖ b

Tactic:
exact CovBy.of_image f (hbot.symm ▸ hb)

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Hom.lean
theorem lift_apply_mk' (f : c.Quotient →* P) :
    (c.lift (f.comp c.mk') fun x y h => show f ↑x = f ↑y by rw [c.eq.2 h]) = f

Proof state:
case h.mk
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : c.Quotient →* P
x : c.Quotient
a✝ : M
⊢ (c.lift (f.comp c.mk') ⋯) (Quot.mk (⇑c.toSetoid) a✝) = f (Quot.mk (⇑c.toSetoid) a✝)

Tactic:
rfl

Result:
no goals

Proof state:
case h
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : c.Quotient →* P
x : c.Quotient
⊢ (c.lift (f.comp c.mk') ⋯) x = f x

Tactic:
rcases x with ⟨⟩

Result:
case h.mk
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : c.Quotient →* P
x : c.Quotient
a✝ : M
⊢ (c.lift (f.comp c.mk') ⋯) (Quot.mk (⇑c.toSetoid) a✝) = f (Quot.mk (⇑c.toSetoid) a✝)

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f✝ : M →* P
f : c.Quotient →* P
x y : M
h : c x y
⊢ f ↑x = f ↑y

Tactic:
rw [c.eq.2 h]

Result:
no goals

Proof state:
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : c.Quotient →* P
⊢ c.lift (f.comp c.mk') ⋯ = f

Tactic:
ext x

Result:
case h
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : c.Quotient →* P
x : c.Quotient
⊢ (c.lift (f.comp c.mk') ⋯) x = f x
-- Mathlib/Data/List/Perm/Basic.lean
theorem map_perm_map_iff {l' : List α} {f : α → β} (hf : f.Injective) :
    map f l ~ map f l' ↔ l ~ l' := calc
  map f l ~ map f l' ↔ Relation.Comp (· = map f ·) (· ~ ·) (map f l) l'

Proof state:
α : Type u_1
β : Type u_2
l l' : List α
f : α → β
hf : Function.Injective f
⊢ Relation.Comp (fun x1 x2 => x1 = map f x2) (fun x1 x2 => x1 ~ x2) (map f l) l' ↔ l ~ l'

Tactic:
simp [Relation.Comp, map_inj_right hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l l' : List α
f : α → β
hf : Function.Injective f
⊢ map f l ~ map f l' ↔ Relation.Comp (fun x1 x2 => x1 = map f x2) (fun x1 x2 => x1 ~ x2) (map f l) l'

Tactic:
rw [eq_map_comp_perm]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
/-- If a `C^2` map has an invertible derivative at a point, then nearby derivatives can be written
as continuous linear equivs, which depend in a `C^1` way on the point, as well as their inverse, and
moreover one can compute the derivative of the inverse. -/
lemma _root_.exists_continuousLinearEquiv_fderiv_symm_eq
    {f : E → F} {x : E} (h'f : ContDiffAt 𝕜 2 f x) (hf : (fderiv 𝕜 f x).IsInvertible) :
    ∃ N : E → (E ≃L[𝕜] F), ContDiffAt 𝕜 1 (fun y ↦ (N y : E →L[𝕜] F)) x
    ∧ ContDiffAt 𝕜 1 (fun y ↦ ((N y).symm : F →L[𝕜] E)) x
    ∧ (∀ᶠ y in 𝓝 x, N y = fderiv 𝕜 f y)
    ∧ ∀ v, fderiv 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) x v
      = - (N x).symm  ∘L ((fderiv 𝕜 (fderiv 𝕜 f) x v)) ∘L (N x).symm

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
inst✝ : CompleteSpace E
f : E → F
x : E
hf : (fderivWithin 𝕜 f univ x).IsInvertible
h'f : ContDiffWithinAt 𝕜 2 f univ x
⊢ ∃ N,
    ContDiffWithinAt 𝕜 1 (fun y => ↑(N y)) univ x ∧
      ContDiffWithinAt 𝕜 1 (fun y => ↑(N y).symm) univ x ∧
        (∀ᶠ (y : E) in 𝓝[univ] x, ↑(N y) = fderivWithin 𝕜 f univ y) ∧
          ∀ (v : E),
            (fderivWithin 𝕜 (fun y => ↑(N y).symm) univ x) v =
              -(↑(N x).symm).comp (((fderivWithin 𝕜 (fderivWithin 𝕜 f univ) univ x) v).comp ↑(N x).symm)

Tactic:
exact exists_continuousLinearEquiv_fderivWithin_symm_eq h'f hf uniqueDiffOn_univ (mem_univ _)

Result:
no goals

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
inst✝ : CompleteSpace E
f : E → F
x : E
h'f : ContDiffAt 𝕜 2 f x
hf : (fderiv 𝕜 f x).IsInvertible
⊢ ∃ N,
    ContDiffAt 𝕜 1 (fun y => ↑(N y)) x ∧
      ContDiffAt 𝕜 1 (fun y => ↑(N y).symm) x ∧
        (∀ᶠ (y : E) in 𝓝 x, ↑(N y) = fderiv 𝕜 f y) ∧
          ∀ (v : E),
            (fderiv 𝕜 (fun y => ↑(N y).symm) x) v = -(↑(N x).symm).comp (((fderiv 𝕜 (fderiv 𝕜 f) x) v).comp ↑(N x).symm)

Tactic:
simp only [← fderivWithin_univ, ← contDiffWithinAt_univ, ← nhdsWithin_univ] at hf h'f ⊢

Result:
𝕜 : 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
inst✝ : CompleteSpace E
f : E → F
x : E
hf : (fderivWithin 𝕜 f univ x).IsInvertible
h'f : ContDiffWithinAt 𝕜 2 f univ x
⊢ ∃ N,
    ContDiffWithinAt 𝕜 1 (fun y => ↑(N y)) univ x ∧
      ContDiffWithinAt 𝕜 1 (fun y => ↑(N y).symm) univ x ∧
        (∀ᶠ (y : E) in 𝓝[univ] x, ↑(N y) = fderivWithin 𝕜 f univ y) ∧
          ∀ (v : E),
            (fderivWithin 𝕜 (fun y => ↑(N y).symm) univ x) v =
              -(↑(N x).symm).comp (((fderivWithin 𝕜 (fderivWithin 𝕜 f univ) univ x) v).comp ↑(N x).symm)
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem self_eq_mass_smul_normalize : μ = μ.mass • μ.normalize.toFiniteMeasure

Proof state:
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ μ = μ.mass • μ.normalize.toFiniteMeasure

Tactic:
apply eq_of_forall_apply_eq

Result:
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ ∀ (s : Set Ω), MeasurableSet s → μ s = (μ.mass • μ.normalize.toFiniteMeasure) s

Proof state:
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ μ s = (μ.mass • μ.normalize.toFiniteMeasure) s

Tactic:
rw [μ.self_eq_mass_mul_normalize s, smul_apply, smul_eq_mul,
  ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn]

Result:
no goals

Proof state:
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ ∀ (s : Set Ω), MeasurableSet s → μ s = (μ.mass • μ.normalize.toFiniteMeasure) s

Tactic:
intro s _s_mble

Result:
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ μ s = (μ.mass • μ.normalize.toFiniteMeasure) s
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_zero [Nontrivial R] : rank (0 : Matrix m n R) = 0

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ rank 0 = 0

Tactic:
rw [rank, mulVecLin_zero, LinearMap.range_zero, finrank_bot]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_one_add_smoothingFn_r_pos : ∀ᶠ (n : ℕ) in atTop, ∀ i, 0 < 1 + ε (r i n)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < 1 + ε ↑(r i n)

Tactic:
rw [Filter.eventually_all]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < 1 + ε ↑(r i x)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < 1 + ε ↑(r i x)

Tactic:
exact fun i => (R.tendsto_atTop_r i).eventually (f := r i) eventually_one_add_smoothingFn_pos

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
theorem HigherFacesVanish.on_Γ₀_summand_id (K : ChainComplex C ℕ) (n : ℕ) :
    @HigherFacesVanish C _ _ (Γ₀.obj K) _ n (n + 1)
      (((Γ₀.splitting K).cofan _).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)))

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫ (Γ₀.obj K).δ j.succ = 0

Tactic:
rw [Γ₀.Obj.Termwise.mapMono_eq_zero K, zero_comp] at eq

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op =
    0
⊢ ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫ (Γ₀.obj K).δ j.succ = 0

case h₁
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ ⦋n + 1⦌ ≠ ⦋n⦌

case h₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
j : Fin (n + 1)
a✝ : n + 1 ≤ ↑j + (n + 1)
eq :
  ((Γ₀.splitting K).cofan (op ⦋n + 1⦌)).inj (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op =
    Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))
⊢ ¬Isδ₀ (SimplexCategory.δ j.succ)
-- Mathlib/Data/Nat/Init.lean
protected lemma div_le_div_of_mul_le_mul (hd : d ≠ 0) (hdc : d ∣ c) (h : a * d ≤ c * b) :
    a / b ≤ c / d :=
  Nat.div_le_of_le_mul' <| by
    rwa [← Nat.mul_div_assoc _ hdc, Nat.le_div_iff_mul_le (Nat.pos_iff_ne_zero.2 hd), b.mul_comm]

Proof state:
a b c d : ℕ
hd : d ≠ 0
hdc : d ∣ c
h : a * d ≤ c * b
⊢ a ≤ b * (c / d)

Tactic:
rwa [← Nat.mul_div_assoc _ hdc, Nat.le_div_iff_mul_le (Nat.pos_iff_ne_zero.2 hd), b.mul_comm]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem toSubfield_injective : Function.Injective (toSubfield : IntermediateField K L → _)

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ a₂✝ : IntermediateField K L
h : a₁✝.toSubfield = a₂✝.toSubfield
x✝ : L
⊢ x✝ ∈ a₁✝ ↔ x✝ ∈ a₂✝

Tactic:
simp_rw [← mem_toSubfield, h]

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Function.Injective toSubfield

Tactic:
intro _ _ h

Result:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ a₂✝ : IntermediateField K L
h : a₁✝.toSubfield = a₂✝.toSubfield
⊢ a₁✝ = a₂✝

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ a₂✝ : IntermediateField K L
h : a₁✝.toSubfield = a₂✝.toSubfield
⊢ a₁✝ = a₂✝

Tactic:
ext

Result:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
a₁✝ a₂✝ : IntermediateField K L
h : a₁✝.toSubfield = a₂✝.toSubfield
x✝ : L
⊢ x✝ ∈ a₁✝ ↔ x✝ ∈ a₂✝