harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem fill_toFin {w : Nat} {v : Bool} :
    (fill w v).toFin = if v = true then (allOnes w).toFin else Fin.ofNat' (2 ^ w) 0

Proof state:
w : Nat
v : Bool
⊢ (fill w v).toFin = if v = true then (allOnes w).toFin else Fin.ofNat' (2 ^ w) 0

Tactic:
by_cases h : v <;> simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem getElem_mapFinIdx (a : Vector α n) (f : (i : Nat) → α → (h : i < n) → β) (i : Nat)
    (h : i < n) :
    (a.mapFinIdx f)[i] = f i a[i] h

Proof state:
case mk
α : Type u_1
β : Type u_2
i : Nat
a : Array α
f : (i : Nat) → α → i < a.size → β
h : i < a.size
⊢ ({ toArray := a, size_toArray := ⋯ }.mapFinIdx f)[i] = f i { toArray := a, size_toArray := ⋯ }[i] h

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
a : Vector α n
f : (i : Nat) → α → i < n → β
i : Nat
h : i < n
⊢ (a.mapFinIdx f)[i] = f i a[i] h

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
i : Nat
a : Array α
f : (i : Nat) → α → i < a.size → β
h : i < a.size
⊢ ({ toArray := a, size_toArray := ⋯ }.mapFinIdx f)[i] = f i { toArray := a, size_toArray := ⋯ }[i] h
-- Mathlib/Data/List/Chain.lean
theorem Chain'.rel_head? {x l} (h : Chain' R (x :: l)) ⦃y⦄ (hy : y ∈ head? l) : R x y

Proof state:
α : Type u
R : α → α → Prop
x : α
l : List α
h : Chain' R (x :: l)
y : α
hy : y ∈ l.head?
⊢ R x y

Tactic:
rw [← cons_head?_tail hy] at h

Result:
α : Type u
R : α → α → Prop
x : α
l : List α
y : α
h : Chain' R (x :: y :: l.tail)
hy : y ∈ l.head?
⊢ R x y

Proof state:
α : Type u
R : α → α → Prop
x : α
l : List α
y : α
h : Chain' R (x :: y :: l.tail)
hy : y ∈ l.head?
⊢ R x y

Tactic:
exact h.rel_head

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem symm_apply_mk_proj {x : Z} (ex : x ∈ e.source) :
    e.toPartialEquiv.symm (proj x, (e x).2) = x

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : Z
ex : x ∈ e.source
⊢ ↑e.symm (proj x, (↑e x).2) = x

Tactic:
rw [← e.coe_fst ex, ← e.coe_coe, e.left_inv ex]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
@[to_additive]
lemma Topology.IsInducing.multipliable_iff_tprod_comp_mem_range [CommMonoid γ] [TopologicalSpace γ]
    [T2Space γ] {G} [FunLike G α γ] [MonoidHomClass G α γ] {g : G} (hg : IsInducing g) (f : β → α) :
    Multipliable f ↔ Multipliable (g ∘ f) ∧ ∏' i, g (f i) ∈ Set.range g

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hgf : Multipliable (⇑g ∘ f)
a : α
ha : g a = ∏' (i : β), g (f i)
this : HasProd (⇑g ∘ f) (g a)
⊢ HasProd f a

Tactic:
exact (hg.hasProd_iff f a).mp this

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
lemma integrable_left_of_integrable_add_of_nonneg {f g : α → ℝ}
    (h_meas : AEStronglyMeasurable f μ) (hf : 0 ≤ᵐ[μ] f) (hg : 0 ≤ᵐ[μ] g)
    (h_int : Integrable (f + g) μ) : Integrable f μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
hg : 0 ≤ᶠ[ae μ] g
h_int : Integrable (f + g) μ
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ (f + g) a

Tactic:
filter_upwards [hf, hg] with a haf hag

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
hg : 0 ≤ᶠ[ae μ] g
h_int : Integrable (f + g) μ
a : α
haf : 0 a ≤ f a
hag : 0 a ≤ g a
⊢ ‖f a‖ ≤ (f + g) a

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
hg : 0 ≤ᶠ[ae μ] g
h_int : Integrable (f + g) μ
⊢ Integrable f μ

Tactic:
refine h_int.mono' h_meas ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
hg : 0 ≤ᶠ[ae μ] g
h_int : Integrable (f + g) μ
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ (f + g) a

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᶠ[ae μ] f
hg : 0 ≤ᶠ[ae μ] g
h_int : Integrable (f + g) μ
a : α
haf : 0 a ≤ f a
hag : 0 a ≤ g a
⊢ ‖f a‖ ≤ (f + g) a

