harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Bases.lean
theorem mem_iff_inf_principal_compl {f : Filter α} {s : Set α} : s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥

Proof state:
α : Type u_1
f : Filter α
s : Set α
h : ∀ U ∈ f, (U ∩ sᶜ).Nonempty
hs : s ∈ f
⊢ False

Tactic:
simpa [Set.not_nonempty_empty] using h s hs

Result:
no goals

Proof state:
α : Type u_1
f : Filter α
s : Set α
⊢ (∀ U ∈ f, (U ∩ sᶜ).Nonempty) ↔ s ∉ f

Tactic:
exact
  ⟨fun h hs => by simpa [Set.not_nonempty_empty] using h s hs, fun hs t ht =>
    inter_compl_nonempty_iff.2 fun hts => hs <| mem_of_superset ht hts⟩

Result:
no goals

Proof state:
α : Type u_1
f : Filter α
s : Set α
⊢ s ∈ f ↔ f ⊓ 𝓟 sᶜ = ⊥

Tactic:
refine not_iff_not.1 ((inf_principal_neBot_iff.trans ?_).symm.trans neBot_iff)

Result:
α : Type u_1
f : Filter α
s : Set α
⊢ (∀ U ∈ f, (U ∩ sᶜ).Nonempty) ↔ s ∉ f
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_of_stronglyMeasurable (hm : m ≤ m₀) [hμm : SigmaFinite (μ.trim hm)] {f : α → E}
    (hf : StronglyMeasurable[m] f) (hfi : Integrable f μ) : μ[f|m] = f

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ μ[f|m] = f

Tactic:
rw [condExp_of_sigmaFinite hm, if_pos hfi, if_pos hf]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_list_count_of_subset [DecidableEq α] [CommMonoid α] (m : List α) (s : Finset α)
    (hs : m.toFinset ⊆ s) : m.prod = ∏ i ∈ s, i ^ m.count i

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : List α
s : Finset α
hs : m.toFinset ⊆ s
x : α
x✝ : x ∈ s
hx : x ∉ m.toFinset
⊢ x ^ count x m = 1

Tactic:
rw [mem_toFinset] at hx

Result:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : List α
s : Finset α
hs : m.toFinset ⊆ s
x : α
x✝ : x ∈ s
hx : x ∉ m
⊢ x ^ count x m = 1

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : List α
s : Finset α
hs : m.toFinset ⊆ s
⊢ m.prod = ∏ i ∈ s, i ^ count i m

Tactic:
rw [prod_list_count]

Result:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : List α
s : Finset α
hs : m.toFinset ⊆ s
⊢ ∏ m_1 ∈ m.toFinset, m_1 ^ count m_1 m = ∏ i ∈ s, i ^ count i m

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : List α
s : Finset α
hs : m.toFinset ⊆ s
⊢ ∏ m_1 ∈ m.toFinset, m_1 ^ count m_1 m = ∏ i ∈ s, i ^ count i m

Tactic:
refine prod_subset hs fun x _ hx => ?_

Result:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : List α
s : Finset α
hs : m.toFinset ⊆ s
x : α
x✝ : x ∈ s
hx : x ∉ m.toFinset
⊢ x ^ count x m = 1

Proof state:
α : Type u_3
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
m : List α
s : Finset α
hs : m.toFinset ⊆ s
x : α
x✝ : x ∈ s
hx : x ∉ m
⊢ x ^ count x m = 1

Tactic:
rw [count_eq_zero_of_not_mem hx, pow_zero]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
lemma map_iInf {ι : Type*} [Nonempty ι] {p : ι → Submodule R M} (f : F) (hf : Injective f) :
    (⨅ i, p i).map f = ⨅ i, (p i).map f :=
  SetLike.coe_injective <| by simpa only [map_coe, iInf_coe] using hf.injOn.image_iInter_eq

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝³ : RingHomSurjective σ₁₂
F : Type u_9
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F σ₁₂ M M₂
ι : Type u_10
inst✝ : Nonempty ι
p : ι → Submodule R M
f : F
hf : Injective ⇑f
⊢ ↑(map f (⨅ i, p i)) = ↑(⨅ i, map f (p i))

Tactic:
simpa only [map_coe, iInf_coe] using hf.injOn.image_iInter_eq

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem t0Space_iff_not_inseparable (X : Type u) [TopologicalSpace X] :
    T0Space X ↔ Pairwise fun x y : X => ¬Inseparable x y

Proof state:
X : Type u
inst✝ : TopologicalSpace X
⊢ T0Space X ↔ Pairwise fun x y => ¬Inseparable x y

