harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Complex/Basic.lean
@[norm_cast] lemma ofReal_zsmul (n : ℤ) (r : ℝ) : ↑(n • r) = n • (r : ℂ)

Proof state:
n : ℤ
r : ℝ
⊢ ↑(n • r) = n • ↑r

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem mapsTo_preimage (h : Semiconj f fa fb) {s t : Set β} (hb : MapsTo fb s t) :
    MapsTo fa (f ⁻¹' s) (f ⁻¹' t) := fun x hx => by simp only [mem_preimage, h x, hb hx]

Proof state:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s t : Set β
hb : MapsTo fb s t
x : α
hx : x ∈ f ⁻¹' s
⊢ fa x ∈ f ⁻¹' t

Tactic:
simp only [mem_preimage, h x, hb hx]

Result:
no goals
-- Mathlib/Order/Category/Lat.lean
lemma id_apply (X : Lat) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : Lat
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_fst_unzip (as : Array (α × β)) :
    as.unzip.1.toList = as.toList.unzip.1

Proof state:
α : Type u_1
β : Type u_2
as : Array (α × β)
⊢ as.unzip.fst.toList = as.toList.unzip.fst

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_empty [IsEmpty β] : ∏' b, f b = 1

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : IsEmpty β
⊢ ∏' (b : β), f b = 1

Tactic:
rw [tprod_eq_prod (s := (∅ : Finset β))] <;> simp

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_pow_dvd (n : ℕ) : orderOf (x ^ n) ∣ orderOf x

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
⊢ orderOf (x ^ n) ∣ orderOf x

Tactic:
rw [orderOf_dvd_iff_pow_eq_one, pow_right_comm, pow_orderOf_eq_one, one_pow]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean
@[reassoc (attr := simp)]
lemma extendCyclesIso_inv_iCycles :
    (K.extendCyclesIso e hj').inv ≫ (K.extend e).iCycles j' =
      K.iCycles j ≫ (K.extendXIso e hj').inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.extendCyclesIso e hj').inv ≫ (K.extend e).iCycles j' = K.iCycles j ≫ (K.extendXIso e hj').inv