Tactic:
exact (Real.norm_of_nonneg haf).symm ▸ le_add_of_nonneg_right hag

Result:
no goals
-- Mathlib/Control/Traversable/Equiv.lean
theorem naturality (f : α → F β) (x : t' α) :
    η (Equiv.traverse eqv f x) = Equiv.traverse eqv (@η _ ∘ f) x

Proof state:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
x : t' α
⊢ (fun {α} => η.app α) (Equiv.traverse eqv f x) = Equiv.traverse eqv ((fun {α} => η.app α) ∘ f) x

Tactic:
simp only [Equiv.traverse, functor_norm]

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
lemma isMinOn_of_rightDeriv_eq_zero (hf : ConvexOn ℝ S f) (hx : x ∈ interior S)
    (hf_rd : derivWithin f (Ioi x) x = 0) :
    IsMinOn f S x

Proof state:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_rd : derivWithin f (Ioi x) x = 0
⊢ derivWithin f (Iio x) x ≤ 0

Tactic:
exact (hf.leftDeriv_le_rightDeriv_of_mem_interior hx).trans_eq hf_rd

Result:
no goals

Proof state:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_rd : derivWithin f (Ioi x) x = 0
⊢ IsMinOn f S x

Tactic:
refine hf.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg hx ?_ hf_rd.symm.le

Result:
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_rd : derivWithin f (Ioi x) x = 0
⊢ derivWithin f (Iio x) x ≤ 0
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma nonsingular_zero [Nontrivial R] : W'.Nonsingular ![0, 1, 0]

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : Nontrivial R
h : 3 * 0 ^ 2 = 0 ∧ 1 ^ 2 + W'.a₁ * 0 * 1 - W'.a₂ * 0 ^ 2 = 0
⊢ 1 = 0

Tactic:
linear_combination (norm := ring1) h.right

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : Nontrivial R
⊢ ¬(3 * 0 ^ 2 = 0 ∧ 1 ^ 2 + W'.a₁ * 0 * 1 - W'.a₂ * 0 ^ 2 = 0)

Tactic:
exact fun h => one_ne_zero <| by linear_combination (norm := ring1) h.right

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : Nontrivial R
⊢ W'.Nonsingular ![0, 1, 0]

Tactic:
simp only [nonsingular_of_Z_eq_zero, equation_zero, true_and, fin3_def_ext, ← not_and_or]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : Nontrivial R
⊢ ¬(3 * 0 ^ 2 = 0 ∧ 1 ^ 2 + W'.a₁ * 0 * 1 - W'.a₂ * 0 ^ 2 = 0)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem umod_eq_divRec (hd : 0#w < d) :
    let out := divRec w {n, d} (DivModState.init w)
    n % d = out.r

Proof state:
w : Nat
d n : BitVec w
hd : 0#w < d
this : DivModState.Lawful { n := n, d := d } (DivModState.init w)
⊢ let out := divRec w { n := n, d := d } (DivModState.init w);
  n % d = out.r

Tactic:
have := lawful_divRec this

Result:
w : Nat
d n : BitVec w
hd : 0#w < d
this✝ : DivModState.Lawful { n := n, d := d } (DivModState.init w)
this : DivModState.Lawful { n := n, d := d } (divRec (DivModState.init w).wn { n := n, d := d } (DivModState.init w))
⊢ let out := divRec w { n := n, d := d } (DivModState.init w);
  n % d = out.r

Proof state:
w : Nat
d n : BitVec w
hd : 0#w < d
⊢ let out := divRec w { n := n, d := d } (DivModState.init w);
  n % d = out.r

Tactic:
have := DivModState.lawful_init {n, d} hd

Result:
w : Nat
d n : BitVec w
hd : 0#w < d
this : DivModState.Lawful { n := n, d := d } (DivModState.init w)
⊢ let out := divRec w { n := n, d := d } (DivModState.init w);
  n % d = out.r

Proof state:
w : Nat
d n : BitVec w
hd : 0#w < d
this✝ : DivModState.Lawful { n := n, d := d } (DivModState.init w)
this : DivModState.Lawful { n := n, d := d } (divRec (DivModState.init w).wn { n := n, d := d } (DivModState.init w))
⊢ let out := divRec w { n := n, d := d } (DivModState.init w);
  n % d = out.r

Tactic:
apply DivModState.umod_eq_of_lawful this (wn_divRec ..)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem any_push [BEq α] {as : Vector α n} {a : α} {p : α → Bool} :
    (as.push a).any p = (as.any p || p a)

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
p : α → Bool
as : Array α
⊢ ({ toArray := as, size_toArray := ⋯ }.push a).any p = ({ toArray := as, size_toArray := ⋯ }.any p || p a)

Tactic:
simp [Array.any_push]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
as : Vector α n
a : α
p : α → Bool
⊢ (as.push a).any p = (as.any p || p a)

Tactic:
rcases as with ⟨as, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
p : α → Bool
as : Array α
⊢ ({ toArray := as, size_toArray := ⋯ }.push a).any p = ({ toArray := as, size_toArray := ⋯ }.any p || p a)
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
/-- If `f b = 1` for all `b ∈ t`, then the product of `f a` with `a ∈ s` is the same as the
product of `f a` with `a ∈ s ∖ t`. -/
@[to_additive "If `f b = 0` for all `b ∈ t`, then the sum of `f a` with `a ∈ s` is the same as the
sum of `f a` with `a ∈ s ∖ t`."]
lemma tprod_setElem_eq_tprod_setElem_diff {f : β → α} (s t : Set β)
    (hf₀ : ∀ b ∈ t, f b = 1) :
    ∏' a : s, f a = ∏' a : (s \ t : Set β), f a :=
  .symm <| (Set.inclusion_injective (t := s) Set.diff_subset).tprod_eq (f := f ∘ (↑)) <|
    mulSupport_subset_iff'.2 fun b hb ↦ hf₀ b <| by simpa using hb

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
s t : Set β
hf₀ : ∀ b ∈ t, f b = 1
b : ↑s
hb : b ∉ Set.range (Set.inclusion ⋯)
⊢ ↑b ∈ t

Tactic:
simpa using hb

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem isCompact_univ_pi {s : ∀ i, Set (X i)} (h : ∀ i, IsCompact (s i)) :
    IsCompact (pi univ s)

Proof state:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι), IsCompact (s i)
⊢ IsCompact (univ.pi s)

Tactic:
convert isCompact_pi_infinite h

Result:
case h.e'_3
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι), IsCompact (s i)
⊢ univ.pi s = {x | ∀ (i : ι), x i ∈ s i}

Proof state:
case h.e'_3
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι), IsCompact (s i)
⊢ univ.pi s = {x | ∀ (i : ι), x i ∈ s i}

