harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Ring/Defs.lean
lemma ite_zero_mul : ite P a 0 * b = ite P (a * b) 0

Proof state:
α : Type u
inst✝¹ : MulZeroClass α
P : Prop
inst✝ : Decidable P
a b : α
⊢ (if P then a else 0) * b = if P then a * b else 0

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem Algebra.IsSeparable.insepDegree_eq [Algebra.IsSeparable F E] : insepDegree F E = 1

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
⊢ insepDegree F E = 1

Tactic:
rw [insepDegree, (separableClosure.eq_top_iff F E).2 ‹_›, IntermediateField.rank_top]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem IsSelfAdjoint.sq_nonneg {a : R} (ha : IsSelfAdjoint a) : 0 ≤ a ^ 2

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : IsSelfAdjoint a
⊢ 0 ≤ a ^ 2

Tactic:
simp [sq, ha.mul_self_nonneg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
    [Std.Irrefl (· < · : α → α → Prop)]
    [Std.Antisymm (¬ · < · : α → α → Prop)]
    [Std.Total (¬ · < · : α → α → Prop)]
    {l₁ l₂ : Array α} : l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂

Proof state:
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : Array α
⊢ l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂

Tactic:
simpa using List.le_iff_lt_or_eq (l₁ := l₁.toList) (l₂ := l₂.toList)

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean
theorem opNorm_prod (f : E →L[𝕜] F) (g : E →L[𝕜] G) : ‖f.prod g‖ = ‖(f, g)‖ :=
  le_antisymm
      (opNorm_le_bound _ (norm_nonneg _) fun x => by
        simpa only [prod_apply, Prod.norm_def, max_mul_of_nonneg, norm_nonneg] using
          max_le_max (le_opNorm f x) (le_opNorm g x)) <|
    max_le
      (opNorm_le_bound _ (norm_nonneg _) fun x =>
        (le_max_left _ _).trans ((f.prod g).le_opNorm x))
      (opNorm_le_bound _ (norm_nonneg _) fun x =>
        (le_max_right _ _).trans ((f.prod g).le_opNorm x))

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F
g : E →L[𝕜] G
x : E
⊢ ‖(f.prod g) x‖ ≤ ‖(f, g)‖ * ‖x‖

Tactic:
simpa only [prod_apply, Prod.norm_def, max_mul_of_nonneg, norm_nonneg] using
  max_le_max (le_opNorm f x) (le_opNorm g x)

Result:
no goals
-- Mathlib/Algebra/Order/Round.lean
theorem round_natCast (n : ℕ) : round (n : α) = n

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
n : ℕ
⊢ round ↑n = ↑n

Tactic:
simp [round]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem sub_eq_zero_of_eq {a b : Int} (h : a = b) : a - b = 0

Proof state:
a b : Int
h : a = b
⊢ a - b = 0

Tactic:
rw [h, Int.sub_self]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem invOneSubPow_val_one_eq_invUnitSub_one :
    (invOneSubPow S 1).val = invUnitsSub (1 : Sˣ)

Proof state:
S : Type u_1
inst✝ : CommRing S
⊢ ↑(invOneSubPow S 1) = invUnitsSub 1

Tactic:
simp [invOneSubPow, invUnitsSub]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.const_smul [AddMonoid α] [Group γ] [DistribMulAction γ α]
    (h : Periodic f c) (a : γ) : Periodic (fun x => f (a • x)) (a⁻¹ • c) := fun x => by
  simpa only [smul_add, smul_inv_smul] using h (a • x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddMonoid α
inst✝¹ : Group γ
inst✝ : DistribMulAction γ α
h : Periodic f c
a : γ
x : α
⊢ (fun x => f (a • x)) (x + a⁻¹ • c) = (fun x => f (a • x)) x

Tactic:
simpa only [smul_add, smul_inv_smul] using h (a • x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem head?_zipWith {f : α → β → γ} :
    (List.zipWith f as bs).head? = match as.head?, bs.head? with
      | some a, some b => some (f a b) | _, _ => none

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
⊢ (zipWith f as bs).head? =
    match as.head?, bs.head? with
    | some a, some b => some (f a b)
    | x, x_1 => none

Tactic:
simp [head?_eq_getElem?, getElem?_zipWith]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Ergodic.lean
theorem zero_measure {f : α → α} (hf : Measurable f) : @Ergodic α m f 0 where
  measurable := hf
  map_eq

Proof state:
α : Type u_1
m : MeasurableSpace α
f : α → α
hf : Measurable f
⊢ Measure.map f 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_insert [LawfulBEq α] (h : m.WF) {k a : α} {fallback : β a} {v : β k} :
    (m.insert k v).getD a fallback =
      if h : k == a then cast (congrArg β (eq_of_beq h)) v else m.getD a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k a : α
fallback : β a
v : β k
⊢ (m.insert k v).getD a fallback = if h : (k == a) = true then cast ⋯ v else m.getD a fallback

Tactic:
simp_to_raw using Raw₀.getD_insert

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {a : α} :
    a ∈ m → m.getKey? a = some (m.getKey! a)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
a : α
⊢ a ∈ m → m.getKey? a = some (m.getKey! a)

Tactic:
simpa [mem_iff_contains] using getKey?_eq_some_getKey!_of_contains h

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Icc_eq_zero_iff : Icc a b = 0 ↔ ¬a ≤ b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc a b = 0 ↔ ¬a ≤ b

Tactic:
rw [Icc, Finset.val_eq_zero, Finset.Icc_eq_empty_iff]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem inclusion_injective : Function.Injective (inclusion h) := fun x y ↦ by
  simp only [inclusion_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
h : N ≤ N'
x y : ↥N
⊢ (inclusion h) x = (inclusion h) y → x = y

Tactic:
simp only [inclusion_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]

Result:
no goals
-- Mathlib/FieldTheory/AbelRuffini.lean
theorem gal_C_isSolvable (x : F) : IsSolvable (C x).Gal

Proof state:
F : Type u_1
inst✝ : Field F
x : F
⊢ IsSolvable (C x).Gal

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_modify_self [LawfulBEq α] {k : α} [Inhabited (β k)] {f : β k → β k} (h : m.WF) :
    (m.modify k f).get! k = ((m.get? k).map f).get!

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
k : α
inst✝ : Inhabited (β k)
f : β k → β k
h : m.WF
⊢ (m.modify k f).get! k = (Option.map f (m.get? k)).get!

Tactic:
simp_to_raw using Raw₀.get!_modify_self

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem abs_cos_eq_of_two_zsmul_eq {θ ψ : Angle} (h : (2 : ℤ) • θ = (2 : ℤ) • ψ) :
    |cos θ| = |cos ψ|

Proof state:
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |θ.cos| = |ψ.cos|

Tactic:
exact abs_cos_eq_of_two_nsmul_eq h

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem Prop.forall_iff {p : Prop → Prop} : (∀ h, p h) ↔ p False ∧ p True :=
  ⟨fun H ↦ ⟨H _, H _⟩, fun ⟨h₁, h₂⟩ h ↦ by by_cases H : h <;> simpa only [H]⟩

Proof state:
p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
⊢ p h

Tactic:
by_cases H : h <;> simpa only [H]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
@[simp] lemma monovary_inv_right₀ (hg : StrongLT 0 g) : Monovary f g⁻¹ ↔ Antivary f g :=
  forall_swap.trans <| forall₂_congr fun i j ↦ by simp [inv_lt_inv₀ (hg _) (hg _)]

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrderedSemifield α
inst✝ : LinearOrderedSemifield β
f : ι → α
g : ι → β
hg : StrongLT 0 g
i j : ι
⊢ g⁻¹ j < g⁻¹ i → f j ≤ f i ↔ g i < g j → f j ≤ f i

Tactic:
simp [inv_lt_inv₀ (hg _) (hg _)]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem dense (hp_ne_top : p ≠ ∞) : Dense (Lp.simpleFunc E p μ : Set (Lp E p μ))

Proof state:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
hp_ne_top : p ≠ ⊤
⊢ Dense ↑(simpleFunc E p μ)

Tactic:
simpa only [denseRange_subtype_val] using simpleFunc.denseRange (E := E) (μ := μ) hp_ne_top

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
lemma unop_list_prod (l : List Mᵐᵒᵖ) : l.prod.unop = (l.map unop).reverse.prod

Proof state:
M : Type u_4
inst✝ : Monoid M
l : List Mᵐᵒᵖ
⊢ unop l.prod = (map unop l).reverse.prod

Tactic:
rw [← op_inj, op_unop, MulOpposite.op_list_prod, map_reverse, map_map, reverse_reverse,
  op_comp_unop, map_id]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem isLowerSet_iff_Iio_subset : IsLowerSet s ↔ ∀ ⦃a⦄, a ∈ s → Iio a ⊆ s

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
⊢ IsLowerSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Iio a ⊆ s

Tactic:
simp [isLowerSet_iff_forall_lt, subset_def, @forall_swap (_ ∈ s)]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
@[simp]
protected lemma map_apply (f : R →+* S) (i j : n) (g : GL n R) : map f g i j = f (g i j)

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
i j : n
g : GL n R
⊢ ↑((map f) g) i j = f (↑g i j)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem star_add_self' : star a + a = ↑(2 * a.re)

Proof state:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ star a + a = ↑(2 * a.re)

Tactic:
simp [a.star_add_self', Quaternion.coe]

Result:
no goals
-- Mathlib/Topology/SeparatedMap.lean
lemma isSeparatedMap_iff_nhds {f : X → Y} : IsSeparatedMap f ↔
    ∀ x₁ x₂, f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂

Proof state:
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsSeparatedMap f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂

Tactic:
simp_rw [isSeparatedMap_iff_disjoint_nhds, Filter.disjoint_iff]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContinuousLinearEquiv.comp_contDiff_iff (e : F ≃L[𝕜] G) :
    ContDiff 𝕜 n (e ∘ f) ↔ ContDiff 𝕜 n f

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
n : WithTop ℕ∞
e : F ≃L[𝕜] G
⊢ ContDiff 𝕜 n (⇑e ∘ f) ↔ ContDiff 𝕜 n f

Tactic:
simp only [← contDiffOn_univ, e.comp_contDiffOn_iff]

Result:
no goals
-- Mathlib/Order/Monotone/Basic.lean
theorem StrictMonoOn.lt_iff_lt (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :
    f a < f b ↔ a < b

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a < f b ↔ a < b

Tactic:
rw [lt_iff_le_not_le, lt_iff_le_not_le, hf.le_iff_le ha hb, hf.le_iff_le hb ha]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem iSup_lt_lift_of_isRegular {ι} {f : ι → Cardinal} {c} (hc : IsRegular c)
    (hι : Cardinal.lift.{v, u} #ι < c) : (∀ i, f i < c) → iSup.{max u v + 1, u + 1} f < c :=
  iSup_lt_lift.{u, v} (by rwa [hc.cof_eq])

Proof state:
ι : Type u
f : ι → Cardinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
⊢ lift.{v, u} #ι < c.ord.cof

Tactic:
rwa [hc.cof_eq]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem lsub_lt_ord_lift_of_isRegular {ι} {f : ι → Ordinal} {c} (hc : IsRegular c)
    (hι : Cardinal.lift.{v, u} #ι < c) : (∀ i, f i < c.ord) → Ordinal.lsub.{u, v} f < c.ord :=
  lsub_lt_ord_lift (by rwa [hc.cof_eq])

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
⊢ lift.{v, u} #ι < c.ord.cof

Tactic:
rwa [hc.cof_eq]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
@[simp]
lemma disjoint_prod {f' : Filter α} {g' : Filter β} :
    Disjoint (f ×ˢ g) (f' ×ˢ g') ↔ Disjoint f f' ∨ Disjoint g g'

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
f' : Filter α
g' : Filter β
⊢ Disjoint (f ×ˢ g) (f' ×ˢ g') ↔ Disjoint f f' ∨ Disjoint g g'

Tactic:
simp only [disjoint_iff, prod_inf_prod, prod_eq_bot]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
lemma nnreal_le_iff [Algebra ℝ A] {a : A}
    (ha : SpectrumRestricts a ContinuousMap.realToNNReal) {r : ℝ≥0} :
    (∀ x ∈ spectrum ℝ≥0 a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, r ≤ x

Proof state:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
r : ℝ≥0
⊢ (∀ x ∈ spectrum ℝ≥0 a, r ≤ x) ↔ ∀ x ∈ spectrum ℝ a, ↑r ≤ x

Tactic:
simp [← ha.algebraMap_image]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem norm_derivWithin_eq_norm_fderivWithin : ‖derivWithin f s x‖ = ‖fderivWithin 𝕜 f s x‖

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
⊢ ‖derivWithin f s x‖ = ‖fderivWithin 𝕜 f s x‖

Tactic:
simp [← derivWithin_fderivWithin]

Result:
no goals
-- Mathlib/Computability/NFA.lean
theorem mem_stepSet (s : σ) (S : Set σ) (a : α) : s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.step t a

Proof state:
α : Type u
σ : Type v
M : NFA α σ
s : σ
S : Set σ
a : α
⊢ s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.step t a

Tactic:
simp [stepSet]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_eq_one_iff : orderOf x = 1 ↔ x = 1

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
⊢ orderOf x = 1 ↔ x = 1

Tactic:
rw [orderOf, minimalPeriod_eq_one_iff_isFixedPt, IsFixedPt, mul_one]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Iio_diff_Iic : Iio b \ Iic a = Ioo a b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Iio b \ Iic a = Ioo a b

Tactic:
rw [diff_eq, compl_Iic, inter_comm, Ioi_inter_Iio]

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma preNormEDS'_zero : preNormEDS' b c d 0 = 0

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS' b c d 0 = 0

Tactic:
rw [preNormEDS']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_eq_append_iff {f : α → β} :
    map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Proof state:
α : Type u_1
β : Type u_2
l : List α
L₁ L₂ : List β
f : α → β
⊢ map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂

Tactic:
rw [← filterMap_eq_map, filterMap_eq_append_iff]

Result:
no goals
-- Mathlib/Control/Traversable/Instances.lean
theorem comp_traverse {α β γ} (f : β → F γ) (g : α → G β) (x : List α) :
    List.traverse (Comp.mk ∘ (f <$> ·) ∘ g) x =
    Comp.mk (List.traverse f <$> List.traverse g x)

Proof state:
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α : Type u_1
β γ : Type u
f : β → F γ
g : α → G β
x : List α
⊢ List.traverse (Comp.mk ∘ (fun x => f <$> x) ∘ g) x = Comp.mk (List.traverse f <$> List.traverse g x)

Tactic:
induction x <;> simp! [*, functor_norm] <;> rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Arsinh.lean
theorem arsinh_nonpos_iff : arsinh x ≤ 0 ↔ x ≤ 0

Proof state:
x : ℝ
⊢ arsinh x ≤ 0 ↔ x ≤ 0

Tactic:
rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem ofReal_sub (r s : ℝ) : ((r - s : ℝ) : ℂ) = r - s :=
  Complex.ext_iff.2 <| by simp [ofReal]

Proof state:
r s : ℝ
⊢ (↑(r - s)).re = (↑r - ↑s).re ∧ (↑(r - s)).im = (↑r - ↑s).im

Tactic:
simp [ofReal]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem trace_conj' {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :
    trace (M⁻¹ * N * M) = trace N

Proof state:
m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (M⁻¹ * N * M).trace = N.trace

Tactic:
rw [← h.unit_spec, ← coe_units_inv, trace_units_conj']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isGT_swap {o : Ordering} : o.swap.isGT = o.isLT

Proof state:
o : Ordering
⊢ o.swap.isGT = o.isLT

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem det_coe {g : SL(2, ℤ)} : det (Units.val <| Subtype.val <| coe g) = 1

Proof state:
g : SL(2, ℤ)
⊢ (↑↑↑g).det = 1

Tactic:
simp only [SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix, SpecialLinearGroup.det_coe, coe]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Bilinear.lean
theorem apply_mem_map₂ (f : M →ₗ[R] N →ₗ[R] P) {m : M} {n : N} {p : Submodule R M}
    {q : Submodule R N} (hm : m ∈ p) (hn : n ∈ q) : f m n ∈ map₂ f p q :=
  (le_iSup _ ⟨m, hm⟩ : _ ≤ map₂ f p q) ⟨n, hn, by rfl⟩

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
n : N
p : Submodule R M
q : Submodule R N
hm : m ∈ p
hn : n ∈ q
⊢ (f ↑⟨m, hm⟩) n = (f m) n

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma nonsingular_iff_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.Nonsingular P ↔ W.Equation P ∧ (eval P W.polynomialX ≠ 0 ∨ eval P W.polynomialY ≠ 0)

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.Nonsingular P ↔ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ (eval P) W.polynomialY ≠ 0)

Tactic:
rw [nonsingular_of_Z_ne_zero hPz, Affine.Nonsingular, ← equation_of_Z_ne_zero hPz,
  ← eval_polynomialX_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 4 hPz,
  ← eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 3 hPz]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean
theorem closedBall_eq_image (x : E) (r : ℝ) :
    closedBall x r = toEuclidean.symm '' Metric.closedBall (toEuclidean x) r

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ closedBall x r = ⇑toEuclidean.symm '' Metric.closedBall (toEuclidean x) r

Tactic:
rw [toEuclidean.image_symm_eq_preimage, closedBall_eq_preimage]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem zero_lt_one_add_norm_sq' (x : E) : 0 < 1 + ‖x‖ ^ 2

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ 0 < 1 + ‖x‖ ^ 2

Tactic:
positivity

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma pullbacks_le [P.IsStableUnderBaseChange] : P.pullbacks ≤ P

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
⊢ P.pullbacks ≤ P

Tactic:
rwa [← isStableUnderBaseChange_iff_pullbacks_le]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk_eq_mk' (s : S) (m : M) :
    LocalizedModule.mk m s = mk' (LocalizedModule.mkLinearMap S M) m s

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
m : M
⊢ LocalizedModule.mk m s = mk' (LocalizedModule.mkLinearMap S M) m s

Tactic:
rw [eq_comm, mk'_eq_iff, Submonoid.smul_def, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
  LocalizedModule.mk_cancel, LocalizedModule.mkLinearMap_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombinationLineMapWeights_apply_of_ne [DecidableEq ι] {i j t : ι} (hi : t ≠ i)
    (hj : t ≠ j) (c : k) : affineCombinationLineMapWeights i j c t = 0

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i j t : ι
hi : t ≠ i
hj : t ≠ j
c : k
⊢ affineCombinationLineMapWeights i j c t = 0

Tactic:
simp [affineCombinationLineMapWeights, hi, hj]

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem IsAtom.le_iff (h : IsAtom a) : x ≤ a ↔ x = ⊥ ∨ x = a

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a x : α
h : IsAtom a
⊢ x ≤ a ↔ x = ⊥ ∨ x = a

Tactic:
rw [le_iff_lt_or_eq, h.lt_iff]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem Prime.factorization_pos_of_dvd {n p : ℕ} (hp : p.Prime) (hn : n ≠ 0) (h : p ∣ n) :
    0 < n.factorization p

Proof state:
n p : ℕ
hp : Prime p
hn : n ≠ 0
h : p ∣ n
⊢ 0 < n.factorization p

Tactic:
rwa [← primeFactorsList_count_eq, count_pos_iff, mem_primeFactorsList_iff_dvd hn hp]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem sec_spec' {f : LocalizationMap S N} (z : N) :
    f.toMap (f.sec z).1 = f.toMap (f.sec z).2 * z

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z : N
⊢ f.toMap (f.sec z).1 = f.toMap ↑(f.sec z).2 * z

Tactic:
rw [mul_comm, sec_spec]

Result:
no goals
-- Mathlib/Order/Filter/Partial.lean
theorem tendsto_iff_ptendsto (l₁ : Filter α) (l₂ : Filter β) (s : Set α) (f : α → β) :
    Tendsto f (l₁ ⊓ 𝓟 s) l₂ ↔ PTendsto (PFun.res f s) l₁ l₂

Proof state:
α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
s : Set α
f : α → β
⊢ Tendsto f (l₁ ⊓ 𝓟 s) l₂ ↔ PTendsto (PFun.res f s) l₁ l₂

Tactic:
simp only [Tendsto, PTendsto, pmap_res]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem map_count_True_eq_filter_card (s : Multiset α) (p : α → Prop) [DecidablePred p] :
    (s.map p).count True = card (s.filter p)

Proof state:
α : Type u_1
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ count True (map p s) = (filter p s).card

Tactic:
simp only [count_eq_card_filter_eq, filter_map, card_map, Function.id_comp,
  eq_true_eq_id, Function.comp_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma smul_equiv_smul (P Q : Fin 3 → R) {u v : R} (hu : IsUnit u) (hv : IsUnit v) :
    u • P ≈ v • Q ↔ P ≈ Q

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ u • P ≈ v • Q ↔ P ≈ Q

Tactic:
rw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv, smul_eq P hu, smul_eq Q hv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_of_contains_insertIfNew' [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α}
    {v : β k} :
    (m.insertIfNew k v).contains a → ¬((k == a) ∧ m.contains k = false) → m.contains a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true

Tactic:
simp_to_model [insertIfNew] using List.containsKey_of_containsKey_insertEntryIfNew'

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_eq_zero_iff {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) :
    μ.withDensity f = 0 ↔ f =ᵐ[μ] 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ μ.withDensity f = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
rw [← measure_univ_eq_zero, withDensity_apply _ .univ, restrict_univ, lintegral_eq_zero_iff' hf]

Result:
no goals