harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/DFinsupp/Order.lean
theorem support_inf : (f ⊓ g).support = f.support ∩ g.support

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ a✝ ∈ (f ⊓ g).support ↔ a✝ ∈ f.support ∩ g.support

Tactic:
simp only [inf_apply, mem_support_iff, Ne, Finset.mem_inter]

Result:
case h
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ ¬f a✝ ⊓ g a✝ = 0 ↔ ¬f a✝ = 0 ∧ ¬g a✝ = 0

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ ¬f a✝ ⊓ g a✝ = 0 ↔ ¬f a✝ = 0 ∧ ¬g a✝ = 0

Tactic:
simp only [← nonpos_iff_eq_zero, min_le_iff, not_or]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ (f ⊓ g).support = f.support ∩ g.support

Tactic:
ext

Result:
case h
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
a✝ : ι
⊢ a✝ ∈ (f ⊓ g).support ↔ a✝ ∈ f.support ∩ g.support
-- Mathlib/Data/Set/Pairwise/Lattice.lean
theorem pairwiseDisjoint_unique {y : α}
    (h_disjoint : PairwiseDisjoint s f)
    (hy : y ∈ (⋃ i ∈ s, f i)) : ∃! i, i ∈ s ∧ y ∈ f i

Proof state:
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∃! i, i ∈ s ∧ y ∈ f i

Tactic:
refine existsUnique_of_exists_of_unique ?ex ?unique

Result:
case ex
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∃ x ∈ s, y ∈ f x

case unique
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∀ (y₁ y₂ : ι), y₁ ∈ s ∧ y ∈ f y₁ → y₂ ∈ s ∧ y ∈ f y₂ → y₁ = y₂

Proof state:
case unique
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∀ (y₁ y₂ : ι), y₁ ∈ s ∧ y ∈ f y₁ → y₂ ∈ s ∧ y ∈ f y₂ → y₁ = y₂

Tactic:
rintro i j ⟨his, hi⟩ ⟨hjs, hj⟩

Result:
case unique.intro.intro
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
i j : ι
his : i ∈ s
hi : y ∈ f i
hjs : j ∈ s
hj : y ∈ f j
⊢ i = j

Proof state:
case unique.intro.intro
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
i j : ι
his : i ∈ s
hi : y ∈ f i
hjs : j ∈ s
hj : y ∈ f j
⊢ i = j

Tactic:
exact h_disjoint.elim his hjs <| not_disjoint_iff.mpr ⟨y, ⟨hi, hj⟩⟩

Result:
no goals

Proof state:
case ex
α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
y : α
h_disjoint : s.PairwiseDisjoint f
hy : y ∈ ⋃ i ∈ s, f i
⊢ ∃ x ∈ s, y ∈ f x

Tactic:
simpa only [mem_iUnion, exists_prop] using hy

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem coe_finsetBasisOfLinearIndependentOfCardEqFinrank {s : Finset V} (hs : s.Nonempty)
    (lin_ind : LinearIndependent K ((↑) : s → V)) (card_eq : s.card = finrank K V) :
    ⇑(finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq) = ((↑) : s → V)

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : s.Nonempty
lin_ind : LinearIndependent K Subtype.val
card_eq : s.card = finrank K V
⊢ ⇑(basisOfLinearIndependentOfCardEqFinrank lin_ind ⋯) = Subtype.val

Tactic:
exact Basis.coe_mk _ _

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : s.Nonempty
lin_ind : LinearIndependent K Subtype.val
card_eq : s.card = finrank K V
⊢ ⇑(finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq) = Subtype.val

Tactic:
rw [finsetBasisOfLinearIndependentOfCardEqFinrank]

Result:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : s.Nonempty
lin_ind : LinearIndependent K Subtype.val
card_eq : s.card = finrank K V
⊢ ⇑(basisOfLinearIndependentOfCardEqFinrank lin_ind ⋯) = Subtype.val
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem right_inv_eq_right_inv (h : A * B = 1) (g : A * C = 1) : B = C

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : A * C = 1
⊢ B = C

