harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Card.lean
theorem card_eq_succ : #s = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ #t = n :=
  ⟨fun h =>
    let ⟨a, has⟩ := card_pos.mp (h.symm ▸ Nat.zero_lt_succ _ : 0 < #s)
    ⟨a, s.erase a, s.not_mem_erase a, insert_erase has, by
      simp only [h, card_erase_of_mem has, Nat.add_sub_cancel_right]⟩,
    fun ⟨_, _, hat, s_eq, n_eq⟩ => s_eq ▸ n_eq ▸ card_insert_of_not_mem hat⟩

Proof state:
α : Type u_1
s : Finset α
n : ℕ
inst✝ : DecidableEq α
h : #s = n + 1
a : α
has : a ∈ s
⊢ #(s.erase a) = n

Tactic:
simp only [h, card_erase_of_mem has, Nat.add_sub_cancel_right]

Result:
no goals
-- Mathlib/GroupTheory/Exponent.lean
theorem exponent_eq_zero_iff_range_orderOf_infinite (h : ∀ g : G, 0 < orderOf g) :
    exponent G = 0 ↔ (Set.range (orderOf : G → ℕ)).Infinite

Proof state:
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : exponent G ≠ 0 ↔ (Set.range orderOf).Finite
⊢ exponent G = 0 ↔ (Set.range orderOf).Infinite

Tactic:
rwa [Ne, not_iff_comm, Iff.comm] at this

Result:
no goals

Proof state:
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = 0 ↔ (Set.range orderOf).Infinite

Tactic:
have := exponent_ne_zero_iff_range_orderOf_finite h

Result:
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : exponent G ≠ 0 ↔ (Set.range orderOf).Finite
⊢ exponent G = 0 ↔ (Set.range orderOf).Infinite
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_add_one' (hx : 0 ≤ x) (h : y + 1 ≠ 0) : x ^ (y + 1) = x ^ y * x

Proof state:
x y : ℝ
hx : 0 ≤ x
h : y + 1 ≠ 0
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
rw [rpow_add' hx h, rpow_one]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/Minpoly.lean
theorem pow_isRoot_minpoly {m : ℕ} (hcop : Nat.Coprime m n) :
    IsRoot (map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ m)

Proof state:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
hcop : m.Coprime n
⊢ (map (Int.castRingHom K) (minpoly ℤ μ)).IsRoot (μ ^ m)

Tactic:
simp only [minpoly_eq_pow_coprime h hcop, IsRoot.def, eval_map]

Result:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
hcop : m.Coprime n
⊢ eval₂ (Int.castRingHom K) (μ ^ m) (minpoly ℤ (μ ^ m)) = 0

Proof state:
n : ℕ
K : Type u_1
inst✝² : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝¹ : IsDomain K
inst✝ : CharZero K
m : ℕ
hcop : m.Coprime n
⊢ eval₂ (Int.castRingHom K) (μ ^ m) (minpoly ℤ (μ ^ m)) = 0

Tactic:
exact minpoly.aeval ℤ (μ ^ m)

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem nhds_bot_basis : (𝓝 (⊥ : EReal)).HasBasis (fun _ : ℝ ↦ True) (Iio ·)

Proof state:
case intro.intro
x : EReal
hx : ⊥ < x
y : ℚ
hxy : ↑↑y < x
⊢ ∃ i', True ∧ Iio ↑i' ⊆ Iio x

Tactic:
exact ⟨_, trivial, Iio_subset_Iio hxy.le⟩

Result:
no goals

Proof state:
⊢ (𝓝 ⊥).HasBasis (fun x => True) fun x => Iio ↑x

Tactic:
refine _root_.nhds_bot_basis.to_hasBasis (fun x hx => ?_) fun _ _ ↦ ⟨_, bot_lt_coe _, Subset.rfl⟩

Result:
x : EReal
hx : ⊥ < x
⊢ ∃ i', True ∧ Iio ↑i' ⊆ Iio x

Proof state:
x : EReal
hx : ⊥ < x
⊢ ∃ i', True ∧ Iio ↑i' ⊆ Iio x

Tactic:
rcases exists_rat_btwn_of_lt hx with ⟨y, -, hxy⟩

Result:
case intro.intro
x : EReal
hx : ⊥ < x
y : ℚ
hxy : ↑↑y < x
⊢ ∃ i', True ∧ Iio ↑i' ⊆ Iio x
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Iic_pred_eq_Iio (b : α) : Iic (pred b) = Iio b := coe_injective <| by simp

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
b : α
⊢ ↑(Iic (pred b)) = ↑(Iio b)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem hasFDerivWithinAt_comp_sub (a : E) :
    HasFDerivWithinAt (fun x ↦ f (x - a)) f' s x ↔ HasFDerivWithinAt f f' (-a +ᵥ s) (x - a)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
a : E
⊢ HasFDerivWithinAt (fun x => f (x - a)) f' s x ↔ HasFDerivWithinAt f f' (-a +ᵥ s) (x - a)

Tactic:
simpa [sub_eq_add_neg] using hasFDerivWithinAt_comp_add_right (-a)

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma mem_piFinset_iff_pivot_removeNth (p : Fin (n + 1)) :
    f ∈ piFinset s ↔ f p ∈ s p ∧ removeNth p f ∈ piFinset (removeNth p s)

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
f : (i : Fin (n + 1)) → α i
s : (i : Fin (n + 1)) → Finset (α i)
p : Fin (n + 1)
⊢ f ∈ piFinset s ↔ f p ∈ s p ∧ p.removeNth f ∈ piFinset (p.removeNth s)

Tactic:
simp only [Fintype.mem_piFinset, forall_iff_succAbove p, removeNth]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_map (p : β → Bool) (f : α → β) (l : Vector α n) :
    countP p (map f l) = countP (p ∘ f) l

Proof state:
case mk
α : Type u_2
β : Type u_1
p : β → Bool
f : α → β
l : Array α
⊢ countP p (map f { toArray := l, size_toArray := ⋯ }) = countP (p ∘ f) { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_1
n : Nat
p : β → Bool
f : α → β
l : Vector α n
⊢ countP p (map f l) = countP (p ∘ f) l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_2
β : Type u_1
p : β → Bool
f : α → β
l : Array α
⊢ countP p (map f { toArray := l, size_toArray := ⋯ }) = countP (p ∘ f) { toArray := l, size_toArray := ⋯ }
-- Mathlib/Probability/Distributions/Poisson.lean
/-- The Poisson pmf is measurable. -/
@[measurability]
lemma measurable_poissonPMFReal (r : ℝ≥0) : Measurable (poissonPMFReal r)

Proof state:
r : ℝ≥0
⊢ Measurable (poissonPMFReal r)

Tactic:
measurability

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma mem_piFinset_iff_zero_tail :
    f ∈ Fintype.piFinset s ↔ f 0 ∈ s 0 ∧ tail f ∈ piFinset (tail s)

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
f : (i : Fin (n + 1)) → α i
s : (i : Fin (n + 1)) → Finset (α i)
⊢ f ∈ piFinset s ↔ f 0 ∈ s 0 ∧ tail f ∈ piFinset (tail s)

Tactic:
simp only [Fintype.mem_piFinset, forall_fin_succ, tail]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
lemma piCongrLeft_apply_apply {ι ι' : Type*} (e : ι ≃ ι') {β : ι' → Type*}
    [∀ i', MeasurableSpace (β i')] (x : (i : ι) → β (e i)) (i : ι) :
    piCongrLeft (fun i' ↦ β i') e x (e i) = x i

Proof state:
ι : Type u_8
ι' : Type u_9
e : ι ≃ ι'
β : ι' → Type u_10
inst✝ : (i' : ι') → MeasurableSpace (β i')
x : (i : ι) → β (e i)
i : ι
⊢ (piCongrLeft (fun i' => β i') e) x (e i) = x i

Tactic:
rw [piCongrLeft, coe_mk, Equiv.piCongrLeft_apply_apply]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean
theorem mapClusterPt_self_atTop_pow (x : G) : MapClusterPt x atTop (x ^ · : ℕ → G)

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ MapClusterPt x atTop fun x_1 => x ^ x_1

Tactic:
simpa using mapClusterPt_self_zpow_atTop_pow x 1

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/End.lean
theorem iterate_surjective (h : Surjective f') : ∀ n : ℕ, Surjective (f' ^ n)
  | 0 => surjective_id
  | n + 1 => by
    rw [iterate_succ]
    exact (iterate_surjective h n).comp h

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
h : Surjective ⇑f'
n : ℕ
⊢ Surjective ⇑((f' ^ n) ∘ₗ f')

Tactic:
exact (iterate_surjective h n).comp h

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
h : Surjective ⇑f'
n : ℕ
⊢ Surjective ⇑(f' ^ (n + 1))

Tactic:
rw [iterate_succ]

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
h : Surjective ⇑f'
n : ℕ
⊢ Surjective ⇑((f' ^ n) ∘ₗ f')
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
/-- A row partitioned matrix in a Star ring when conjugate transposed gives a column partitioned
matrix with the rows of the initial matrix conjugate transposed to become columns. -/
lemma conjTranspose_fromRows_eq_fromCols_conjTranspose (A₁ : Matrix m₁ n R)
    (A₂ : Matrix m₂ n R) : conjTranspose (fromRows A₁ A₂) =
      fromCols (conjTranspose A₁) (conjTranspose A₂)

Proof state:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Star R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
⊢ (A₁.fromRows A₂)ᴴ = A₁ᴴ.fromCols A₂ᴴ

Tactic:
ext _ (_ | _) <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.toLin'_mul_apply [Fintype m] [DecidableEq m] (M : Matrix l m R) (N : Matrix m n R)
    (x) : Matrix.toLin' (M * N) x = Matrix.toLin' M (Matrix.toLin' N x)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix l m R
N : Matrix m n R
x : n → R
⊢ (toLin' (M * N)) x = (toLin' M) ((toLin' N) x)

Tactic:
rw [Matrix.toLin'_mul, LinearMap.comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem State.unsat_iff : State.Unsat state ↔ state.cnf.Unsat

Proof state:
aig✝ : AIG Nat
state : State aig✝
⊢ state.Unsat ↔ state.cnf.Unsat

Tactic:
simp [State.unsat_def]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem fg_bot : (⊥ : IntermediateField F E).FG :=
  ⟨∅, by simp only [Finset.coe_empty, adjoin_empty]⟩

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ adjoin F ↑∅ = ⊥

Tactic:
simp only [Finset.coe_empty, adjoin_empty]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_neg : sin (-x) = -sin x

Proof state:
x : ℂ
⊢ sin (-x) = -sin x

Tactic:
simp [sin, sub_eq_add_neg, exp_neg, (neg_div _ _).symm, add_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem add_right_neg (a : Int) : a + -a = 0

Proof state:
a : Int
⊢ a + -a = 0

Tactic:
rw [Int.add_comm, Int.add_left_neg]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_unit' {n : ZMod 0} : IsUnit n ↔ n.val = 1

Proof state:
n : ZMod 0
⊢ IsUnit n ↔ n.val = 1

Tactic:
simp only [val]

Result:
n : ZMod 0
⊢ IsUnit n ↔ Int.natAbs n = 1

Proof state:
n : ZMod 0
⊢ IsUnit n ↔ Int.natAbs n = 1

Tactic:
rw [Int.isUnit_iff, Int.natAbs_eq_iff, Nat.cast_one]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem filter_le_eq_Ici [DecidablePred (a ≤ ·)] : ({x | a ≤ x} : Finset _) = Ici a

Proof state:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => a ≤ x
⊢ filter (fun x => a ≤ x) univ = Ici a

Tactic:
ext

Result:
case h
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => a ≤ x
a✝ : α
⊢ a✝ ∈ filter (fun x => a ≤ x) univ ↔ a✝ ∈ Ici a

Proof state:
case h
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
a : α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun x => a ≤ x
a✝ : α
⊢ a✝ ∈ filter (fun x => a ≤ x) univ ↔ a✝ ∈ Ici a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem norm_deriv_le_of_lipschitzOn {f : 𝕜 → F} {x₀ : 𝕜} {s : Set 𝕜} (hs : s ∈ 𝓝 x₀)
    {C : ℝ≥0} (hlip : LipschitzOnWith C f s) : ‖deriv f x₀‖ ≤ C

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖deriv f x₀‖ ≤ ↑C

Tactic:
simpa [norm_deriv_eq_norm_fderiv] using norm_fderiv_le_of_lipschitzOn 𝕜 hs hlip

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_mapIdx {l : Array α} {f : Nat → α → β} {g : Nat → β → γ} :
    (l.mapIdx f).mapIdx g = l.mapIdx (fun i => g i ∘ f i)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Array α
f : Nat → α → β
g : Nat → β → γ
⊢ mapIdx g (mapIdx f l) = mapIdx (fun i => g i ∘ f i) l

Tactic:
simp [mapIdx_eq_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem coeFn_comp₂ (g : β → γ → δ) (hg : Continuous (uncurry g)) (f₁ : α →ₘ[μ] β)
    (f₂ : α →ₘ[μ] γ) : comp₂ g hg f₁ f₂ =ᵐ[μ] fun a => g (f₁ a) (f₂ a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ → δ
hg : Continuous (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(comp₂ g hg f₁ f₂) =ᶠ[ae μ] fun a => g (↑f₁ a) (↑f₂ a)

Tactic:
rw [comp₂_eq_mk]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ → δ
hg : Continuous (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯) =ᶠ[ae μ] fun a => g (↑f₁ a) (↑f₂ a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β → γ → δ
hg : Continuous (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯) =ᶠ[ae μ] fun a => g (↑f₁ a) (↑f₂ a)

Tactic:
apply coeFn_mk

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem Int.natCast_pow_pred (b p : ℕ) (w : 0 < b) : ((b ^ p - 1 : ℕ) : ℤ) = (b : ℤ) ^ p - 1

Proof state:
b p : ℕ
w : 0 < b
⊢ ↑(b ^ p - 1) = ↑b ^ p - 1

Tactic:
have : 1 ≤ b ^ p := Nat.one_le_pow p b w

Result:
b p : ℕ
w : 0 < b
this : 1 ≤ b ^ p
⊢ ↑(b ^ p - 1) = ↑b ^ p - 1

Proof state:
b p : ℕ
w : 0 < b
this : 1 ≤ b ^ p
⊢ ↑(b ^ p - 1) = ↑b ^ p - 1

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem lift_apply_inr (f : R →ₐ[S] A) (g : M →ₗ[S] A)
    (hg : ∀ x y, g x * g y = 0)
    (hfg : ∀ r x, g (r •> x) = f r * g x)
    (hgf : ∀ r x, g (x <• r) = g x * f r)
    (m : M) :
    lift f g hg hfg hgf (inr m) = g m :=
  show f 0 + g m = g m by rw [map_zero, zero_add]

Proof state:
S : Type u_1
R : Type u
M : Type v
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : Module R M
inst✝⁵ : Module Rᵐᵒᵖ M
inst✝⁴ : SMulCommClass R Rᵐᵒᵖ M
inst✝³ : IsScalarTower S R M
inst✝² : IsScalarTower S Rᵐᵒᵖ M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
m : M
⊢ f 0 + g m = g m

Tactic:
rw [map_zero, zero_add]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
lemma compProd_id_eq_copy_comp [SFinite μ] : μ ⊗ₘ Kernel.id = Kernel.copy α ∘ₘ μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ μ ⊗ₘ Kernel.id = ⇑(Kernel.copy α) ∘ₘ μ

Tactic:
rw [compProd_id, Kernel.copy, deterministic_comp_eq_map]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem Reachable.dist_eq_zero_iff (hr : G.Reachable u v) :
    G.dist u v = 0 ↔ u = v

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
hr : G.Reachable u v
⊢ G.dist u v = 0 ↔ u = v

Tactic:
simp [hr]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem whiskerLeft_hom {X Y : Mon_ C} (f : X ⟶ Y) (Z : Mon_ C) :
    (f ▷ Z).hom = f.hom ▷ Z.X

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : Mon_ C
f : X ⟶ Y
Z : Mon_ C
⊢ (f ▷ Z).hom = f.hom ▷ Z.X

Tactic:
rw [← tensorHom_id]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : Mon_ C
f : X ⟶ Y
Z : Mon_ C
⊢ (f ▷ Z).hom = f.hom ⊗ 𝟙 Z.X

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : Mon_ C
f : X ⟶ Y
Z : Mon_ C
⊢ (f ▷ Z).hom = f.hom ⊗ 𝟙 Z.X

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_fin (n : ℕ) : #(Fin n) = n

Proof state:
n : ℕ
⊢ #(Fin n) = ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem ker_eq_bot_iff_ker_flip_eq_bot (H : B.IsRefl) :
    LinearMap.ker B = ⊥ ↔ LinearMap.ker B.flip = ⊥

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
h : ker B.flip = ⊥
⊢ ker B = ⊥

Tactic:
exact (congr_arg _ B.flip_flip.symm).trans (ker_flip_eq_bot (flip_isRefl_iff.mpr H) h)

Result:
no goals

Proof state:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
⊢ ker B = ⊥ ↔ ker B.flip = ⊥

Tactic:
refine ⟨ker_flip_eq_bot H, fun h ↦ ?_⟩

Result:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
h : ker B.flip = ⊥
⊢ ker B = ⊥
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/MinMax.lean
theorem le_max_left ( a b : Nat) : a ≤ max a b

Proof state:
a b : Nat
⊢ a ≤ max a b

Tactic:
by_cases (a <= b) <;> simp [Nat.max_def, *]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem uniformContinuous_of_const [UniformSpace β] {c : α → β} (h : ∀ a b, c a = c b) :
    UniformContinuous c :=
  have : (fun x : α × α => (c x.fst, c x.snd)) ⁻¹' idRel = univ :=
    eq_univ_iff_forall.2 fun ⟨a, b⟩ => h a b
  le_trans (map_le_iff_le_comap.2 <| by simp [comap_principal, this, univ_mem]) refl_le_uniformity

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
c : α → β
h : ∀ (a b : α), c a = c b
this : (fun x => (c x.1, c x.2)) ⁻¹' idRel = univ
⊢ 𝓤 α ≤ comap (fun x => (c x.1, c x.2)) (𝓟 idRel)

Tactic:
simp [comap_principal, this, univ_mem]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
theorem cofan_inj_id (n : ℕ) : (s.cofan _).inj (IndexSet.id (op ⦋n⦌)) = s.ι n

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
n : ℕ
⊢ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) = s.ι n

Tactic:
simp [IndexSet.id, IndexSet.e, cofan_inj_eq]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem count_sum' {s : Finset β} {a : α} {f : β → Multiset α} :
    count a (∑ x ∈ s, f x) = ∑ x ∈ s, count a (f x)

Proof state:
α : Type u_3
β : Type u_4
inst✝ : DecidableEq α
s : Finset β
a : α
f : β → Multiset α
⊢ count a (∑ x ∈ s, f x) = ∑ x ∈ s, count a (f x)

Tactic:
dsimp only [Finset.sum]

Result:
α : Type u_3
β : Type u_4
inst✝ : DecidableEq α
s : Finset β
a : α
f : β → Multiset α
⊢ count a (map (fun x => f x) s.val).sum = (map (fun x => count a (f x)) s.val).sum

Proof state:
α : Type u_3
β : Type u_4
inst✝ : DecidableEq α
s : Finset β
a : α
f : β → Multiset α
⊢ count a (map (fun x => f x) s.val).sum = (map (fun x => count a (f x)) s.val).sum

Tactic:
rw [count_sum]

Result:
no goals
-- Mathlib/RingTheory/Localization/AtPrime.lean
theorem to_map_mem_maximal_iff (x : R) (h : IsLocalRing S := isLocalRing S I) :
    algebraMap R S x ∈ IsLocalRing.maximalIdeal S ↔ x ∈ I :=
  not_iff_not.mp <| by
    simpa only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] using
      isUnit_to_map_iff S I x

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
I : Ideal R
hI : I.IsPrime
inst✝ : IsLocalization.AtPrime S I
x : R
h : optParam (IsLocalRing S) ⋯
⊢ (algebraMap R S) x ∉ IsLocalRing.maximalIdeal S ↔ x ∉ I

Tactic:
simpa only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] using
  isUnit_to_map_iff S I x

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem smul_dirac_apply (a : ℝ≥0∞) (b : α) (s : Set α) :
    (a • dirac b) s = indicator s (fun _ => a) b

Proof state:
α : Type u_1
a : ℝ≥0∞
b : α
s : Set α
⊢ (a • dirac b) s = s.indicator (fun x => a) b

Tactic:
simp only [smul_apply, smul_eq_mul, dirac_apply, ← indicator_mul_right _ fun _ => a, mul_one]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem finiteMultiplicity_iff_emultiplicity_ne_top :
    FiniteMultiplicity a b ↔ emultiplicity a b ≠ ⊤

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
⊢ FiniteMultiplicity a b ↔ emultiplicity a b ≠ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lt_one_iff_zero {c : Cardinal} : c < 1 ↔ c = 0

Proof state:
c : Cardinal.{u_1}
⊢ c < 1 ↔ c = 0

Tactic:
simpa using lt_succ_bot_iff (a := c)

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem gcd_self (i : ℤ) : gcd i i = natAbs i

Proof state:
i : ℤ
⊢ i.gcd i = i.natAbs

Tactic:
simp [gcd]

Result:
no goals
-- Mathlib/Order/Part.lean
lemma Antitone.partMap (hg : Antitone g) : Antitone fun x ↦ (g x).map f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : β → γ
g : α → Part β
hg : Antitone g
⊢ Antitone fun x => map f (g x)

Tactic:
simpa only [← bind_some_eq_map] using hg.partBind antitone_const

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/EventuallyConstant.lean
@[simp]
lemma coconeιApp_eq_id : h.coconeιApp i₀ = 𝟙 _

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_4, u_1} J
inst✝¹ : Category.{u_3, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
⊢ h.coconeιApp i₀ = 𝟙 (F.obj i₀)

Tactic:
rw [h.coconeιApp_eq i₀ i₀ (𝟙 _) (𝟙 _), h.isoMap_hom_inv_id]

Result:
no goals
-- Mathlib/Data/Int/Log.lean
theorem clog_one_left (r : R) : clog 1 r = 0

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
r : R
⊢ clog 1 r = 0

Tactic:
simp only [clog, Nat.log_one_left, Nat.cast_zero, Nat.clog_one_left, neg_zero, ite_self]

Result:
no goals
-- Mathlib/RingTheory/Complex.lean
theorem Algebra.norm_complex_apply (z : ℂ) : Algebra.norm ℝ z = Complex.normSq z

Proof state:
z : ℂ
⊢ !![z.re, -z.im; z.im, z.re] 0 0 * !![z.re, -z.im; z.im, z.re] 1 1 -
      !![z.re, -z.im; z.im, z.re] 0 1 * !![z.re, -z.im; z.im, z.re] 1 0 =
    z.re * z.re + z.im * z.im

Tactic:
simp

Result:
no goals

Proof state:
z : ℂ
⊢ (norm ℝ) z = normSq z

Tactic:
rw [Algebra.norm_eq_matrix_det Complex.basisOneI, Algebra.leftMulMatrix_complex,
  Matrix.det_fin_two, normSq_apply]

Result:
z : ℂ
⊢ !![z.re, -z.im; z.im, z.re] 0 0 * !![z.re, -z.im; z.im, z.re] 1 1 -
      !![z.re, -z.im; z.im, z.re] 0 1 * !![z.re, -z.im; z.im, z.re] 1 0 =
    z.re * z.re + z.im * z.im
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem AntilipschitzWith.le_mul_norm' {f : E → F} {K : ℝ≥0} (h : AntilipschitzWith K f)
    (hf : f 1 = 1) (x) : ‖x‖ ≤ K * ‖f x‖

Proof state:
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
K : ℝ≥0
h : AntilipschitzWith K f
hf : f 1 = 1
x : E
⊢ ‖x‖ ≤ ↑K * ‖f x‖

Tactic:
simpa only [dist_one_right, hf] using h.le_mul_dist x 1

Result:
no goals
-- Mathlib/Topology/Algebra/Indicator.lean
@[to_additive]
lemma IsClopen.continuous_mulIndicator (hs : IsClopen s) (hf : Continuous f) :
    Continuous (s.mulIndicator f) :=
  hf.mulIndicator (by simp [isClopen_iff_frontier_eq_empty.mp hs])

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hs : IsClopen s
hf : Continuous f
⊢ ∀ a ∈ frontier s, f a = 1

Tactic:
simp [isClopen_iff_frontier_eq_empty.mp hs]

Result:
no goals
-- Mathlib/RingTheory/SurjectiveOnStalks.lean
lemma surjectiveOnStalks_iff_forall_maximal' :
    f.SurjectiveOnStalks ↔ ∀ I : Ideal S, I.IsMaximal →
      ∀ s : S, ∃ x r : R, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x

Proof state:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
⊢ f.SurjectiveOnStalks ↔ ∀ (I : Ideal S), I.IsMaximal → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x

Tactic:
simp only [surjectiveOnStalks_iff_forall_maximal, surjective_localRingHom_iff]

Result:
no goals