harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma setLIntegral_condKernel_univ_right (hf : Measurable f) (a : α) {s : Set β}
    (hs : MeasurableSet s) :
    ∫⁻ b in s, ∫⁻ ω, f (b, ω) ∂(Kernel.condKernel κ (a, b)) ∂(Kernel.fst κ a)
      = ∫⁻ x in s ×ˢ Set.univ, f x ∂(κ a)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ a

Tactic:
rw [← setLIntegral_condKernel hf a hs MeasurableSet.univ]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in Set.univ, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in Set.univ, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a

Tactic:
simp_rw [Measure.restrict_univ]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_preimage_eq_inter_range {f : α → β} {t : Set β} : f '' (f ⁻¹' t) = t ∩ range f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
t : Set β
⊢ f '' (f ⁻¹' t) = t ∩ range f

Tactic:
rw [image_preimage_eq_range_inter, inter_comm]

Result:
no goals
-- Mathlib/Data/Fintype/Pi.lean
@[simp]
lemma piFinset_nonempty : (piFinset s).Nonempty ↔ ∀ a, (s a).Nonempty

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
γ : α → Type u_3
s : (a : α) → Finset (γ a)
⊢ (piFinset s).Nonempty ↔ ∀ (a : α), (s a).Nonempty

Tactic:
simp [piFinset]

Result:
no goals
-- Mathlib/Order/BooleanSubalgebra.lean
@[simp, norm_cast]
lemma coe_iInf (f : ι → BooleanSubalgebra α) : ⨅ i, f i = ⋂ i, (f i : Set α)

Proof state:
ι : Sort u_1
α : Type u_2
inst✝ : BooleanAlgebra α
f : ι → BooleanSubalgebra α
⊢ ↑(⨅ i, f i) = ⋂ i, ↑(f i)

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
lemma IsLowerSet.isUpperSet_preimage_coe (hs : IsLowerSet s) :
    IsUpperSet ((↑) ⁻¹' t : Set s) ↔ ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t

Proof state:
α : Type u_1
inst✝ : LE α
s t : Set α
hs : IsLowerSet s
⊢ IsUpperSet (Subtype.val ⁻¹' t) ↔ ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_div_base {a b : ℝ} (h₁ : a ≠ 0) (h₂ : b ≠ 0) (c : ℝ) :
    logb (a / b) c = ((logb a c)⁻¹ - (logb b c)⁻¹)⁻¹

Proof state:
a b : ℝ
h₁ : a ≠ 0
h₂ : b ≠ 0
c : ℝ
⊢ logb (a / b) c = ((logb a c)⁻¹ - (logb b c)⁻¹)⁻¹

Tactic:
rw [← inv_logb_div_base h₁ h₂ c, inv_inv]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem add_le_mul_two_add [ZeroLEOneClass α] [MulPosMono α] [AddLeftMono α]
    (a2 : 2 ≤ a) (b0 : 0 ≤ b) : a + (2 + b) ≤ a * (2 + b) :=
  calc
    a + (2 + b) ≤ a + (a + a * b) :=
      add_le_add_left (add_le_add a2 <| le_mul_of_one_le_left b0 <| one_le_two.trans a2) a
    _ ≤ a * (2 + b)

Proof state:
α : Type u
inst✝⁴ : Semiring α
inst✝³ : Preorder α
a b : α
inst✝² : ZeroLEOneClass α
inst✝¹ : MulPosMono α
inst✝ : AddLeftMono α
a2 : 2 ≤ a
b0 : 0 ≤ b
⊢ a + (a + a * b) ≤ a * (2 + b)

Tactic:
rw [mul_add, mul_two, add_assoc]

Result:
no goals
-- Mathlib/Probability/Variance.lean
theorem variance_mul (c : ℝ) (X : Ω → ℝ) (μ : Measure Ω) :
    variance (fun ω => c * X ω) μ = c ^ 2 * variance X μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ c ^ 2 * eVar[X; μ].toReal = c ^ 2 * Var[X; μ]

Tactic:
rfl

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ Var[fun ω => c * X ω; μ] = c ^ 2 * Var[X; μ]

Tactic:
rw [variance, evariance_mul, ENNReal.toReal_mul, ENNReal.toReal_ofReal (sq_nonneg _)]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ c ^ 2 * eVar[X; μ].toReal = c ^ 2 * Var[X; μ]
-- Mathlib/Analysis/Normed/Module/Basic.lean
theorem norm_algebraMap' [NormOneClass 𝕜'] (x : 𝕜) : ‖algebraMap 𝕜 𝕜' x‖ = ‖x‖

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x : 𝕜
⊢ ‖(algebraMap 𝕜 𝕜') x‖ = ‖x‖

Tactic:
rw [norm_algebraMap, norm_one, mul_one]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_sub_Ico : (fun x => a - x) ⁻¹' Ico b c = Ioc (a - c) (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) ⁻¹' Ico b c = Ioc (a - c) (a - b)

Tactic:
simp [← Ioi_inter_Iic, ← Ici_inter_Iio, inter_comm]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem filter_union_right (s : Finset α) : s.filter p ∪ s.filter q = s.filter fun x => p x ∨ q x :=
  ext fun x => by simp [mem_filter, mem_union, ← and_or_left]

Proof state:
α : Type u_1
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
x : α
⊢ x ∈ filter p s ∪ filter q s ↔ x ∈ filter (fun x => p x ∨ q x) s

Tactic:
simp [mem_filter, mem_union, ← and_or_left]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
lemma coeSubgraph_adj {G' : G.Subgraph} (G'' : G'.coe.Subgraph) (v w : V) :
    (G'.coeSubgraph G'').Adj v w ↔
      ∃ (hv : v ∈ G'.verts) (hw : w ∈ G'.verts), G''.Adj ⟨v, hv⟩ ⟨w, hw⟩

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
v w : V
⊢ (Subgraph.coeSubgraph G'').Adj v w ↔ ∃ (hv : v ∈ G'.verts) (hw : w ∈ G'.verts), G''.Adj ⟨v, hv⟩ ⟨w, hw⟩

Tactic:
simp [Relation.Map]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean
theorem liftAlternating_algebraMap (f : ∀ i, M [⋀^Fin i]→ₗ[R] N) (r : R) :
    liftAlternating (R := R) (M := M) (N := N) f (algebraMap _ (ExteriorAlgebra R M) r) =
    r • f 0 0

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
r : R
⊢ (liftAlternating f) ((algebraMap R (ExteriorAlgebra R M)) r) = r • (f 0) 0

Tactic:
rw [Algebra.algebraMap_eq_smul_one, map_smul, liftAlternating_one]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive] lemma pow_mem_pow (ha : a ∈ s) : a ^ n ∈ s ^ n

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
a : α
n : ℕ
ha : a ∈ s
⊢ a ^ n ∈ s ^ n

Tactic:
simpa using pow_subset_pow_left (singleton_subset_iff.2 ha)

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_length (l : List α) : rotate l l.length = l

Proof state:
α : Type u
l : List α
⊢ l.rotate l.length = l

Tactic:
rw [rotate_eq_rotate', rotate'_length]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem eq_mk'_iff_mul_eq {x} {y : S} {z} : z = f.mk' x y ↔ z * f.toMap y = f.toMap x :=
  ⟨fun H ↦ by rw [H, mk'_spec], fun H ↦ by rw [mk', mul_inv_right, H]⟩

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
z : N
H : z = f.mk' x y
⊢ z * f.toMap ↑y = f.toMap x

Tactic:
rw [H, mk'_spec]

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
z : N
H : z * f.toMap ↑y = f.toMap x
⊢ z = f.mk' x y

Tactic:
rw [mk', mul_inv_right, H]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem aeval_eq_prod_aroots_sub_of_monic_of_splits [Algebra K L] {p : K[X]} (m : Monic p)
    (hsplit : Splits (algebraMap K L) p) (v : L) :
    aeval v p = ((p.aroots L).map fun a ↦ v - a).prod

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
m : p.Monic
hsplit : Splits (algebraMap K L) p
v : L
⊢ (aeval v) p = (Multiset.map (fun a => v - a) (p.aroots L)).prod

Tactic:
simp [aeval_eq_prod_aroots_sub_of_splits hsplit, m]

Result:
no goals
-- Mathlib/Data/Multiset/Nodup.lean
theorem Nodup.mem_erase_iff [DecidableEq α] {a b : α} {l} (d : Nodup l) :
    a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
l : Multiset α
d : l.Nodup
⊢ a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l

Tactic:
rw [d.erase_eq_filter b, mem_filter, and_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_bmod (a b : Int) (n : Nat) : (a + b).bmod n = (a.bmod n + b.bmod n).bmod n

Proof state:
a b : Int
n : Nat
⊢ (a + b).bmod n = (a.bmod n + b.bmod n).bmod n

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Extend.lean
theorem extendTo𝕜'_apply_re (fr : F →ₗ[ℝ] ℝ) (x : F) : re (fr.extendTo𝕜' x : 𝕜) = fr x

Proof state:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
F : Type u_2
inst✝³ : AddCommGroup F
inst✝² : Module ℝ F
inst✝¹ : Module 𝕜 F
inst✝ : IsScalarTower ℝ 𝕜 F
fr : F →ₗ[ℝ] ℝ
x : F
⊢ re (fr.extendTo𝕜' x) = fr x

Tactic:
simp only [extendTo𝕜'_apply, map_sub, zero_mul, mul_zero, sub_zero,
  rclike_simps]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_eq_flatten_iff {xs : List (List α)} {ys zs : List α} :
    ys ++ zs = xs.flatten ↔
      (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
        ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧
          zs = c :: cs ++ ds.flatten

Proof state:
α : Type u_1
xs : List (List α)
ys zs : List α
⊢ ys ++ zs = xs.flatten ↔
    (∃ as bs, xs = as ++ bs ∧ ys = as.flatten ∧ zs = bs.flatten) ∨
      ∃ as bs c cs ds, xs = as ++ (bs ++ c :: cs) :: ds ∧ ys = as.flatten ++ bs ∧ zs = c :: cs ++ ds.flatten

Tactic:
rw [eq_comm, flatten_eq_append_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem cancel_unit_right_assoc {W X X' Y : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) :
    f ≫ g ≫ e.unit.app Y = f' ≫ g' ≫ e.unit.app Y ↔ f ≫ g = f' ≫ g'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
W X X' Y : C
f : W ⟶ X
g : X ⟶ Y
f' : W ⟶ X'
g' : X' ⟶ Y
⊢ f ≫ g ≫ e.unit.app Y = f' ≫ g' ≫ e.unit.app Y ↔ f ≫ g = f' ≫ g'

Tactic:
simp only [← Category.assoc, cancel_mono]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem coe_eq_pair {s : Finset α} {a b : α} : (s : Set α) = {a, b} ↔ s = {a, b}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
⊢ ↑s = {a, b} ↔ s = {a, b}

Tactic:
rw [← coe_pair, coe_inj]

Result:
no goals
-- Mathlib/RingTheory/Derivation/MapCoeffs.lean
@[simp]
lemma mapCoeffs_monomial (n : ℕ) (x : A) :
    mapCoeffs (monomial n x) = monomial n x′

Proof state:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Differential A
n : ℕ
x : A
⊢ mapCoeffs ((monomial n) x) = (monomial n) x′

Tactic:
simp [mapCoeffs]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mkRat_zero (n) : mkRat n 0 = 0

Proof state:
n : Int
⊢ mkRat n 0 = 0

Tactic:
simp [mkRat_def]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem isUnit_diagonal {v : n → α} : IsUnit (diagonal v) ↔ IsUnit v

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
⊢ IsUnit (diagonal v) ↔ IsUnit v

Tactic:
simp only [← nonempty_invertible_iff_isUnit,
  (diagonalInvertibleEquivInvertible v).nonempty_congr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Relabel.lean
theorem relabel_id : relabel id x = x

Proof state:
α✝ : Type u_1
x : CNF α✝
⊢ relabel id x = x

Tactic:
simp [relabel]

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem mem_smul_iff_of_ne {i j : ι} (hij : i ≠ j) {m₁ : M i} {m₂ : M j} {w : Word M} :
    ⟨_, m₁⟩ ∈ (of m₂ • w).toList ↔ ⟨i, m₁⟩ ∈ w.toList

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
hij : i ≠ j
m₁ : M i
m₂ : M j
w : Word M
⊢ ⟨i, m₁⟩ ∈ (of m₂ • w).toList ↔ ⟨i, m₁⟩ ∈ w.toList

Tactic:
simp [mem_smul_iff, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem dropLast_cons_of_ne_nil {α : Type u} {x : α}
    {l : List α} (h : l ≠ []) : (x :: l).dropLast = x :: l.dropLast

Proof state:
α : Type u
x : α
l : List α
h : l ≠ []
⊢ (x :: l).dropLast = x :: l.dropLast

Tactic:
simp [dropLast, h]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem postcomp_map_heq' (H : D ⥤ E) (hobj : ∀ X : C, F.obj X = G.obj X)
    (hmap : ∀ {X Y} (f : X ⟶ Y), HEq (F.map f) (G.map f)) :
    HEq ((F ⋙ H).map f) ((G ⋙ H).map f)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y : C
f : X ⟶ Y
H : D ⥤ E
hobj : ∀ (X : C), F.obj X = G.obj X
hmap : ∀ {X Y : C} (f : X ⟶ Y), HEq (F.map f) (G.map f)
⊢ HEq ((F ⋙ H).map f) ((G ⋙ H).map f)

Tactic:
rw [Functor.hext hobj fun _ _ => hmap]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem natCast_def' (n : ℕ) : (n : A ⊗[R] B) = (1 : A) ⊗ₜ (n : B)

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoidWithOne A
inst✝² : Module R A
inst✝¹ : AddCommMonoidWithOne B
inst✝ : Module R B
n : ℕ
⊢ ↑n = 1 ⊗ₜ[R] ↑n

Tactic:
rw [natCast_def, ← nsmul_one, smul_tmul, nsmul_one]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigOWith_neg_right : (IsBigOWith c l f fun x => -g' x) ↔ IsBigOWith c l f g'

Proof state:
α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
c : ℝ
f : α → E
g' : α → F'
l : Filter α
⊢ (IsBigOWith c l f fun x => -g' x) ↔ IsBigOWith c l f g'

Tactic:
simp only [IsBigOWith_def, norm_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem homEquiv_leftAdjointUniq_hom_app {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
    (x : C) : adj1.homEquiv _ _ ((leftAdjointUniq adj1 adj2).hom.app x) = adj2.unit.app x

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : C
⊢ (adj1.homEquiv x (F'.obj x)) ((adj1.leftAdjointUniq adj2).hom.app x) = adj2.unit.app x

Tactic:
simp [leftAdjointUniq]

Result:
no goals
-- Mathlib/Algebra/Category/MonCat/Basic.lean
@[to_additive]
lemma inv_hom_apply {M N : MonCat} (e : M ≅ N) (x : M) : e.inv (e.hom x) = x

Proof state:
M N : MonCat
e : M ≅ N
x : ↑M
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/Finite/Polynomial.lean
theorem eq_zero_of_eval_eq_zero [Finite σ] (p : MvPolynomial σ K) (h : ∀ v : σ → K, eval v p = 0)
    (hp : p ∈ restrictDegree σ K (Fintype.card K - 1)) : p = 0 :=
  let p' : R σ K := ⟨p, hp⟩
  have : p' ∈ ker (evalᵢ σ K) := funext h
  show p'.1 = (0 : R σ K).1 from congr_arg _ <| by rwa [ker_evalₗ, mem_bot] at this

Proof state:
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
p : MvPolynomial σ K
h : ∀ (v : σ → K), (eval v) p = 0
hp : p ∈ restrictDegree σ K (Fintype.card K - 1)
p' : R σ K := ⟨p, hp⟩
this : p' ∈ ker (evalᵢ σ K)
⊢ p' = 0

Tactic:
rwa [ker_evalₗ, mem_bot] at this

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_mul_Ioo_of_neg (a b : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Ioo a b = Ioo (b / c) (a / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : c < 0
⊢ (fun x => c * x) ⁻¹' Ioo a b = Ioo (b / c) (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Ioo_of_neg a b h

Result:
no goals
-- Mathlib/Analysis/Fourier/ZMod.lean
/-- For a primitive Dirichlet character `χ`, the Fourier transform of `χ` is a constant multiple
of `χ⁻¹` (and the constant is essentially the Gauss sum). -/
lemma IsPrimitive.fourierTransform_eq_inv_mul_gaussSum {χ : DirichletCharacter ℂ N}
    (hχ : IsPrimitive χ) (k : ZMod N) :
    𝓕 χ k = χ⁻¹ (-k) * gaussSum χ stdAddChar

Proof state:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
k : ZMod N
⊢ 𝓕 (⇑χ) k = χ⁻¹ (-k) * gaussSum χ stdAddChar

Tactic:
rw [fourierTransform_eq_gaussSum_mulShift, gaussSum_mulShift_of_isPrimitive _ hχ]

Result:
no goals
-- Mathlib/Tactic/NormNum/NatLog.lean
private lemma nat_log_helper0 (b n : Nat) (hl : Nat.blt n b = true) :
    Nat.log b n = 0

Proof state:
b n : ℕ
hl : n < b
⊢ Nat.log b n = 0

Tactic:
simp [hl]

Result:
no goals

Proof state:
b n : ℕ
hl : n.blt b = true
⊢ Nat.log b n = 0

Tactic:
rw [Nat.blt_eq] at hl

Result:
b n : ℕ
hl : n < b
⊢ Nat.log b n = 0
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem Finset.nnnorm_prod_le' {α : Type*} [NormedCommRing α] (s : Finset ι) (hs : s.Nonempty)
    (f : ι → α) : ‖∏ i ∈ s, f i‖₊ ≤ ∏ i ∈ s, ‖f i‖₊ :=
  (s.norm_prod_le' hs f).trans_eq <| by simp [NNReal.coe_prod]

Proof state:
ι : Type u_4
α : Type u_5
inst✝ : NormedCommRing α
s : Finset ι
hs : s.Nonempty
f : ι → α
⊢ ∏ i ∈ s, ‖f i‖ = (fun a => ↑a) (∏ i ∈ s, ‖f i‖₊)

Tactic:
simp [NNReal.coe_prod]

Result:
no goals
-- Mathlib/GroupTheory/Order/Min.lean
@[simp]
lemma minOrder_of_prime {p : ℕ} (hp : p.Prime) : minOrder (ZMod p) = p

Proof state:
p : ℕ
hp : Nat.Prime p
⊢ minOrder (ZMod p) = ↑p

Tactic:
rw [ZMod.minOrder hp.ne_zero hp.ne_one, hp.minFac_eq]

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
/-- As `sSup s = 0` when `s` is a set of reals that's either empty or unbounded above,
it suffices to show that all elements of `s` are nonnegative to show that `0 ≤ sSup s`. -/
lemma sSup_nonneg (hs : ∀ x ∈ s, 0 ≤ x) : 0 ≤ sSup s

Proof state:
case inr.intro
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
x : ℝ
hx : x ∈ s
⊢ 0 ≤ sSup s

Tactic:
exact sSup_nonneg' ⟨x, hx, hs _ hx⟩

Result:
no goals

Proof state:
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
⊢ 0 ≤ sSup s

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Result:
case inl
hs : ∀ x ∈ ∅, 0 ≤ x
⊢ 0 ≤ sSup ∅

case inr.intro
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
x : ℝ
hx : x ∈ s
⊢ 0 ≤ sSup s

Proof state:
case inl
hs : ∀ x ∈ ∅, 0 ≤ x
⊢ 0 ≤ sSup ∅

Tactic:
exact sSup_empty.ge

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem root_mul_left_of_isRoot (p : R[X]) {q : R[X]} : IsRoot q a → IsRoot (p * q) a := fun H => by
  rw [IsRoot, eval_mul, IsRoot.def.1 H, mul_zero]

Proof state:
R : Type u
a : R
inst✝ : CommSemiring R
p q : R[X]
H : q.IsRoot a
⊢ (p * q).IsRoot a

Tactic:
rw [IsRoot, eval_mul, IsRoot.def.1 H, mul_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_eq_of_eq_mul_left (H1 : 0 < n) (H2 : m = k * n) : m / n = k :=
by rw [H2, Nat.mul_div_cancel _ H1]

Proof state:
n m k : Nat
H1 : 0 < n
H2 : m = k * n
⊢ m / n = k

Tactic:
rw [H2, Nat.mul_div_cancel _ H1]

Result:
no goals
-- Mathlib/GroupTheory/Subgroup/Centralizer.lean
@[to_additive]
lemma mem_centralizer_singleton_iff {g k : G} :
    k ∈ Subgroup.centralizer {g} ↔ k * g = g * k

Proof state:
G : Type u_1
inst✝ : Group G
g k : G
⊢ k ∈ centralizer {g} ↔ k * g = g * k

Tactic:
simp only [mem_centralizer_iff, Set.mem_singleton_iff, forall_eq]

Result:
G : Type u_1
inst✝ : Group G
g k : G
⊢ g * k = k * g ↔ k * g = g * k

Proof state:
G : Type u_1
inst✝ : Group G
g k : G
⊢ g * k = k * g ↔ k * g = g * k

Tactic:
exact eq_comm

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
lemma pmap_pmap {P : α → Prop} {Q : β → Prop} (f : ∀ a, P a → β) (g : ∀ b, Q b → γ)
    (z : Sym2 α) (h : ∀ a ∈ z, P a) (h' : ∀ b ∈ z.pmap f h, Q b) :
    (z.pmap f h).pmap g h' = z.pmap (fun a ha => g (f a (h a ha))
    (h' _ ((mem_pmap_iff f z h _).mpr ⟨a, ha, rfl⟩))) (fun _ ha ↦ ha)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : (b : β) → Q b → γ
z : Sym2 α
h : ∀ a ∈ z, P a
h' : ∀ b ∈ pmap f z h, Q b
⊢ pmap g (pmap f z h) h' = pmap (fun a ha => g (f a ⋯) ⋯) z ⋯

Tactic:
induction' z with x y

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : (b : β) → Q b → γ
x y : α
h : ∀ a ∈ s(x, y), P a
h' : ∀ b ∈ pmap f s(x, y) h, Q b
⊢ pmap g (pmap f s(x, y) h) h' = pmap (fun a ha => g (f a ⋯) ⋯) s(x, y) ⋯

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
Q : β → Prop
f : (a : α) → P a → β
g : (b : β) → Q b → γ
x y : α
h : ∀ a ∈ s(x, y), P a
h' : ∀ b ∈ pmap f s(x, y) h, Q b
⊢ pmap g (pmap f s(x, y) h) h' = pmap (fun a ha => g (f a ⋯) ⋯) s(x, y) ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Filter/Tendsto.lean
theorem tendsto_comap_iff {f : α → β} {g : β → γ} {a : Filter α} {c : Filter γ} :
    Tendsto f a (c.comap g) ↔ Tendsto (g ∘ f) a c :=
  ⟨fun h => tendsto_comap.comp h, fun h => map_le_iff_le_comap.mp <| by rwa [map_map]⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
a : Filter α
c : Filter γ
h : Tendsto (g ∘ f) a c
⊢ map g (map f a) ≤ c

Tactic:
rwa [map_map]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma homologyMap_comm :
    homologyMap φ ≫ h₂.homologyIso.hom = h₁.homologyIso.hom ≫ γ.φH

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ homologyMap φ ≫ h₂.homologyIso.hom = h₁.homologyIso.hom ≫ γ.φH

Tactic:
simp only [γ.homologyMap_eq, assoc, Iso.inv_hom_id, comp_id]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem Ici_iSup₂ (f : ∀ i, κ i → α) : Ici (⨆ (i) (j), f i j) = ⨆ (i) (j), Ici (f i j)

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Ici (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, Ici (f i j)

Tactic:
simp_rw [Ici_iSup]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem sinh_nonneg_iff : 0 ≤ sinh x ↔ 0 ≤ x

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

Tactic:
simpa only [sinh_zero] using @sinh_le_sinh 0 x

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_eq_foldl_reverse (l : Array α) (f : α → β → β) (b) :
    l.foldr f b = l.reverse.foldl (fun x y => f y x) b

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → β → β
b : β
⊢ foldr f b l = foldl (fun x y => f y x) b l.reverse

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[simp]
lemma Nat.cast_card_eq_zero (R) [AddGroupWithOne R] [Fintype R] : (Fintype.card R : R) = 0

Proof state:
R : Type u_6
inst✝¹ : AddGroupWithOne R
inst✝ : Fintype R
⊢ ↑(card R) = 0

Tactic:
rw [← nsmul_one, card_nsmul_eq_zero]

Result:
no goals
-- Mathlib/Data/Set/Sigma.lean
theorem mk_preimage_sigma_fn_eq_if {β : Type*} [DecidablePred (· ∈ s)] (g : β → α i) :
    (fun b ↦ Sigma.mk i (g b)) ⁻¹' s.sigma t = if i ∈ s then g ⁻¹' t i else ∅ :=
  ext fun _ ↦ by split_ifs <;> simp [*]

Proof state:
ι : Type u_1
α : ι → Type u_3
s : Set ι
t : (i : ι) → Set (α i)
i : ι
β : Type u_7
inst✝ : DecidablePred fun x => x ∈ s
g : β → α i
x✝ : β
⊢ x✝ ∈ (fun b => ⟨i, g b⟩) ⁻¹' s.sigma t ↔ x✝ ∈ if i ∈ s then g ⁻¹' t i else ∅

Tactic:
split_ifs <;> simp [*]

Result:
no goals