Tactic:
rw [← inv_eq_right_inv h, ← inv_eq_right_inv g]

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
theorem count_coe_fill_of_ne [DecidableEq α] {a x : α} {i : Fin (n + 1)} {s : Sym α (n - i)}
    (hx : x ≠ a) :
    count x (fill a i s : Multiset α) = count x s

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a x : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : x ≠ a
⊢ x ∉ Multiset.replicate (↑i) a

Tactic:
simp [Multiset.mem_replicate, hx]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a x : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : x ≠ a
this : x ∉ Multiset.replicate (↑i) a
⊢ count x ↑(fill a i s) = count x ↑s

Tactic:
simp [coe_fill, coe_replicate, this]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a x : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : x ≠ a
⊢ count x ↑(fill a i s) = count x ↑s

Tactic:
suffices x ∉ Multiset.replicate i a by simp [coe_fill, coe_replicate, this]

Result:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a x : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : x ≠ a
⊢ x ∉ Multiset.replicate (↑i) a
-- Mathlib/NumberTheory/JacobiSum/Basic.lean
lemma jacobiSum_comm (χ ψ : MulChar R R') : jacobiSum χ ψ = jacobiSum ψ χ

Proof state:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype R
inst✝ : CommRing R'
χ ψ : MulChar R R'
⊢ ∑ x : R, ψ (1 - x) * χ x = ∑ x : R, ψ x * χ (1 - x)

Tactic:
rw [← (Equiv.subLeft 1).sum_comp]

Result:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype R
inst✝ : CommRing R'
χ ψ : MulChar R R'
⊢ ∑ i : R, ψ (1 - (Equiv.subLeft 1) i) * χ ((Equiv.subLeft 1) i) = ∑ x : R, ψ x * χ (1 - x)

Proof state:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype R
inst✝ : CommRing R'
χ ψ : MulChar R R'
⊢ ∑ i : R, ψ (1 - (Equiv.subLeft 1) i) * χ ((Equiv.subLeft 1) i) = ∑ x : R, ψ x * χ (1 - x)

Tactic:
simp only [Equiv.subLeft_apply, sub_sub_cancel]

Result:
no goals

Proof state:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype R
inst✝ : CommRing R'
χ ψ : MulChar R R'
⊢ jacobiSum χ ψ = jacobiSum ψ χ

Tactic:
simp only [jacobiSum, mul_comm (χ _)]

Result:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype R
inst✝ : CommRing R'
χ ψ : MulChar R R'
⊢ ∑ x : R, ψ (1 - x) * χ x = ∑ x : R, ψ x * χ (1 - x)
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem injective_boxes : Function.Injective (boxes : Prepartition I → Finset (Box ι))

Proof state:
ι : Type u_1
I : Box ι
⊢ Injective boxes

Tactic:
rintro ⟨s₁, h₁, h₁'⟩ ⟨s₂, h₂, h₂'⟩ (rfl : s₁ = s₂)

Result:
case mk.mk
ι : Type u_1
I : Box ι
s₁ : Finset (Box ι)
h₁ : ∀ J ∈ s₁, J ≤ I
h₁' : (↑s₁).Pairwise (Disjoint on Box.toSet)
h₂ : ∀ J ∈ s₁, J ≤ I
h₂' : (↑s₁).Pairwise (Disjoint on Box.toSet)
⊢ { boxes := s₁, le_of_mem' := h₁, pairwiseDisjoint := h₁' } =
    { boxes := s₁, le_of_mem' := h₂, pairwiseDisjoint := h₂' }

Proof state:
case mk.mk
ι : Type u_1
I : Box ι
s₁ : Finset (Box ι)
h₁ : ∀ J ∈ s₁, J ≤ I
h₁' : (↑s₁).Pairwise (Disjoint on Box.toSet)
h₂ : ∀ J ∈ s₁, J ≤ I
h₂' : (↑s₁).Pairwise (Disjoint on Box.toSet)
⊢ { boxes := s₁, le_of_mem' := h₁, pairwiseDisjoint := h₁' } =
    { boxes := s₁, le_of_mem' := h₂, pairwiseDisjoint := h₂' }

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
lemma BddBelow.range_comp {γ : Type*} [Preorder β] [Preorder γ] {f : α → β} {g : β → γ}
    (hf : BddBelow (range f)) (hg : Monotone g) : BddBelow (range (fun x => g (f x)))

Proof state:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddBelow (range f)
hg : Monotone g
⊢ BddBelow (range fun x => g (f x))

Tactic:
change BddBelow (range (g ∘ f))

Result:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddBelow (range f)
hg : Monotone g
⊢ BddBelow (range (g ∘ f))

Proof state:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddBelow (range f)
hg : Monotone g
⊢ BddBelow (range (g ∘ f))

Tactic:
simpa only [Set.range_comp] using hg.map_bddBelow hf

Result:
no goals
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem exists_nonzero_mem_of_ne_bot {P : Ideal R[X]} (Pb : P ≠ ⊥) (hP : ∀ x : R, C x ∈ P → x = 0) :
    ∃ p : R[X], p ∈ P ∧ Polynomial.map (Quotient.mk (P.comap (C : R →+* R[X]))) p ≠ 0

Proof state:
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
⊢ ∃ p ∈ P, Polynomial.map (Quotient.mk (comap C P)) p ≠ 0

Tactic:
obtain ⟨m, hm⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr Pb)