Tactic:
simp only [t0Space_iff_inseparable, Ne, not_imp_not, Pairwise]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_add_sinh : cosh x + sinh x = exp x

Proof state:
x : ℂ
⊢ cosh x + sinh x = cexp x

Tactic:
rw [← mul_right_inj' (two_ne_zero' ℂ), mul_add, two_cosh, two_sinh, add_add_sub_cancel, two_mul]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivAt.div_const (hc : HasDerivAt c c' x) (d : 𝕜') :
    HasDerivAt (fun x => c x / d) (c' / d) x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivAt c c' x
d : 𝕜'
⊢ HasDerivAt (fun x => c x / d) (c' / d) x

Tactic:
simpa only [div_eq_mul_inv] using hc.mul_const d⁻¹

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Path.lean
lemma cons_ne_nil (p : Path a b) (e : b ⟶ a) : p.cons e ≠ Path.nil :=
  fun h => by injection h

Proof state:
V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
e : b ⟶ a
h : p.cons e = nil
⊢ False

Tactic:
injection h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
theorem lift_base : lift f fs w ≫ base arrows = f

Proof state:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
⊢ lift f fs w ≫ base arrows = f

Tactic:
simp only [limit.lift_π, WidePullbackShape.mkCone_pt, WidePullbackShape.mkCone_π_app]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_equiv_of_lift_eq (leq : lift.{v} #α = lift.{u} #β') : #(α ≃ β') = 2 ^ lift.{v} #α

Proof state:
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
⊢ #(α ≃ β') = 2 ^ lift.{v, u} #α

Tactic:
erw [← (lift_mk_eq'.2 ⟨.equivCongr (.refl α) (lift_mk_eq'.1 leq).some⟩).trans (lift_id'.{u,v} _),
  lift_umax.{u,v}, mk_perm_eq_two_power, lift_power, lift_natCast]

Result:
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
⊢ ↑2 ^ lift.{v, u} #α = 2 ^ lift.{v, u} #α

Proof state:
α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
⊢ ↑2 ^ lift.{v, u} #α = 2 ^ lift.{v, u} #α

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β)
    (l : Array α) (init : β) (w : start = (l.filter p).size) :
    (l.filter p).foldrM g init start 0 =
      l.foldrM (fun x y => if p x then g x y else pure y) init

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : α → β → m β
init : β
toList✝ : List α
⊢ foldrM g init (filter p { toList := toList✝ }) =
    foldrM (fun x y => if p x = true then g x y else pure y) init { toList := toList✝ }

Tactic:
simp [List.foldrM_filter]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : α → β → m β
l : Array α
init : β
⊢ foldrM g init (filter p l) = foldrM (fun x y => if p x = true then g x y else pure y) init l

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : α → β → m β
init : β
toList✝ : List α
⊢ foldrM g init (filter p { toList := toList✝ }) =
    foldrM (fun x y => if p x = true then g x y else pure y) init { toList := toList✝ }

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
start : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : α → β → m β
l : Array α
init : β
w : start = (filter p l).size
⊢ foldrM g init (filter p l) start = foldrM (fun x y => if p x = true then g x y else pure y) init l

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : α → β → m β
l : Array α
init : β
⊢ foldrM g init (filter p l) = foldrM (fun x y => if p x = true then g x y else pure y) init l
-- Mathlib/GroupTheory/Solvable.lean
theorem derivedSeries_le_map_derivedSeries (hf : Function.Surjective f) (n : ℕ) :
    derivedSeries G' n ≤ (derivedSeries G n).map f

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
n : ℕ
⊢ derivedSeries G' n ≤ map f (derivedSeries G n)

Tactic:
induction n with
| zero => exact (map_top_of_surjective f hf).ge
| succ n ih => exact commutator_le_map_commutator ih ih

Result:
no goals

Proof state:
case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
n : ℕ
ih : derivedSeries G' n ≤ map f (derivedSeries G n)
⊢ derivedSeries G' (n + 1) ≤ map f (derivedSeries G (n + 1))

Tactic:
exact commutator_le_map_commutator ih ih

Result:
no goals

Proof state:
case zero
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
⊢ derivedSeries G' 0 ≤ map f (derivedSeries G 0)

Tactic:
exact (map_top_of_surjective f hf).ge

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean
theorem mono_fst_of_is_pullback_of_mono {t : PullbackCone f g} (ht : IsLimit t) [Mono g] :
    Mono t.fst

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono g
W : C
h k : W ⟶ t.pt
i : h ≫ t.fst = k ≫ t.fst
⊢ h ≫ t.snd = k ≫ t.snd

Tactic:
rw [← cancel_mono g, Category.assoc, Category.assoc, ← condition]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono g
W : C
h k : W ⟶ t.pt
i : h ≫ t.fst = k ≫ t.fst
⊢ h ≫ t.fst ≫ f = k ≫ t.fst ≫ f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono g
⊢ Mono t.fst

Tactic:
refine ⟨fun {W} h k i => IsLimit.hom_ext ht i ?_⟩

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono g
W : C
h k : W ⟶ t.pt
i : h ≫ t.fst = k ≫ t.fst
⊢ h ≫ t.snd = k ≫ t.snd

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono g
W : C
h k : W ⟶ t.pt
i : h ≫ t.fst = k ≫ t.fst
⊢ h ≫ t.fst ≫ f = k ≫ t.fst ≫ f

Tactic:
apply reassoc_of% i

Result:
no goals
-- Mathlib/Order/Compare.lean
theorem Compares.ne_lt [Preorder α] : ∀ {o} {a b : α}, Compares o a b → (o ≠ lt ↔ b ≤ a)
  | lt, _, _, h => ⟨absurd rfl, fun h' => (not_le_of_lt h h').elim⟩
  | eq, _, _, h => ⟨fun _ => ge_of_eq h, fun _ h => by injection h⟩
  | gt, _, _, h => ⟨fun _ => le_of_lt h, fun _ h => by injection h⟩

Proof state:
α : Type u_1
inst✝ : Preorder α
x✝² x✝¹ : α
h✝ : eq.Compares x✝² x✝¹
x✝ : x✝¹ ≤ x✝²
h : eq = lt
⊢ False

Tactic:
injection h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x✝² x✝¹ : α
h✝ : gt.Compares x✝² x✝¹
x✝ : x✝¹ ≤ x✝²
h : gt = lt
⊢ False

Tactic:
injection h

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem preAleph_limit {o : Ordinal} (ho : o.IsLimit) : preAleph o = ⨆ a : Iio o, preAleph a

Proof state:
o : Ordinal.{u_1}
ho : o.IsLimit
⊢ preAleph o ≤ ⨆ a, preAleph ↑a

Tactic:
rw [preAleph_le_of_isLimit ho]

Result:
o : Ordinal.{u_1}
ho : o.IsLimit
⊢ ∀ o' < o, preAleph o' ≤ ⨆ a, preAleph ↑a

Proof state:
o : Ordinal.{u_1}
ho : o.IsLimit
⊢ ∀ o' < o, preAleph o' ≤ ⨆ a, preAleph ↑a

Tactic:
exact fun a ha => le_ciSup (bddAbove_of_small _) (⟨a, ha⟩ : Iio o)

Result:
no goals

Proof state:
o : Ordinal.{u_1}
ho : o.IsLimit
⊢ preAleph o = ⨆ a, preAleph ↑a

Tactic:
refine le_antisymm ?_ (ciSup_le' fun i => preAleph_le_preAleph.2 i.2.le)

Result:
o : Ordinal.{u_1}
ho : o.IsLimit
⊢ preAleph o ≤ ⨆ a, preAleph ↑a
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_matrix (m : Type v) (n : Type w) [Finite m] [Finite n] :
    Module.rank R (Matrix m n R) =
      Cardinal.lift.{max v w u, v} #m * Cardinal.lift.{max v w u, w} #n

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m : Type v
n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Module.rank R (Matrix m n R) = lift.{max v w u, v} #m * lift.{max v w u, w} #n

Tactic:
rw [rank_matrix_module, rank_self, lift_one, mul_one, ← lift_lift.{v, max u w}, lift_id,
  ← lift_lift.{w, max u v}, lift_id]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem index_map_dvd {f : G →* G'} (hf : Function.Surjective f) :
    (H.map f).index ∣ H.index

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Function.Surjective ⇑f
⊢ (map f H).index ∣ H.index

Tactic:
rw [index_map, f.range_eq_top_of_surjective hf, index_top, mul_one]

Result:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Function.Surjective ⇑f
⊢ (H ⊔ f.ker).index ∣ H.index

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
hf : Function.Surjective ⇑f
⊢ (H ⊔ f.ker).index ∣ H.index

Tactic:
exact index_dvd_of_le le_sup_left

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_empty [Inhabited α] {a : α} {c} :
    (empty c : Raw α β).getKey! a = default

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : Inhabited α
a : α
c : Nat
⊢ (empty c).getKey! a = default

Tactic:
simp_to_raw using Raw₀.getKey!_empty

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
lemma tendsto_coe_toNNReal {a : ℝ≥0∞} (ha : a ≠ ⊤) : Tendsto (↑) (𝓝 a.toNNReal) (𝓝 a)

Proof state:
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 ↑a.toNNReal)

Tactic:
exact continuous_coe.tendsto _

Result:
no goals

Proof state:
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 a)

Tactic:
nth_rewrite 2 [← coe_toNNReal ha]

Result:
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 ↑a.toNNReal)
-- Mathlib/Data/ZMod/Basic.lean
theorem intCast_eq_intCast_iff_dvd_sub (a b : ℤ) (c : ℕ) : (a : ZMod c) = ↑b ↔ ↑c ∣ b - a