Tactic:
simp only [← mem_univ_pi, setOf_mem_eq]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem cauchy₂ (hf : IsCauSeq abv f) {ε : α} (ε0 : 0 < ε) :
    ∃ i, ∀ j ≥ i, ∀ k ≥ i, abv (f j - f k) < ε

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f j - f k) < ε / 2 + ε / 2

Tactic:
refine lt_of_le_of_lt (abv_sub_le abv _ _ _) (add_lt_add (hi _ ij) ?_)

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f i - f k) < ε / 2

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f i - f k) < ε / 2

Tactic:
rw [abv_sub abv]

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f k - f i) < ε / 2

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
⊢ ∃ i, ∀ j ≥ i, ∀ k ≥ i, abv (f j - f k) < ε

Tactic:
refine (hf _ (half_pos ε0)).imp fun i hi j ij k ik => ?_

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f j - f k) < ε

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f k - f i) < ε / 2

Tactic:
exact hi _ ik

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f j - f k) < ε

Tactic:
rw [← add_halves ε]

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : ℕ → β
hf : IsCauSeq abv f
ε : α
ε0 : 0 < ε
i : ℕ
hi : ∀ j ≥ i, abv (f j - f i) < ε / 2
j : ℕ
ij : j ≥ i
k : ℕ
ik : k ≥ i
⊢ abv (f j - f k) < ε / 2 + ε / 2
-- Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean
theorem t1Space [T1Space R] : T1Space V

Proof state:
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T1Space R
x y : V
hxy : x ≠ y
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U

Tactic:
rcases exists_separating_of_ne (R := R) hxy with ⟨f, hf⟩

Result:
case intro
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T1Space R
x y : V
hxy : x ≠ y
f : V →L[R] R
hf : f x ≠ f y
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U

Proof state:
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T1Space R
⊢ T1Space V

Tactic:
apply t1Space_iff_exists_open.2 (fun x y hxy ↦ ?_)