Result:
case intro
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
m : ↥P
hm : m ≠ 0
⊢ ∃ p ∈ P, Polynomial.map (Quotient.mk (comap C P)) p ≠ 0

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
m : ↥P
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ comap C P = ⊥

Tactic:
exact (Submodule.eq_bot_iff _).mpr fun x hx => hP x (mem_comap.mp hx)

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
m : ↥P
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ RingHom.ker (Quotient.mk (comap C P)) = ⊥

Tactic:
rw [mk_ker]

Result:
case intro
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
m : ↥P
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ comap C P = ⊥

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
m : ↥P
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ Function.Injective ⇑(mapRingHom (Quotient.mk (comap C P)))

Tactic:
refine map_injective _ ((Ideal.Quotient.mk (P.comap C)).injective_iff_ker_eq_bot.mpr ?_)

Result:
case intro
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
m : ↥P
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ RingHom.ker (Quotient.mk (comap C P)) = ⊥

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
m : ↥P
hm : m ≠ 0
⊢ ∃ p ∈ P, Polynomial.map (Quotient.mk (comap C P)) p ≠ 0

Tactic:
refine ⟨m, Submodule.coe_mem m, fun pp0 => hm (Submodule.coe_eq_zero.mp ?_)⟩

Result:
case intro
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
m : ↥P
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ ↑m = 0

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
m : ↥P
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ ↑m = 0

Tactic:
refine
  (injective_iff_map_eq_zero (Polynomial.mapRingHom (Ideal.Quotient.mk
    (P.comap (C : R →+* R[X]))))).mp
    ?_ _ pp0

Result:
case intro
R : Type u_1
inst✝ : CommRing R
P : Ideal R[X]
Pb : P ≠ ⊥
hP : ∀ (x : R), C x ∈ P → x = 0
m : ↥P
hm : m ≠ 0
pp0 : Polynomial.map (Quotient.mk (comap C P)) ↑m = 0
⊢ Function.Injective ⇑(mapRingHom (Quotient.mk (comap C P)))
-- Mathlib/Algebra/Group/PNatPowAssoc.lean
theorem ppow_mul' (x : M) (m n : ℕ+) : x ^ (m * n) = (x ^ n) ^ m

Proof state:
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m n : ℕ+
⊢ x ^ (n * m) = (x ^ n) ^ m

Tactic:
exact ppow_mul x n m

Result:
no goals

Proof state:
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m n : ℕ+
⊢ x ^ (m * n) = (x ^ n) ^ m

Tactic:
rw [mul_comm]

Result:
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m n : ℕ+
⊢ x ^ (n * m) = (x ^ n) ^ m
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
lemma lowerSemicontinuous_add : LowerSemicontinuous fun p : EReal × EReal ↦ p.1 + p.2