Proof state:
a b : ℤ
c : ℕ
⊢ ↑a = ↑b ↔ ↑c ∣ b - a

Tactic:
rw [ZMod.intCast_eq_intCast_iff, Int.modEq_iff_dvd]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma map_op_inv (s : Finset α) : s⁻¹.map opEquiv.toEmbedding = (s.map opEquiv.toEmbedding)⁻¹

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Inv α
s : Finset α
⊢ map opEquiv.toEmbedding s⁻¹ = (map opEquiv.toEmbedding s)⁻¹

Tactic:
simp [map_eq_image, image_op_inv]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_polynomialY : (W'.baseChange B).toJacobian.polynomialY =
    MvPolynomial.map f (W'.baseChange A).toJacobian.polynomialY

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (baseChange W' B).toJacobian.polynomialY = (MvPolynomial.map ↑f) (baseChange W' A).toJacobian.polynomialY

Tactic:
rw [← map_polynomialY, map_baseChange]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
@[simp]
lemma LSeries_sub {f g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s) (hg : LSeriesSummable g s) :
    LSeries (f - g) s = LSeries f s - LSeries g s

Proof state:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeries (f - g) s = LSeries f s - LSeries g s

Tactic:
simpa [LSeries, term_sub] using tsum_sub hf hg

Result:
no goals
-- Mathlib/Algebra/Order/Ring/WithTop.lean
lemma mul_coe_eq_bind {b : α} (hb : b ≠ 0) : ∀ a, (a * b : WithBot α) = a.bind fun a ↦ ↑(a * b)
  | ⊥ => by simp only [ne_eq, coe_eq_zero, hb, not_false_eq_true, bot_mul]; rfl
  | (a : α) => rfl

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊥ = Option.bind ⊥ fun a => Option.some (a * b)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊥ * ↑b = Option.bind ⊥ fun a => Option.some (a * b)

Tactic:
simp only [ne_eq, coe_eq_zero, hb, not_false_eq_true, bot_mul]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : α
hb : b ≠ 0
⊢ ⊥ = Option.bind ⊥ fun a => Option.some (a * b)
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem HasDerivWithinAt.norm_sq {f : ℝ → F} {f' : F} {s : Set ℝ} {x : ℝ}
    (hf : HasDerivWithinAt f f' s x) :
    HasDerivWithinAt (‖f ·‖ ^ 2) (2 * Inner.inner (f x) f') s x

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
f : ℝ → F
f' : F
s : Set ℝ
x : ℝ
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun x => ‖f x‖ ^ 2) (2 * Inner.inner (f x) f') s x

Tactic:
simpa using hf.hasFDerivWithinAt.norm_sq.hasDerivWithinAt

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem mul_ne_one : a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Proof state:
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1

Tactic:
rw [not_iff_comm]

Result:
α : Type u
inst✝¹ : LeftCancelMonoid α
inst✝ : Subsingleton αˣ
a b : α
⊢ ¬(a ≠ 1 ∨ b ≠ 1) ↔ a * b = 1
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
lemma indicator_prod_one {t : Set κ} {j : κ} :
    (s ×ˢ t).indicator (1 : ι × κ → M₀) (i, j) = s.indicator 1 i * t.indicator 1 j

Proof state:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (if i ∈ s ∧ j ∈ t then 1 (i, j) else 0) = (if i ∈ s then 1 i else 0) * if j ∈ t then 1 j else 0

Tactic:
split_ifs with h₀ <;> simp only [Pi.one_apply, mul_one, mul_zero] <;> tauto

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (s ×ˢ t).indicator 1 (i, j) = s.indicator 1 i * t.indicator 1 j

Tactic:
simp_rw [indicator, mem_prod_eq]

Result:
ι : Type u_1
κ : Type u_2
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s : Set ι
i : ι
t : Set κ
j : κ
⊢ (if i ∈ s ∧ j ∈ t then 1 (i, j) else 0) = (if i ∈ s then 1 i else 0) * if j ∈ t then 1 j else 0
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem IsEquivalent.refl : u ~[l] u

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ 0 =o[l] u

Tactic:
exact isLittleO_zero _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ u ~[l] u

Tactic:
rw [IsEquivalent, sub_self]

Result:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
⊢ 0 =o[l] u
-- Mathlib/MeasureTheory/Measure/Prod.lean
lemma prod_sum_left {ι : Type*} (m : ι → Measure α) (μ : Measure β) [SFinite μ] :
    (Measure.sum m).prod μ = Measure.sum (fun i ↦ (m i).prod μ)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ι : Type u_4
m : ι → Measure α
μ : Measure β
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ ((sum m).prod μ) s = (sum fun i => (m i).prod μ) s

Tactic:
simp only [prod_apply hs, lintegral_sum_measure, hs, sum_apply, ENNReal.tsum_prod']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ι : Type u_4
m : ι → Measure α
μ : Measure β
inst✝ : SFinite μ
⊢ (sum m).prod μ = sum fun i => (m i).prod μ

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ι : Type u_4
m : ι → Measure α
μ : Measure β
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ ((sum m).prod μ) s = (sum fun i => (m i).prod μ) s
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_add_aux {a b c d : ℂ} :
    (a - b) * (c + d) + (a + b) * (c - d) = 2 * (a * c - b * d)

Proof state:
a b c d : ℂ
⊢ (a - b) * (c + d) + (a + b) * (c - d) = 2 * (a * c - b * d)

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·)

Proof state:
a b : Nat
⊢ range (a + b) = range a ++ range' a b

Tactic:
simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm

Result:
no goals

Proof state:
a b : Nat
⊢ range (a + b) = range a ++ map (fun x => a + x) (range b)

Tactic:
rw [← range'_eq_map_range]

Result:
a b : Nat
⊢ range (a + b) = range a ++ range' a b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem or_all_distrib_right (l : List α) (p : α → Bool) (q : Bool) :
    (l.all p || q) = l.all fun a => p a || q

Proof state:
α : Type u_1
l : List α
p : α → Bool
q : Bool
⊢ (l.all p || q) = l.all fun a => p a || q

Tactic:
induction l with simp | cons _ _ ih => rw [Bool.or_and_distrib_right, ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
q : Bool
head✝ : α
tail✝ : List α
ih : (tail✝.all p || q) = tail✝.all fun a => p a || q
⊢ (p head✝ && tail✝.all p || q) = ((p head✝ || q) && tail✝.all fun a => p a || q)

Tactic:
rw [Bool.or_and_distrib_right, ih]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Balanced.dual : ∀ {t : Ordnode α}, Balanced t → Balanced (dual t)
  | nil, _ => ⟨⟩
  | node _ l _ r, ⟨b, bl, br⟩ => ⟨by rw [size_dual, size_dual]; exact b.symm, br.dual, bl.dual⟩

Proof state:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
⊢ BalancedSz r.dual.size l.dual.size

Tactic:
rw [size_dual, size_dual]

Result:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
⊢ BalancedSz r.size l.size

Proof state:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
⊢ BalancedSz r.size l.size

Tactic:
exact b.symm

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem submodule_comap_mul_reverse (p q : Submodule R (CliffordAlgebra Q)) :
    (p * q).comap (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) =
      q.comap (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) *
        p.comap (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
p q : Submodule R (CliffordAlgebra Q)
⊢ Submodule.comap reverse (p * q) = Submodule.comap reverse q * Submodule.comap reverse p

Tactic:
simp_rw [← submodule_map_reverse_eq_comap, submodule_map_mul_reverse]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
/-- Half of **Jordan's inequality** for `cos` and negative values. -/
lemma one_add_mul_le_cos (hx₀ : -(π / 2) ≤ x) (hx : x ≤ 0) : 1 + 2 / π * x ≤ cos x

Proof state:
x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
⊢ 1 + 2 / π * x ≤ cos x

Tactic:
simpa using one_sub_mul_le_cos (x := -x) (by linarith) (by linarith)

Result:
no goals

Proof state:
x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
⊢ 0 ≤ -x

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
⊢ -x ≤ π / 2

Tactic:
linarith

Result:
no goals