Result:
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T1Space R
x y : V
hxy : x ≠ y
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U

Proof state:
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T1Space R
x y : V
hxy : x ≠ y
f : V →L[R] R
hf : f x ≠ f y
⊢ y ∉ ⇑f ⁻¹' {f y}ᶜ

Tactic:
simp

Result:
no goals

Proof state:
case intro
R : Type u_1
V : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : TopologicalSpace V
inst✝³ : TopologicalSpace R
inst✝² : Module R V
inst✝¹ : SeparatingDual R V
inst✝ : T1Space R
x y : V
hxy : x ≠ y
f : V →L[R] R
hf : f x ≠ f y
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U

Tactic:
exact ⟨f ⁻¹' {f y}ᶜ, isOpen_compl_singleton.preimage f.continuous, hf, by simp⟩

Result:
no goals
-- Mathlib/GroupTheory/IndexNormal.lean
theorem normal_of_index_eq_two (hH : H.index = 2) : H.Normal where
  conj_mem x hxH g

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.index = 2
x : G
hxH : x ∈ H
g : G
⊢ g * x * g⁻¹ ∈ H

Tactic:
simp_rw [mul_mem_iff_of_index_two hH, hxH, iff_true, inv_mem_iff]

Result:
no goals
-- Mathlib/Topology/Algebra/WithZeroTopology.lean
theorem tendsto_zero : Tendsto f l (𝓝 (0 : Γ₀)) ↔ ∀ (γ₀) (_ : γ₀ ≠ 0), ∀ᶠ x in l, f x < γ₀

Proof state:
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
l : Filter α
f : α → Γ₀
⊢ Tendsto f l (𝓝 0) ↔ ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : α) in l, f x < γ₀

Tactic:
simp [nhds_zero]

Result:
no goals
-- Mathlib/Algebra/Module/Equiv/Defs.lean
@[simp]
lemma coe_addEquiv_apply (x : M) : (e : M ≃+ M₂) x = e x

Proof state:
R : Type u_1
S : Type u_5
M : Type u_6
M₂ : Type u_8
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M
inst✝ : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
x : M
⊢ ↑e x = e x

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Fintype/EquivFin.lean
theorem nonempty_of_card_le [Fintype α] [Fintype β] (h : Fintype.card α ≤ Fintype.card β) :
    Nonempty (α ↪ β)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
h : Fintype.card α ≤ Fintype.card β
⊢ Nonempty (α ↪ β)

Tactic:
classical exact (truncOfCardLE h).nonempty

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
h : Fintype.card α ≤ Fintype.card β
⊢ Nonempty (α ↪ β)

Tactic:
exact (truncOfCardLE h).nonempty

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Arrow.lean
@[simp]
lemma arrow_mk_eqToHom_comp {X' X Y : T} (f : X ⟶ Y) (h : X' = X) :
    Arrow.mk (eqToHom h ≫ f) = Arrow.mk f :=
  ext h rfl (by simp)