Proof state:
case neg
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
hx₂ : ¬x.2 = ⊥
⊢ y < (fun p => p.1 + p.2) x → ∀ᶠ (x' : EReal × EReal) in 𝓝 x, y < (fun p => p.1 + p.2) x'

Tactic:
exact continuousAt_add (.inr hx₂) (.inl hx₁) |>.lowerSemicontinuousAt _

Result:
no goals

Proof state:
case pos
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
hx₂ : x.2 = ⊥
⊢ y < (fun p => p.1 + p.2) x → ∀ᶠ (x' : EReal × EReal) in 𝓝 x, y < (fun p => p.1 + p.2) x'

Tactic:
simp [hx₂]

Result:
no goals

Proof state:
case pos
x : EReal × EReal
y : EReal
hx₁ : x.1 = ⊥
⊢ y < (fun p => p.1 + p.2) x → ∀ᶠ (x' : EReal × EReal) in 𝓝 x, y < (fun p => p.1 + p.2) x'

Tactic:
simp [hx₁]

Result:
no goals

Proof state:
⊢ LowerSemicontinuous fun p => p.1 + p.2

Tactic:
intro x y

Result:
x : EReal × EReal
y : EReal
⊢ y < (fun p => p.1 + p.2) x → ∀ᶠ (x' : EReal × EReal) in 𝓝 x, y < (fun p => p.1 + p.2) x'

Proof state:
case neg
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
⊢ y < (fun p => p.1 + p.2) x → ∀ᶠ (x' : EReal × EReal) in 𝓝 x, y < (fun p => p.1 + p.2) x'

Tactic:
by_cases hx₂ : x.2 = ⊥

Result:
case pos
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
hx₂ : x.2 = ⊥
⊢ y < (fun p => p.1 + p.2) x → ∀ᶠ (x' : EReal × EReal) in 𝓝 x, y < (fun p => p.1 + p.2) x'

case neg
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
hx₂ : ¬x.2 = ⊥
⊢ y < (fun p => p.1 + p.2) x → ∀ᶠ (x' : EReal × EReal) in 𝓝 x, y < (fun p => p.1 + p.2) x'

Proof state:
x : EReal × EReal
y : EReal
⊢ y < (fun p => p.1 + p.2) x → ∀ᶠ (x' : EReal × EReal) in 𝓝 x, y < (fun p => p.1 + p.2) x'

Tactic:
by_cases hx₁ : x.1 = ⊥

Result:
case pos
x : EReal × EReal
y : EReal
hx₁ : x.1 = ⊥
⊢ y < (fun p => p.1 + p.2) x → ∀ᶠ (x' : EReal × EReal) in 𝓝 x, y < (fun p => p.1 + p.2) x'

case neg
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
⊢ y < (fun p => p.1 + p.2) x → ∀ᶠ (x' : EReal × EReal) in 𝓝 x, y < (fun p => p.1 + p.2) x'
-- Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean
theorem hasDerivAt_exp (x : ℂ) : HasDerivAt exp (exp x) x

Proof state:
case h
x : ℂ
this : 1 < 2
⊢ ∀ a ∈ Metric.ball 0 1, ‖cexp (x + a) - cexp x - a • cexp x‖ ≤ ‖cexp x‖ * ‖a ^ 2‖

Tactic:
simp only [Metric.mem_ball, dist_zero_right, norm_pow]

Result:
case h
x : ℂ
this : 1 < 2
⊢ ∀ (a : ℂ), ‖a‖ < 1 → ‖cexp (x + a) - cexp x - a • cexp x‖ ≤ ‖cexp x‖ * ‖a‖ ^ 2

Proof state:
x : ℂ
⊢ 1 < 2

Tactic:
norm_num

Result:
no goals

Proof state:
x : ℂ
⊢ (fun h => cexp (x + h) - cexp x - h • cexp x) =o[𝓝 0] fun h => h

Tactic:
have : (1 : ℕ) < 2 := by norm_num

Result:
x : ℂ
this : 1 < 2
⊢ (fun h => cexp (x + h) - cexp x - h • cexp x) =o[𝓝 0] fun h => h

Proof state:
x : ℂ
this : 1 < 2
⊢ (fun h => cexp (x + h) - cexp x - h • cexp x) =o[𝓝 0] fun h => h

Tactic:
refine (IsBigO.of_bound ‖exp x‖ ?_).trans_isLittleO (isLittleO_pow_id this)

Result:
x : ℂ
this : 1 < 2
⊢ ∀ᶠ (x_1 : ℂ) in 𝓝 0, ‖cexp (x + x_1) - cexp x - x_1 • cexp x‖ ≤ ‖cexp x‖ * ‖x_1 ^ 2‖

Proof state:
case h
x : ℂ
this : 1 < 2
⊢ ∀ (a : ℂ), ‖a‖ < 1 → ‖cexp (x + a) - cexp x - a • cexp x‖ ≤ ‖cexp x‖ * ‖a‖ ^ 2

Tactic:
exact fun z hz => exp_bound_sq x z hz.le

Result:
no goals

Proof state:
x : ℂ
⊢ HasDerivAt cexp (cexp x) x

Tactic:
rw [hasDerivAt_iff_isLittleO_nhds_zero]

Result:
x : ℂ
⊢ (fun h => cexp (x + h) - cexp x - h • cexp x) =o[𝓝 0] fun h => h

Proof state:
x : ℂ
this : 1 < 2
⊢ ∀ᶠ (x_1 : ℂ) in 𝓝 0, ‖cexp (x + x_1) - cexp x - x_1 • cexp x‖ ≤ ‖cexp x‖ * ‖x_1 ^ 2‖

Tactic:
filter_upwards [Metric.ball_mem_nhds (0 : ℂ) zero_lt_one]

Result:
case h
x : ℂ
this : 1 < 2
⊢ ∀ a ∈ Metric.ball 0 1, ‖cexp (x + a) - cexp x - a • cexp x‖ ≤ ‖cexp x‖ * ‖a ^ 2‖
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_prod_of_nonempty {s : Set α} {t : Set β} (h : (s ×ˢ t).Nonempty) :
    MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
h : (s ×ˢ t).Nonempty
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t

Tactic:
rcases h with ⟨⟨x, y⟩, hx, hy⟩

Result:
case intro.mk.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t

Proof state:
case intro.mk.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
hst : MeasurableSet (s ×ˢ t)
this : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t

Tactic:
have : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t) := measurable_prod_mk_left hst

Result:
case intro.mk.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
hst : MeasurableSet (s ×ˢ t)
this✝ : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t)
this : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t

Proof state:
case intro.mk.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
hst : MeasurableSet (s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t

Tactic:
have : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t) := measurable_prod_mk_right hst

Result:
case intro.mk.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
hst : MeasurableSet (s ×ˢ t)
this : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t

Proof state:
case intro.mk.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t

Tactic:
refine ⟨fun hst => ?_, fun h => h.1.prod h.2⟩

Result:
case intro.mk.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
hst : MeasurableSet (s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t

Proof state:
case intro.mk.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
hst : MeasurableSet (s ×ˢ t)
this✝ : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t)
this : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t

Tactic:
simp_all

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Order.lean
@[to_additive]
lemma MulEquiv.strictMono_symm {G G' : Type*} [LinearOrderedCommMonoid G]
    [LinearOrderedCommMonoid G'] {e : G ≃* G'} (he : StrictMono e) : StrictMono e.symm

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : LinearOrderedCommMonoid G
inst✝ : LinearOrderedCommMonoid G'
e : G ≃* G'
he : StrictMono ⇑e
a✝ : G'
⊢ ∀ ⦃b : G'⦄, a✝ < b → e.symm a✝ < e.symm b

Tactic:
simp [← he.lt_iff_lt]

Result:
no goals

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : LinearOrderedCommMonoid G
inst✝ : LinearOrderedCommMonoid G'
e : G ≃* G'
he : StrictMono ⇑e
⊢ StrictMono ⇑e.symm

Tactic:
intro

Result:
G : Type u_1
G' : Type u_2
inst✝¹ : LinearOrderedCommMonoid G
inst✝ : LinearOrderedCommMonoid G'
e : G ≃* G'
he : StrictMono ⇑e
a✝ : G'
⊢ ∀ ⦃b : G'⦄, a✝ < b → e.symm a✝ < e.symm b
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem mul_pow_charP_coeff_zero [CharP R p] (x : 𝕎 R) {m n : ℕ} (h : m < n) :
    (x * p ^ n).coeff m = 0

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → (x * ↑p ^ n).coeff m = 0
m : ℕ
h : m < n + 1
⊢ (x * ↑p ^ (n + 1)).coeff m = 0

Tactic:
rw [pow_succ, ← mul_assoc]

Result:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → (x * ↑p ^ n).coeff m = 0
m : ℕ
h : m < n + 1
⊢ (x * ↑p ^ n * ↑p).coeff m = 0

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → (x * ↑p ^ n).coeff m = 0
m : ℕ
h : m < n + 1
⊢ (x * ↑p ^ n * ↑p).coeff m = 0

Tactic:
cases m with
| zero => exact mul_charP_coeff_zero _
| succ m' =>
  rw [mul_charP_coeff_succ, ih, zero_pow hp.out.ne_zero]
  simpa using h

Result:
no goals

Proof state:
case succ.zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → (x * ↑p ^ n).coeff m = 0
h : 0 < n + 1
⊢ (x * ↑p ^ n * ↑p).coeff 0 = 0

Tactic:
exact mul_charP_coeff_zero _

Result:
no goals

Proof state:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
m : ℕ
h : m < 0
⊢ (x * ↑p ^ 0).coeff m = 0

Tactic:
contradiction

Result:
no goals

Proof state:
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → (x * ↑p ^ n).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ m' < n

Tactic:
simpa using h

Result:
no goals

Proof state:
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → (x * ↑p ^ n).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ (x * ↑p ^ n * ↑p).coeff (m' + 1) = 0

Tactic:
rw [mul_charP_coeff_succ, ih, zero_pow hp.out.ne_zero]

Result:
case succ.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → (x * ↑p ^ n).coeff m = 0
m' : ℕ
h : m' + 1 < n + 1
⊢ m' < n

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
m n : ℕ
h : m < n
⊢ (x * ↑p ^ n).coeff m = 0

Tactic:
induction' n with n ih generalizing m

Result:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
m : ℕ
h : m < 0
⊢ (x * ↑p ^ 0).coeff m = 0

case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, m < n → (x * ↑p ^ n).coeff m = 0
m : ℕ
h : m < n + 1
⊢ (x * ↑p ^ (n + 1)).coeff m = 0
-- Mathlib/MeasureTheory/Measure/Portmanteau.lean
theorem le_measure_compl_liminf_of_limsup_measure_le {ι : Type*} {L : Filter ι} {μ : Measure Ω}
    {μs : ι → Measure Ω} [IsProbabilityMeasure μ] [∀ i, IsProbabilityMeasure (μs i)] {E : Set Ω}
    (E_mble : MeasurableSet E) (h : (L.limsup fun i ↦ μs i E) ≤ μ E) :
    μ Eᶜ ≤ L.liminf fun i ↦ μs i Eᶜ

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
ι : Type u_2
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
E : Set Ω
E_mble : MeasurableSet E
h : limsup (fun i => (μs i) E) L ≤ μ E
hne : L.NeBot
meas_Ec : μ Eᶜ = 1 - μ E
i : ι
⊢ (μs i) Eᶜ = 1 - (μs i) E

Tactic:
simpa only [measure_univ] using measure_compl E_mble (measure_lt_top (μs i) E).ne

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem isHermitian_conjTranspose_mul_mul [Fintype m] {A : Matrix m m α} (B : Matrix m n α)
    (hA : A.IsHermitian) : (Bᴴ * A * B).IsHermitian

Proof state:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝² : NonUnitalSemiring α
inst✝¹ : StarRing α
inst✝ : Fintype m
A : Matrix m m α
B : Matrix m n α
hA : A.IsHermitian
⊢ (Bᴴ * A * B).IsHermitian

Tactic:
simp only [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose, hA.eq, Matrix.mul_assoc]

Result:
no goals