Tactic:
simp only [← cancel_epi (K.extendCyclesIso e hj').hom, Iso.hom_inv_id_assoc,
  extendCyclesIso_hom_iCycles_assoc, Iso.hom_inv_id, comp_id]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem _root_.Matrix.Nondegenerate.toBilin' {M : Matrix ι ι R₂} (h : M.Nondegenerate) :
    M.toBilin'.Nondegenerate := fun x hx =>
  h.eq_zero_of_ortho fun y => by simpa only [toBilin'_apply'] using hx y

Proof state:
R₂ : Type u_3
inst✝² : CommRing R₂
ι : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
M : Matrix ι ι R₂
h : M.Nondegenerate
x : ι → R₂
hx : ∀ (n : ι → R₂), ((Matrix.toBilin' M) x) n = 0
y : ι → R₂
⊢ x ⬝ᵥ M *ᵥ y = 0

Tactic:
simpa only [toBilin'_apply'] using hx y

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
theorem norm_inl (r : R) : ‖(inl r : tsze R M)‖ = ‖r‖

Proof state:
R : Type u_3
M : Type u_4
inst✝¹ : SeminormedRing R
inst✝ : SeminormedAddCommGroup M
r : R
⊢ ‖inl r‖ = ‖r‖

Tactic:
simp [norm_def]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tan_zero : tan 0 = 0

Proof state:
⊢ tan 0 = 0

Tactic:
simp [tan]

Result:
no goals
-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem Martingale.ae_not_tendsto_atTop_atBot [IsFiniteMeasure μ] (hf : Martingale f ℱ μ)
    (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) :
    ∀ᵐ ω ∂μ, ¬Tendsto (fun n => f n ω) atTop atBot

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => f n ω) atTop atBot

Tactic:
filter_upwards [hf.bddAbove_range_iff_bddBelow_range hbdd] with ω hω htop using
  unbounded_of_tendsto_atBot htop (hω.1 <| bddAbove_range_of_tendsto_atTop_atBot htop)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.map_id_id {X Y : C} [HasBinaryProduct X Y] : prod.map (𝟙 X) (𝟙 Y) = 𝟙 _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ map (𝟙 X) (𝟙 Y) = 𝟙 (X ⨯ Y)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.inf_nhdsSet_eq_biSup {K : Set X} (hK : IsCompact K) (l : Filter X) :
    l ⊓ (𝓝ˢ K) = ⨆ x ∈ K, l ⊓ 𝓝 x

Proof state:
X : Type u
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
l : Filter X
⊢ l ⊓ 𝓝ˢ K = ⨆ x ∈ K, l ⊓ 𝓝 x

Tactic:
simp only [inf_comm l, hK.nhdsSet_inf_eq_biSup]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
lemma mul_delta {f : ℕ → ℂ} (h : f 1 = 1) : f * δ = δ

Proof state:
f : ℕ → ℂ
h : f 1 = 1
⊢ f * δ = δ

Tactic:
rw [mul_delta_eq_smul_delta, h, one_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem lt_trans : ∀ {x y z : Bool}, x < y → y < z → x < z

Proof state:
⊢ ∀ {x y z : Bool}, x < y → y < z → x < z

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast_insertEntry_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
    {v : β k} : getValueCast k (insertEntry k v l) containsKey_insertEntry_self = v

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ getValueCast k (insertEntry k v l) ⋯ = v

Tactic:
simp [getValueCast_insertEntry]

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem tendsto_nhds_bot_iff_real {α : Type*} {m : α → EReal} {f : Filter α} :
    Tendsto m f (𝓝 ⊥) ↔ ∀ x : ℝ, ∀ᶠ a in f, m a < x :=
  nhds_bot_basis.tendsto_right_iff.trans <| by simp only [true_implies, mem_Iio]

Proof state:
α : Type u_2
m : α → EReal
f : Filter α
⊢ (∀ (i : ℝ), True → ∀ᶠ (x : α) in f, m x ∈ Iio ↑i) ↔ ∀ (x : ℝ), ∀ᶠ (a : α) in f, m a < ↑x

Tactic:
simp only [true_implies, mem_Iio]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem sSup_sUnion (s : Set (Set β)) : sSup (⋃₀ s) = ⨆ t ∈ s, sSup t

Proof state:
β : Type u_2
inst✝ : CompleteLattice β
s : Set (Set β)
⊢ sSup (⋃₀ s) = ⨆ t ∈ s, sSup t

Tactic:
simp only [sUnion_eq_biUnion, sSup_eq_iSup, iSup_iUnion]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.le_basis_iff (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
    l ≤ l' ↔ ∀ i', p' i' → ∃ i, p i ∧ s i ⊆ s' i'

Proof state:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ l ≤ l' ↔ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'

Tactic:
simp only [hl'.ge_iff, hl.mem_iff]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
lemma trunc_one_X : trunc (R := R) 1 X = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ trunc 1 X = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
theorem sumIDeriv_C (a : R) : sumIDeriv (C a) = C a

Proof state:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ sumIDeriv (C a) = C a

Tactic:
rw [sumIDeriv_apply, natDegree_C, zero_add, sum_range_one, Function.iterate_zero_apply]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem nnnorm_eq_iSup_nnnorm : ‖f‖₊ = ⨆ x : α, ‖f x‖₊ :=
  Subtype.ext <| (norm_eq_iSup_norm f).trans <| by simp_rw [val_eq_coe, NNReal.coe_iSup, coe_nnnorm]

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ⨆ x, ‖f x‖ = ↑(⨆ x, ‖f x‖₊)

Tactic:
simp_rw [val_eq_coe, NNReal.coe_iSup, coe_nnnorm]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem image_subset_image {s₁ s₂ : Finset α} (h : s₁ ⊆ s₂) : s₁.image f ⊆ s₂.image f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ image f s₁ ⊆ image f s₂

Tactic:
simp only [subset_def, image_val, subset_dedup', dedup_subset', Multiset.map_subset_map h]

Result:
no goals
-- Mathlib/NumberTheory/Rayleigh.lean
theorem compl_beattySeq' {r s : ℝ} (hrs : r.IsConjExponent s) :
    {beattySeq' r k | k}ᶜ = {beattySeq s k | k}

Proof state:
r s : ℝ
hrs : r.IsConjExponent s
⊢ {x | ∃ k, beattySeq' r k = x}ᶜ = {x | ∃ k, beattySeq s k = x}

Tactic:
rw [← compl_beattySeq hrs.symm, compl_compl]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem accPt_iff_frequently (x : X) (C : Set X) : AccPt x (𝓟 C) ↔ ∃ᶠ y in 𝓝 x, y ≠ x ∧ y ∈ C

Proof state:
X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ AccPt x (𝓟 C) ↔ ∃ᶠ (y : X) in 𝓝 x, y ≠ x ∧ y ∈ C

Tactic:
simp [acc_principal_iff_cluster, clusterPt_principal_iff_frequently, and_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem neg_inj {a b : Int} : -a = -b ↔ a = b :=
  ⟨fun h => by rw [← Int.neg_neg a, ← Int.neg_neg b, h], congrArg _⟩

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

Tactic:
rw [← Int.neg_neg a, ← Int.neg_neg b, h]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
@[simp]
lemma totallyBounded_insert (a : α) {s : Set α} :
    TotallyBounded (insert a s) ↔ TotallyBounded s

Proof state:
α : Type u
uniformSpace : UniformSpace α
a : α
s : Set α
⊢ TotallyBounded (insert a s) ↔ TotallyBounded s

Tactic:
simp_rw [← singleton_union, totallyBounded_union, totallyBounded_singleton, true_and]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem add_pf_add_lt (a₁ : R) (_ : a₂ + b = c) : (a₁ + a₂) + b = a₁ + c

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a₂ b c a₁ : R
x✝ : a₂ + b = c
⊢ a₁ + a₂ + b = a₁ + c

Tactic:
simp [*, add_assoc]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See also `lt_inv_of_lt_inv₀` for a one-sided implication with one fewer assumption. -/
lemma lt_inv_comm₀ (ha : 0 < a) (hb : 0 < b) : a < b⁻¹ ↔ b < a⁻¹

Proof state:
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : ZeroLEOneClass G₀
inst✝² : PosMulReflectLT G₀
a b : G₀
inst✝¹ : MulPosStrictMono G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
hb : 0 < b
⊢ a < b⁻¹ ↔ b < a⁻¹

Tactic:
rw [← inv_lt_inv₀ (inv_pos.2 hb) ha, inv_inv]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem continuous_of_uniform_approx_of_continuous
    (L : ∀ u ∈ 𝓤 β, ∃ F, Continuous F ∧ ∀ y, (f y, F y) ∈ u) : Continuous f :=
  continuous_iff_continuousOn_univ.mpr <|
    continuousOn_of_uniform_approx_of_continuousOn <| by
      simpa [continuous_iff_continuousOn_univ] using L

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace β
f : α → β
inst✝ : TopologicalSpace α
L : ∀ u ∈ 𝓤 β, ∃ F, Continuous F ∧ ∀ (y : α), (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ F, ContinuousOn F univ ∧ ∀ y ∈ univ, (f y, F y) ∈ u

Tactic:
simpa [continuous_iff_continuousOn_univ] using L

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem b_ne_one' : b ≠ 1

Proof state:
b : ℝ
hb : 1 < b
⊢ b ≠ 1

Tactic:
linarith

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem one_ascFactorial : ∀ (k : ℕ), (1 : ℕ).ascFactorial k = k.factorial
  | 0 => ascFactorial_zero 1
  | (k+1) => by
    rw [ascFactorial_succ, one_ascFactorial k, Nat.add_comm, factorial_succ]

Proof state:
k : ℕ
⊢ ascFactorial 1 (k + 1) = (k + 1)!

Tactic:
rw [ascFactorial_succ, one_ascFactorial k, Nat.add_comm, factorial_succ]

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem isTopologicalBasis_of_isOpen_of_nhds {s : Set (Set α)} (h_open : ∀ u ∈ s, IsOpen u)
    (h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u) :
    IsTopologicalBasis s :=
  .of_hasBasis_nhds <| fun a ↦
    (nhds_basis_opens a).to_hasBasis' (by simpa [and_assoc] using h_nhds a)
      fun _ ⟨hts, hat⟩ ↦ (h_open _ hts).mem_nhds hat

Proof state:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ u ∈ s, IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u
a : α
⊢ ∀ (i : Set α), a ∈ i ∧ IsOpen i → ∃ i', (i' ∈ s ∧ a ∈ i') ∧ id i' ⊆ i

Tactic:
simpa [and_assoc] using h_nhds a

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.not_eq_of_eq_true {a : Bool} (h : a = true) : (!a) = false

Proof state:
a : Bool
h : a = true
⊢ (!a) = false

Tactic:
simp [h]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem values_discrete {q : ℚ} (hq : q ≠ 0) : ∃ z : ℤ, padicNorm p q = (p : ℚ) ^ (-z) :=
  ⟨padicValRat p q, by simp [padicNorm, hq]⟩

Proof state:
p : ℕ
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = ↑p ^ (-padicValRat p q)

Tactic:
simp [padicNorm, hq]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
/-- If `f` tends to infinity along a nontrivial filter,
`fun x ↦ f x / r` tends to negative infinity if and only if `r < 0`. -/
lemma tendsto_div_const_atBot_iff_neg [NeBot l] (h : Tendsto f l atTop) :
    Tendsto (fun x ↦ f x / r) l atBot ↔ r < 0

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto (fun x => f x / r) l atBot ↔ r < 0

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atBot_iff_neg h]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
lemma zeta_prod_apply (a b : α × β) : zeta 𝕜 a b = zeta 𝕜 a.1 b.1 * zeta 𝕜 a.2 b.2

Proof state:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α × β
⊢ (zeta 𝕜) a b = (zeta 𝕜) a.1 b.1 * (zeta 𝕜) a.2 b.2

Tactic:
simp [← ite_and, Prod.le_def, and_comm]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Multiset.lean
@[simp] lemma prod_map_neg (s : Multiset α) : (s.map Neg.neg).prod = (-1) ^ card s * s.prod :=
  Quotient.inductionOn s (by simp)

Proof state:
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : HasDistribNeg α
s : Multiset α
⊢ ∀ (a : List α), (map Neg.neg ⟦a⟧).prod = (-1) ^ card ⟦a⟧ * prod ⟦a⟧

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem reindex_reindex_symm {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) :
    (s.reindex e).reindex e.symm = s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
m n : ℕ
s : Simplex k P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).reindex e.symm = s

Tactic:
rw [← reindex_trans, Equiv.self_trans_symm, reindex_refl]

Result:
no goals
-- Mathlib/Computability/TMConfig.lean
theorem fix_eval (f) : (fix f).eval =
    PFun.fix fun v => (f.eval v).map fun v =>
      if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail

Proof state:
f : Code
⊢ f.fix.eval = PFun.fix fun v => Part.map (fun v => if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/ModelTheory/ElementaryMaps.lean
theorem map_formula (f : M ↪ₑ[L] N) {α : Type*} (φ : L.Formula α) (x : α → M) :
    φ.Realize (f ∘ x) ↔ φ.Realize x

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
α : Type u_5
φ : L.Formula α
x : α → M
⊢ φ.Realize (⇑f ∘ x) ↔ φ.Realize x

Tactic:
rw [Formula.Realize, Formula.Realize, ← f.map_boundedFormula, Unique.eq_default (f ∘ default)]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem norm_unit (u : (𝓞 K)ˣ) :
    mixedEmbedding.norm (mixedEmbedding K u) = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
⊢ mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) = 1

Tactic:
rw [norm_eq_norm, Units.norm, Rat.cast_one]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive (attr := simp) zsmul_neg']
lemma inv_zpow' (a : α) (n : ℤ) : a⁻¹ ^ n = a ^ (-n)

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ a⁻¹ ^ n = a ^ (-n)

Tactic:
rw [inv_zpow, zpow_neg]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_eq_of_eq_mul_inv (h : a = c * b⁻¹) : a * b = c

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : a = c * b⁻¹
⊢ a * b = c

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_cons_eq_false [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} :
    (containsKey a (⟨k, v⟩ :: l) = false) ↔ ((k == a) = false) ∧ (containsKey a l = false)

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ containsKey a (⟨k, v⟩ :: l) = false ↔ (k == a) = false ∧ containsKey a l = false

Tactic:
simp [containsKey_cons, not_or]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
@[reassoc]
lemma SpecMap_awayMap_awayι :
    Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm =
      awayι 𝒜 x (hx ▸ SetLike.mul_mem_graded f_deg g_deg) (hm.trans_le (m.le_add_right m'))

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm = awayι 𝒜 x ⋯ ⋯

Tactic:
rw [awayι, awayι, Iso.eq_inv_comp, basicOpenIsoSpec_hom, basicOpenToSpec_SpecMap_awayMap_assoc,
← basicOpenIsoSpec_hom _ _ f_deg hm, Iso.hom_inv_id_assoc, Scheme.homOfLE_ι]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Trace.lean
theorem trace_one : trace (1 : Matrix n n R) = Fintype.card n

Proof state:
n : Type u_3
R : Type u_6
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : AddCommMonoidWithOne R
⊢ trace 1 = ↑(Fintype.card n)

Tactic:
simp_rw [trace, diag_one, Pi.one_def, Finset.sum_const, nsmul_one, Finset.card_univ]

Result:
no goals
-- Mathlib/Data/Sign.lean
/-- Casting out of `SignType` respects composition with suitable bundled homomorphism types. -/
lemma map_cast {α β F : Type*} [AddGroupWithOne α] [One β] [SubtractionMonoid β]
    [FunLike F α β] [AddMonoidHomClass F α β] [OneHomClass F α β] (f : F) (s : SignType) :
    f s = s

Proof state:
α : Type u_2
β : Type u_3
F : Type u_4
inst✝⁵ : AddGroupWithOne α
inst✝⁴ : One β
inst✝³ : SubtractionMonoid β
inst✝² : FunLike F α β
inst✝¹ : AddMonoidHomClass F α β
inst✝ : OneHomClass F α β
f : F
s : SignType
⊢ f ↑s = ↑s

Tactic:
apply map_cast' <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem takeWhile_replicate (p : α → Bool) :
    (replicate n a).takeWhile p = if p a then replicate n a else []

Proof state:
α : Type u_1
n : Nat
a : α
p : α → Bool
⊢ takeWhile p (replicate n a) = if p a = true then replicate n a else []

Tactic:
rw [takeWhile_replicate_eq_filter, filter_replicate]

Result:
no goals
-- Mathlib/Topology/Algebra/GroupWithZero.lean
theorem nhds_translation_mul_inv₀ (ha : a ≠ 0) : comap (· * a⁻¹) (𝓝 1) = 𝓝 a :=
  ((Homeomorph.mulRight₀ a ha).symm.comap_nhds_eq 1).trans <| by simp

Proof state:
G₀ : Type u_3
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ 𝓝 ((Homeomorph.mulRight₀ a ha).symm.symm 1) = 𝓝 a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.ofNatLt_reduce (n : Nat) (h) : BitVec.ofNatLt n h = BitVec.ofNat w n

Proof state:
w n : Nat
h : n < 2 ^ w
⊢ n#'h = BitVec.ofNat w n

Tactic:
simp [BitVec.ofNatLt, BitVec.ofNat, Fin.ofNat', Nat.mod_eq_of_lt h]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
theorem measurable_of_isOpen {f : δ → γ} (hf : ∀ s, IsOpen s → MeasurableSet (f ⁻¹' s)) :
    Measurable f

Proof state:
γ : Type u_3
δ : Type u_5
inst✝³ : TopologicalSpace γ
inst✝² : MeasurableSpace γ
inst✝¹ : BorelSpace γ
inst✝ : MeasurableSpace δ
f : δ → γ
hf : ∀ (s : Set γ), IsOpen s → MeasurableSet (f ⁻¹' s)
⊢ Measurable f

Tactic:
exact measurable_generateFrom hf

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem image2_eq_seq (f : α → β → γ) (s : Set α) (t : Set β) : image2 f s t = seq (f '' s) t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = (f '' s).seq t

Tactic:
rw [seq_eq_image2, image2_image_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem beq_nil_iff [BEq α] {l : List α} : (l == []) = l.isEmpty

Proof state:
α : Type u_1
inst✝ : BEq α
l : List α
⊢ (l == []) = l.isEmpty

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma uIcc_self : [[a, a]] = {a}

Proof state:
α : Type u_1
inst✝ : Lattice α
a : α
⊢ [[a, a]] = {a}

Tactic:
simp [uIcc]

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

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

Tactic:
simp [w, foldl_eq_foldlM, foldr_eq_foldrM]

Result:
no goals
-- Mathlib/Algebra/Group/Int/Even.lean
lemma not_even_iff : ¬Even n ↔ n % 2 = 1

Proof state:
n : ℤ
⊢ ¬Even n ↔ n % 2 = 1

Tactic:
rw [even_iff, emod_two_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem unzip_zipIdx_eq_prod (l : Array α) {n : Nat} :
    (l.zipIdx n).unzip = (l, range' n l.size)

Proof state:
α : Type u_1
l : Array α
n : Nat
⊢ (l.zipIdx n).unzip = (l, range' n l.size)

Tactic:
simp only [zipIdx_eq_zip_range', unzip_zip, size_range']

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_neg_of_ne_zero {n : ℕ} [nz : NeZero n] (a : ZMod n) [na : NeZero a] :
    (- a).val = n - a.val

Proof state:
n : ℕ
nz : NeZero n
a : ZMod n
na : NeZero a
⊢ (-a).val = n - a.val

Tactic:
simp_all [neg_val a, na.out]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_mul_comm (M N : Matrix m m R) : det (M * N) = det (N * M)

Proof state:
m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M N : Matrix m m R
⊢ (M * N).det = (N * M).det

Tactic:
rw [det_mul, det_mul, mul_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma nnrpow_nnrpow_inv (a : A) {x : ℝ≥0} (hx : x ≠ 0) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
hx : x ≠ 0
ha : autoParam (0 ≤ a) _auto✝
⊢ (a ^ x) ^ x⁻¹ = a

Tactic:
simp [mul_inv_cancel₀ hx, nnrpow_one _ ha]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem conj_neg_I : conj (-I) = (I : K)

Proof state:
K : Type u_1
inst✝ : RCLike K
⊢ (starRingEnd K) (-I) = I

Tactic:
rw [map_neg, conj_I, neg_neg]

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem option_some_iff {f : α →. σ} : (Partrec fun a => (f a).map Option.some) ↔ Partrec f :=
  ⟨fun h => (Nat.Partrec.ppred.comp h).of_eq fun n => by simp [Part.bind_assoc, bind_some_eq_map],
    fun hf => hf.map (option_some.comp snd).to₂⟩

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ
h : Partrec fun a => Part.map Option.some (f a)
n : ℕ
⊢ (do
      let n ← (↑(decode n)).bind fun a => Part.map encode ((fun a => Part.map Option.some (f a)) a)
      ↑n.ppred) =
    (↑(decode n)).bind fun a => Part.map encode (f a)

Tactic:
simp [Part.bind_assoc, bind_some_eq_map]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem card_opow_omega0 {a : Ordinal} (h : 1 < a) : card (a ^ ω) = max ℵ₀ a.card

Proof state:
a : Ordinal.{u_1}
h : 1 < a
⊢ (a ^ ω).card = ℵ₀ ⊔ a.card

Tactic:
rw [card_opow_eq_of_omega0_le_right h le_rfl, card_omega0, max_comm]

Result:
no goals