Proof state:
T : Type u
inst✝ : Category.{v, u} T
X' X Y : T
f : X ⟶ Y
h : X' = X
⊢ (mk (eqToHom h ≫ f)).hom = eqToHom h ≫ (mk f).hom ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem posMulMono_iff_covariant_pos :
    PosMulMono α ↔ CovariantClass α>0 α (fun x y => x * y) (· ≤ ·) :=
  ⟨@PosMulMono.to_covariantClass_pos_mul_le _ _ _ _, fun h =>
    { elim a b c h

Proof state:
case inl
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : CovariantClass α>0 α (fun x y => ↑x * y) fun x1 x2 => x1 ≤ x2
a : α≥0
b c : α
h : b ≤ c
ha : 0 = ↑a
⊢ ↑a * b ≤ ↑a * c

Tactic:
simp [← ha]

Result:
no goals

Proof state:
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : CovariantClass α>0 α (fun x y => ↑x * y) fun x1 x2 => x1 ≤ x2
a : α≥0
b c : α
h : b ≤ c
⊢ ↑a * b ≤ ↑a * c

Tactic:
obtain ha | ha := a.prop.eq_or_lt

Result:
case inl
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : CovariantClass α>0 α (fun x y => ↑x * y) fun x1 x2 => x1 ≤ x2
a : α≥0
b c : α
h : b ≤ c
ha : 0 = ↑a
⊢ ↑a * b ≤ ↑a * c

case inr
α : Type u_3
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : CovariantClass α>0 α (fun x y => ↑x * y) fun x1 x2 => x1 ≤ x2
a : α≥0
b c : α
h : b ≤ c
ha : 0 < ↑a
⊢ ↑a * b ≤ ↑a * c
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem rev_le_rev {i j : Fin n} : rev i ≤ rev j ↔ j ≤ i

Proof state:
n : Nat
i j : Fin n
⊢ i.rev ≤ j.rev ↔ j ≤ i

Tactic:
simp only [le_def, val_rev, Nat.sub_le_sub_iff_left (Nat.succ_le.2 j.is_lt)]

Result:
n : Nat
i j : Fin n
⊢ (↑j).succ ≤ ↑i + 1 ↔ ↑j ≤ ↑i

Proof state:
n : Nat
i j : Fin n
⊢ (↑j).succ ≤ ↑i + 1 ↔ ↑j ≤ ↑i

Tactic:
exact Nat.succ_le_succ_iff

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem getThenInsertIfNew?_snd_val [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} {a : α}
    {b : β a} : (m.val.getThenInsertIfNew? a b).2 = (m.getThenInsertIfNew? a b).2.1

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
b : β a
⊢ (m.val.getThenInsertIfNew? a b).snd = (m.getThenInsertIfNew? a b).snd.val

Tactic:
simp [Raw.getThenInsertIfNew?, m.2]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_append_left {as : Vector α n} {bs : Vector α m} {i : Nat} (hn : i < n) :
    (as ++ bs)[i]? = as[i]?

Proof state:
α : Type u_1
n m : Nat
as : Vector α n
bs : Vector α m
i : Nat
hn : i < n
⊢ (as ++ bs)[i]? = as[i]?

Tactic:
have hn' : i < n + m := by omega

Result:
α : Type u_1
n m : Nat
as : Vector α n
bs : Vector α m
i : Nat
hn : i < n
hn' : i < n + m
⊢ (as ++ bs)[i]? = as[i]?

Proof state:
α : Type u_1
n m : Nat
as : Vector α n
bs : Vector α m
i : Nat
hn : i < n
⊢ i < n + m

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
as : Vector α n
bs : Vector α m
i : Nat
hn : i < n
hn' : i < n + m
⊢ (as ++ bs)[i]? = as[i]?

Tactic:
simp_all [getElem?_eq_getElem, getElem_append]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Polynomial.lean
theorem polynomialFunctions_coe (X : Set R) :
    (polynomialFunctions X : Set C(X, R)) = Set.range (Polynomial.toContinuousMapOnAlgHom X)

Proof state:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
⊢ ↑(polynomialFunctions X) = Set.range ⇑(toContinuousMapOnAlgHom X)

Tactic:
ext

Result:
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
x✝ : C(↑X, R)
⊢ x✝ ∈ ↑(polynomialFunctions X) ↔ x✝ ∈ Set.range ⇑(toContinuousMapOnAlgHom X)

Proof state:
case h
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
X : Set R
x✝ : C(↑X, R)
⊢ x✝ ∈ ↑(polynomialFunctions X) ↔ x✝ ∈ Set.range ⇑(toContinuousMapOnAlgHom X)

Tactic:
simp [polynomialFunctions]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean
theorem sqrt_one_add_norm_sq_le (x : E) : √((1 : ℝ) + ‖x‖ ^ 2) ≤ 1 + ‖x‖

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ^ 2 ≤ (1 + ‖x‖) ^ 2

Tactic:
simp [add_sq]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 0 ≤ 1 + ‖x‖

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ √(1 + ‖x‖ ^ 2) ≤ 1 + ‖x‖

Tactic:
rw [sqrt_le_left (by positivity)]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ^ 2 ≤ (1 + ‖x‖) ^ 2
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma IsDiameter.ofDiameter_eq (h : s.IsDiameter p₁ p₂) : .ofDiameter p₁ p₂ = s

Proof state:
case radius
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ (Sphere.ofDiameter p₁ p₂).radius = s.radius

Tactic:
simp [Sphere.ofDiameter, ← h.dist_left_right_div_two]

Result:
no goals

Proof state:
case center
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ (Sphere.ofDiameter p₁ p₂).center = s.center

Tactic:
simp [Sphere.ofDiameter, h.midpoint_eq_center]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ Sphere.ofDiameter p₁ p₂ = s

Tactic:
ext

Result:
case center
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ (Sphere.ofDiameter p₁ p₂).center = s.center

case radius
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ (Sphere.ofDiameter p₁ p₂).radius = s.radius