harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem map_zero {R : Type*} [CommMonoidWithZero R] [Nontrivial R] (χ : MulChar R R') :
    χ (0 : R) = 0

Proof state:
R' : Type u_2
inst✝² : CommMonoidWithZero R'
R : Type u_3
inst✝¹ : CommMonoidWithZero R
inst✝ : Nontrivial R
χ : MulChar R R'
⊢ χ 0 = 0

Tactic:
rw [map_nonunit χ not_isUnit_zero]

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_mapAccumr₂_right_left (f₁ : α → γ → σ₁ → σ₁ × φ) (f₂ : α → β → σ₂ → σ₂ × γ) :
    (mapAccumr₂ f₁ xs (mapAccumr₂ f₂ xs ys s₂).snd s₁)
    = let m := mapAccumr₂ (fun x y (s₁, s₂) =>
                let r₂ := f₂ x y s₂
                let r₁ := f₁ x r₂.snd s₁
                ((r₁.fst, r₂.fst), r₁.snd)
              )
            xs ys (s₁, s₂)
    (m.fst.fst, m.snd)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
φ : Type u_8
n : ℕ
s₁ : σ₁
s₂ : σ₂
xs : Vector α n
ys : Vector β n
f₁ : α → γ → σ₁ → σ₁ × φ
f₂ : α → β → σ₂ → σ₂ × γ
⊢ mapAccumr₂ f₁ xs (mapAccumr₂ f₂ xs ys s₂).2 s₁ =
    let m :=
      mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            let r₂ := f₂ x y s₂;
            let r₁ := f₁ x r₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_re_add_im {f : X → 𝕜} (hf : Integrable f μ) :
    ((∫ x, RCLike.re (f x) ∂μ : ℝ) : 𝕜) + (∫ x, RCLike.im (f x) ∂μ : ℝ) * RCLike.I =
      ∫ x, f x ∂μ

Proof state:
X : Type u_1
inst✝¹ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝ : RCLike 𝕜
f : X → 𝕜
hf : Integrable f μ
⊢ ↑(∫ (x : X), re (f x) ∂μ) + ↑(∫ (x : X), im (f x) ∂μ) * I = ∫ (x : X), f x ∂μ

Tactic:
rw [← integral_ofReal, ← integral_ofReal, integral_coe_re_add_coe_im hf]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem mk'_d_1_0 : (mk' X₀ X₁ d₀ succ').d 0 1 = d₀

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₀ ⟶ X₁
succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0
⊢ (if 1 = 0 + 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀

Tactic:
rw [if_pos rfl, Category.comp_id]

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₀ ⟶ X₁
succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0
⊢ (mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').d 0 1 = d₀

Tactic:
change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ : V
d₀ : X₀ ⟶ X₁
succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0
⊢ (if 1 = 0 + 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
-- Mathlib/Order/ModularLattice.lean
theorem inf_sup_assoc_of_le {x : α} (y : α) {z : α} (h : z ≤ x) : x ⊓ y ⊔ z = x ⊓ (y ⊔ z)

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z : α
h : z ≤ x
⊢ x ⊓ y ⊔ z = x ⊓ (y ⊔ z)

Tactic:
rw [inf_comm, sup_comm, ← sup_inf_assoc_of_le y h, inf_comm, sup_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem lineMap_eq_lineMap_iff [NoZeroSMulDivisors k V1] {p₀ p₁ : P1} {c₁ c₂ : k} :
    lineMap p₀ p₁ c₁ = lineMap p₀ p₁ c₂ ↔ p₀ = p₁ ∨ c₁ = c₂

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V1
inst✝² : Module k V1
inst✝¹ : AffineSpace V1 P1
inst✝ : NoZeroSMulDivisors k V1
p₀ p₁ : P1
c₁ c₂ : k
⊢ (lineMap p₀ p₁) c₁ = (lineMap p₀ p₁) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂

Tactic:
rw [lineMap_apply, lineMap_apply, ← @vsub_eq_zero_iff_eq V1, vadd_vsub_vadd_cancel_right, ←
  sub_smul, smul_eq_zero, sub_eq_zero, vsub_eq_zero_iff_eq, or_comm, eq_comm]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean
theorem withDensityᵥ_sub (hf : Integrable f μ) (hg : Integrable g μ) :
    μ.withDensityᵥ (f - g) = μ.withDensityᵥ f - μ.withDensityᵥ g

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
⊢ μ.withDensityᵥ (f - g) = μ.withDensityᵥ f - μ.withDensityᵥ g

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, withDensityᵥ_add hf hg.neg, withDensityᵥ_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem tensor_whiskerLeft (X Y : C) {Z Z' : C} (f : Z ⟶ Z') :
    (X ⊗ Y) ◁ f = (α_ X Y Z).hom ≫ X ◁ Y ◁ f ≫ (α_ X Y Z').inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ (X ⊗ Y) ◁ f = (α_ X Y Z).hom ≫ X ◁ Y ◁ f ≫ (α_ X Y Z').inv

Tactic:
simp only [← id_tensorHom, ← tensorHom_id]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ 𝟙 (X ⊗ Y) ⊗ f = (α_ X Y Z).hom ≫ (𝟙 X ⊗ 𝟙 Y ⊗ f) ≫ (α_ X Y Z').inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ 𝟙 (X ⊗ Y) ⊗ f = (α_ X Y Z).hom ≫ (𝟙 X ⊗ 𝟙 Y ⊗ f) ≫ (α_ X Y Z').inv

Tactic:
rw [← assoc, ← associator_naturality]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ 𝟙 (X ⊗ Y) ⊗ f = (((𝟙 X ⊗ 𝟙 Y) ⊗ f) ≫ (α_ X Y Z').hom) ≫ (α_ X Y Z').inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ 𝟙 (X ⊗ Y) ⊗ f = (((𝟙 X ⊗ 𝟙 Y) ⊗ f) ≫ (α_ X Y Z').hom) ≫ (α_ X Y Z').inv

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/QExpansion.lean
theorem exp_decay_atImInfty [NeZero n] [CuspFormClass F Γ(n) k] :
    f =O[atImInfty] fun τ ↦ Real.exp (-2 * π * τ.im / n)

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : CuspFormClass F Γ(n) k
⊢ ⇑f =O[atImInfty] fun τ => rexp (-2 * π * τ.im / ↑n)

Tactic:
simpa only [neg_mul, comp_def, ofComplex_apply, coe_im] using
  ((periodic_comp_ofComplex n f).exp_decay_of_zero_at_inf
    (mod_cast (Nat.pos_iff_ne_zero.mpr (NeZero.ne _)))
    (eventually_of_mem (preimage_mem_comap (Ioi_mem_atTop 0))
      fun _ ↦ differentiableAt_comp_ofComplex f)
    (zero_at_infty_comp_ofComplex f)).comp_tendsto tendsto_coe_atImInfty

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean
private lemma hasSmallLocalizedShiftedHom_K_S'_X₁ :
    HasSmallLocalizedShiftedHom.{w} W ℤ K (S').X₁

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ HasSmallLocalizedShiftedHom W ℤ (CochainComplex.mappingCone (S.map (CochainComplex.singleFunctor C 0)).f)
    (S.map (CochainComplex.singleFunctor C 0)).X₁

Tactic:
rw [Localization.hasSmallLocalizedShiftedHom_iff_source.{w} W ℤ qis hqis (S').X₁]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ HasSmallLocalizedShiftedHom W ℤ (S.map (CochainComplex.singleFunctor C 0)).X₃
    (S.map (CochainComplex.singleFunctor C 0)).X₁

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ HasSmallLocalizedShiftedHom W ℤ (S.map (CochainComplex.singleFunctor C 0)).X₃
    (S.map (CochainComplex.singleFunctor C 0)).X₁

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Finset/Piecewise.lean
lemma piecewise_insert_self [DecidableEq ι] {j : ι} [∀ i, Decidable (i ∈ insert j s)] :
    (insert j s).piecewise f g j = f j

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g j = f j

Tactic:
simp [piecewise]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem leftUnitor_naturality {f g : a ⟶ b} (η : f ⟶ g) :
    𝟙 a ◁ η ≫ (λ_ g).hom = (λ_ f).hom ≫ η

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ⟶ g
⊢ 𝟙 a ◁ η ≫ (λ_ g).hom = (λ_ f).hom ≫ η

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addY_neg {P : Fin 3 → R} (hP : W'.Equation P) : W'.addY P (W'.neg P) = -W'.dblZ P ^ 3

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addY P (W'.neg P) = -W'.dblZ P ^ 3

Tactic:
rw [addY, addX_neg hP, negAddY_neg hP, addZ_neg, negY_of_Z_eq_zero rfl, Matrix.cons_val_one,
  Matrix.head_cons]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
@[simp]
lemma sqrt_one : sqrt (1 : A) = 1

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Algebra ℝ A
inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
⊢ sqrt 1 = 1

Tactic:
simp [sqrt_eq_cfc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem if_true_left  (p : Prop) [h : Decidable p] (f : Bool) :
    (ite p true f) = (p || f)

Proof state:
case isTrue
p✝ : Prop
f : Bool
p : p✝
⊢ (if p✝ then true else f) = (decide p✝ || f)

Tactic:
simp [p]

Result:
no goals

Proof state:
p : Prop
h : Decidable p
f : Bool
⊢ (if p then true else f) = (decide p || f)

Tactic:
cases h with | _ p => simp [p]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_insert_self [LawfulBEq α] (h : m.WF) {k : α} {v : β k} :
    (m.insert k v).get k (mem_insert_self h) = v

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k : α
v : β k
⊢ (m.insert k v).get k ⋯ = v

Tactic:
simp_to_raw using Raw₀.get_insert_self ⟨m, _⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_eq_arcsin {x : ℝ} (h : 0 ≤ x) : arccos x = arcsin (√(1 - x ^ 2)) :=
  (arcsin_eq_of_sin_eq (sin_arccos _)
      ⟨(Left.neg_nonpos_iff.2 (div_nonneg pi_pos.le (by norm_num))).trans (arccos_nonneg _),
        arccos_le_pi_div_two.2 h⟩).symm

Proof state:
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem findSomeM?_toList [Monad m] [LawfulMonad m] (p : α → m (Option β)) (as : Array α) :
    as.toList.findSomeM? p = as.findSomeM? p

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m (Option β)
as : Array α
⊢ List.findSomeM? p as.toList = findSomeM? p as

Tactic:
cases as

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m (Option β)
toList✝ : List α
⊢ List.findSomeM? p { toList := toList✝ }.toList = findSomeM? p { toList := toList✝ }

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → m (Option β)
toList✝ : List α
⊢ List.findSomeM? p { toList := toList✝ }.toList = findSomeM? p { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_alter [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β}
    (h : Raw.WFImp m.1) {a : α} {f : Option (β a) → Option (β a)} : Raw.WFImp (m.alter a f).1

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
⊢ Raw.WFImp (m.alterₘ a f).val

Tactic:
exact wfImp_alterₘ h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
⊢ Raw.WFImp (m.alter a f).val

Tactic:
rw [alter_eq_alterₘ]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
⊢ Raw.WFImp (m.alterₘ a f).val
-- Mathlib/Data/Stream/Init.lean
theorem get_succ_iterate (n : ℕ) (f : α → α) (a : α) :
    get (iterate f a) (succ n) = get (iterate f (f a)) n

Proof state:
α : Type u
n : ℕ
f : α → α
a : α
⊢ (iterate f a).get n.succ = (iterate f (f a)).get n

Tactic:
rw [get_succ, tail_iterate]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma IsMeasurableRatCDF.stieltjesFunctionAux_unit_prod {f : α → ℚ → ℝ} (a : α) :
    IsMeasurableRatCDF.stieltjesFunctionAux (fun (p : Unit × α) ↦ f p.2) ((), a)
      = IsMeasurableRatCDF.stieltjesFunctionAux f a

Proof state:
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ stieltjesFunctionAux (fun p => f p.2) ((), a) = stieltjesFunctionAux f a

Tactic:
simp_rw [IsMeasurableRatCDF.stieltjesFunctionAux_def']

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
lemma IsMulFreimanIso.congr (hf₁ : IsMulFreimanIso n A B f₁) (h : EqOn f₁ f₂ A) :
    IsMulFreimanIso n A B f₂ where
  bijOn := hf₁.bijOn.congr h
  map_prod_eq_map_prod s t hsA htA hs ht

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanIso n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
⊢ (map f₂ s).prod = (map f₂ t).prod ↔ s.prod = t.prod

Tactic:
rw [map_congr rfl fun x hx => h.symm (hsA hx), map_congr rfl fun x hx => h.symm (htA hx),
  hf₁.map_prod_eq_map_prod hsA htA hs ht]

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra.lean
theorem quot_mk_eq_ι (m : X) : Quot.mk (FreeAlgebra.Rel R X) m = ι R m

Proof state:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
m : X
⊢ Quot.mk (Rel R X) (Pre.of m) = ι R m

Tactic:
rw [ι_def]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_C_ne_zero (h : n ≠ 0) : (C a).coeff n = 0

Proof state:
R : Type u
a : R
n : ℕ
inst✝ : Semiring R
h : n ≠ 0
⊢ (C a).coeff n = 0

Tactic:
rw [coeff_C, if_neg h]

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
theorem liftAux_apply_I (I' : A) (hI') : liftAux I' hI' I = I'

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hI' : I' * I' = -1
⊢ (liftAux I' hI') I = I'

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSub_apply_const (w : ι → k) (p : P) (h : ∑ i ∈ s, w i = 0) :
    s.weightedVSub (fun _ => p) w = 0

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : P
h : ∑ i ∈ s, w i = 0
⊢ (s.weightedVSub fun x => p) w = 0

Tactic:
rw [weightedVSub, weightedVSubOfPoint_apply_const, h, zero_smul]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem basisFun_apply [DecidableEq ι] (i) :
    basisFun p 𝕜 ι i = (WithLp.equiv p _).symm (Pi.single i 1)

Proof state:
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝² : Finite ι
inst✝¹ : Ring 𝕜
inst✝ : DecidableEq ι
i : ι
⊢ (basisFun p 𝕜 ι) i = (WithLp.equiv p (ι → 𝕜)).symm (Pi.single i 1)

Tactic:
simp_rw [basisFun, Basis.coe_ofEquivFun, WithLp.linearEquiv_symm_apply]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.div [Add α] [Div β] (hf : Periodic f c) (hg : Periodic g c) :
    Periodic (f / g) c

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
c : α
inst✝¹ : Add α
inst✝ : Div β
hf : Periodic f c
hg : Periodic g c
⊢ Periodic (f / g) c

Tactic:
simp_all

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem card_eq_zero {o} : card o = 0 ↔ o = 0

Proof state:
o : Ordinal.{u_1}
⊢ o.card = 0 ↔ o = 0

Tactic:
simpa using card_eq_nat (n := 0)

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Lemmas.lean
lemma parallelComp_comm {η : Kernel γ δ} [IsSFiniteKernel η] :
    (Kernel.id ∥ₖ κ) ∘ₖ (η ∥ₖ Kernel.id) = (η ∥ₖ Kernel.id) ∘ₖ (Kernel.id ∥ₖ κ)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel γ δ
inst✝ : IsSFiniteKernel η
⊢ Kernel.id ∥ₖ κ ∘ₖ (η ∥ₖ Kernel.id) = η ∥ₖ Kernel.id ∘ₖ (Kernel.id ∥ₖ κ)

Tactic:
rw [parallelComp_id_left_comp_parallelComp, parallelComp_id_right_comp_parallelComp,
  comp_id, comp_id]

Result:
no goals
-- Mathlib/Algebra/Ring/Divisibility/Lemmas.lean
lemma add_pow_dvd_pow_of_pow_eq_zero_right (hp : n + m ≤ p + 1) (h_comm : Commute x y)
    (hx : x ^ n = 0) : (x + y) ^ m ∣ y ^ p :=
  (h_comm.add_left rfl).pow_dvd_pow_of_sub_pow_eq_zero hp (by simpa)

Proof state:
R : Type u_1
x y : R
n m p : ℕ
inst✝ : Ring R
hp : n + m ≤ p + 1
h_comm : Commute x y
hx : x ^ n = 0
⊢ (x + y - y) ^ n = 0

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem image_prod_mk_subset_prod {f : α → β} {g : α → γ} {s : Set α} :
    (fun x => (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
s : Set α
⊢ (fun x => (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s)

Tactic:
rintro _ ⟨x, hx, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
s : Set α
x : α
hx : x ∈ s
⊢ (fun x => (f x, g x)) x ∈ (f '' s) ×ˢ (g '' s)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
s : Set α
x : α
hx : x ∈ s
⊢ (fun x => (f x, g x)) x ∈ (f '' s) ×ˢ (g '' s)

Tactic:
exact mk_mem_prod (mem_image_of_mem f hx) (mem_image_of_mem g hx)

Result:
no goals
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
theorem transReflReparamAux_one : transReflReparamAux 1 = 1

Proof state:
⊢ transReflReparamAux 1 = 1

Tactic:
norm_num [transReflReparamAux]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_replace_of_ne [LawfulBEq α] {l : List α} {i : Nat} (h : l[i]? ≠ some a) :
    (l.replace a b)[i]? = l[i]?

Proof state:
α : Type u_1
inst✝¹ : BEq α
a b : α
inst✝ : LawfulBEq α
l : List α
i : Nat
h : l[i]? ≠ some a
⊢ (l.replace a b)[i]? = l[i]?

Tactic:
simp_all [getElem?_replace]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean
theorem IsBoundedBilinearMap.fderivWithin (h : IsBoundedBilinearMap 𝕜 b) (p : E × F)
    (hxs : UniqueDiffWithinAt 𝕜 u p) : fderivWithin 𝕜 b u p = h.deriv p

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
hxs : UniqueDiffWithinAt 𝕜 u p
⊢ fderivWithin 𝕜 b u p = h.deriv p

Tactic:
rw [DifferentiableAt.fderivWithin (h.differentiableAt p) hxs]

Result:
𝕜 : 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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
hxs : UniqueDiffWithinAt 𝕜 u p
⊢ fderiv 𝕜 b p = h.deriv p

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
hxs : UniqueDiffWithinAt 𝕜 u p
⊢ fderiv 𝕜 b p = h.deriv p

Tactic:
exact h.fderiv p

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
@[simp] lemma upperBounds_closure (s : Set α) : upperBounds (closure s : Set α) = upperBounds s :=
  ext fun a ↦ by simp_rw [mem_upperBounds_iff_subset_Iic, isClosed_Iic.closure_subset_iff]

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
s : Set α
a : α
⊢ a ∈ upperBounds (closure s) ↔ a ∈ upperBounds s

Tactic:
simp_rw [mem_upperBounds_iff_subset_Iic, isClosed_Iic.closure_subset_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
@[simp] lemma disjoint_edgeSet : Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂

Proof state:
V : Type u
G₁ G₂ : SimpleGraph V
⊢ Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂

Tactic:
rw [Set.disjoint_iff, disjoint_iff_inf_le, ← edgeSet_inf, ← edgeSet_bot, ← Set.le_iff_subset,
  OrderEmbedding.le_iff_le]

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
lemma isPrimePow_card : IsPrimePow (Fintype.card K)

Proof state:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p : ℕ
n : ℕ+
hp : Nat.Prime p
hn : q = p ^ ↑n
⊢ IsPrimePow q

Tactic:
exact ⟨p, n, Nat.prime_iff.mp hp, n.prop, hn.symm⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
⊢ IsPrimePow q

Tactic:
obtain ⟨p, n, hp, hn⟩ := card' K

Result:
case intro.intro.intro
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p : ℕ
n : ℕ+
hp : Nat.Prime p
hn : q = p ^ ↑n
⊢ IsPrimePow q
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_insert_eq_range_union_iUnion {ι : Type*} (x : ι → β) (t : ι → Set β) :
    ⋃ i, insert (x i) (t i) = range x ∪ ⋃ i, t i

Proof state:
β : Type u_2
ι : Type u_12
x : ι → β
t : ι → Set β
⊢ ⋃ i, insert (x i) (t i) = range x ∪ ⋃ i, t i

Tactic:
simp_rw [← union_singleton, iUnion_union_distrib, union_comm, iUnion_singleton_eq_range]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
/-- The composition product of a measure and a constant kernel is the product between the two
measures. -/
@[simp]
lemma compProd_const {ν : Measure β} [SFinite μ] [SFinite ν] :
    μ ⊗ₘ (Kernel.const α ν) = μ.prod ν

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite μ
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ ⊗ₘ Kernel.const α ν) s = (μ.prod ν) s

Tactic:
simp_rw [compProd_apply hs, prod_apply hs, Kernel.const_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite μ
inst✝ : SFinite ν
⊢ μ ⊗ₘ Kernel.const α ν = μ.prod ν

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite μ
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ ⊗ₘ Kernel.const α ν) s = (μ.prod ν) s
-- Mathlib/Analysis/Convex/Join.lean
theorem mem_convexJoin : x ∈ convexJoin 𝕜 s t ↔ ∃ a ∈ s, ∃ b ∈ t, x ∈ segment 𝕜 a b

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t : Set E
x : E
⊢ x ∈ convexJoin 𝕜 s t ↔ ∃ a ∈ s, ∃ b ∈ t, x ∈ segment 𝕜 a b

Tactic:
simp [convexJoin]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem join_eq_none : o.join = none ↔ o = none ∨ o = some none :=
  match o with | none | some none | some (some _) => by simp

Proof state:
α✝ : Type u_1
o : Option (Option α✝)
val✝ : α✝
⊢ (some (some val✝)).join = none ↔ some (some val✝) = none ∨ some (some val✝) = some none

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/KummerPolynomial.lean
lemma root_X_pow_sub_C_pow (n : ℕ) (a : K) :
    (AdjoinRoot.root (X ^ n - C a)) ^ n = AdjoinRoot.of _ a

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
a : K
⊢ root (X ^ n - C a) ^ n = (of (X ^ n - C a)) a

Tactic:
rw [← sub_eq_zero, ← AdjoinRoot.eval₂_root, eval₂_sub, eval₂_C, eval₂_pow, eval₂_X]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem filter_cons_of_neg {a : α} (s) : ¬p a → filter p (a ::ₘ s) = filter p s :=
  Quot.inductionOn s fun _ h => congr_arg ofList <| List.filter_cons_of_neg <| by simpa using h

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
x✝ : List α
h : ¬p a
⊢ ¬decide (p a) = true

Tactic:
simpa using h

Result:
no goals