harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_erase [LawfulBEq α] (h : m.WF) {k a : α} :
    (m.erase k).get? a = if k == a then none else m.get? a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k a : α
⊢ (m.erase k).get? a = if (k == a) = true then none else m.get? a

Tactic:
simp_to_raw using Raw₀.get?_erase

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Ultra.lean
@[to_additive]
lemma nnnorm_tprod_le (f : ι → M) : ‖∏' i, f i‖₊ ≤ ⨆ i, ‖f i‖₊

Proof state:
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
⊢ ‖∏' (i : ι), f i‖₊ ≤ ⨆ i, ‖f i‖₊

Tactic:
simpa only [← NNReal.coe_le_coe, coe_nnnorm', coe_iSup] using norm_tprod_le f

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

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
a : α
⊢ m.isEmpty = true → m.getKey! a = default

Tactic:
simp_to_raw using Raw₀.getKey!_of_isEmpty ⟨m, _⟩

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem smul_sup : I • (N ⊔ P) = I • N ⊔ I • P :=
  toAddSubmonoid_injective <| by
    simp only [smul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.addSubmonoid_smul_sup]

Proof state:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
I : Submodule R A
N P : Submodule R M
⊢ (I • (N ⊔ P)).toAddSubmonoid = (I • N ⊔ I • P).toAddSubmonoid

Tactic:
simp only [smul_toAddSubmonoid, sup_toAddSubmonoid, AddSubmonoid.addSubmonoid_smul_sup]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem prod_eq_biUnion_right : s ×ˢ t = ⋃ b ∈ t, (fun a => (a, b)) '' s

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = ⋃ b ∈ t, (fun a => (a, b)) '' s

Tactic:
rw [iUnion_image_right, image2_mk_eq_prod]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem univ_pi_Ico_ae_eq_Icc {f g : ∀ i, α i} :
    (pi univ fun i => Ico (f i) (g i)) =ᵐ[Measure.pi μ] Icc f g

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i => Ico (f i) (g i)) =ᶠ[ae (Measure.pi μ)] Icc f g

Tactic:
rw [← pi_univ_Icc]

Result:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i => Ico (f i) (g i)) =ᶠ[ae (Measure.pi μ)] univ.pi fun i => Icc (f i) (g i)

Proof state:
ι : Type u_1
α : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : ∀ (i : ι), NoAtoms (μ i)
f g : (i : ι) → α i
⊢ (univ.pi fun i => Ico (f i) (g i)) =ᶠ[ae (Measure.pi μ)] univ.pi fun i => Icc (f i) (g i)

Tactic:
exact pi_Ico_ae_eq_pi_Icc

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_one : content (1 : R[X]) = 1

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
⊢ content 1 = 1

Tactic:
rw [← C_1, content_C, normalize_one]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem isLeftInversion_mul_right_iff {w : W} :
    cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t

Tactic:
rw [← isRightInversion_inv_iff, ← isRightInversion_inv_iff, mul_inv_rev, ht.inv,
  ht.isRightInversion_mul_left_iff]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma div_le_div_right (h : a ≤ b) : a / c ≤ b / c :=
  (c.eq_zero_or_pos.elim fun hc ↦ by simp [hc]) fun hc ↦
    (le_div_iff_mul_le hc).2 <| Nat.le_trans (Nat.div_mul_le_self _ _) h

Proof state:
a b c : ℕ
h : a ≤ b
hc : c = 0
⊢ a / c ≤ b / c

Tactic:
simp [hc]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem map_nhdsWithin_preimage_eq {x} (hx : x ∈ e.source) (s : Set Y) :
    map e (𝓝[e ⁻¹' s] x) = 𝓝[s] e x

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
x : X
hx : x ∈ e.source
s : Set Y
⊢ map (↑e) (𝓝[↑e ⁻¹' s] x) = 𝓝[s] ↑e x

Tactic:
rw [e.map_nhdsWithin_eq hx, e.image_source_inter_eq', e.target_inter_inv_preimage_preimage,
  e.nhdsWithin_target_inter (e.map_source hx)]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lt_div {a b c : Ordinal} (h : c ≠ 0) : a < b / c ↔ c * succ a ≤ b

Proof state:
a b c : Ordinal.{u_4}
h : c ≠ 0
⊢ a < b / c ↔ c * succ a ≤ b

Tactic:
rw [← not_le, div_le h, not_lt]

Result:
no goals
-- Mathlib/RingTheory/Localization/NumDen.lean
theorem isUnit_den_zero : IsUnit (den A (0 : K) : A)

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsUnit ↑(den A 0)

Tactic:
simp [isUnit_den_iff, IsLocalization.isInteger_zero]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem xor_comm (a b : Prop) : Xor' a b = Xor' b a

Proof state:
a b : Prop
⊢ Xor' a b = Xor' b a

Tactic:
simp [Xor', and_comm, or_comm]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma fromOpcycles_d :
    K.fromOpcycles i j ≫ K.d j k = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
inst✝ : K.HasHomology i
⊢ K.fromOpcycles i j ≫ K.d j k = 0

Tactic:
simp only [← cancel_epi (K.pOpcycles i), p_fromOpcycles_assoc, d_comp_d, comp_zero]

Result:
no goals
-- Mathlib/RingTheory/Flat/EquationalCriterion.lean
theorem isTrivialRelation_of_sum_smul_eq_zero [Flat R M] {ι : Type*} [Fintype ι] {f : ι → R}
    {x : ι → M} (h : ∑ i, f i • x i = 0) : IsTrivialRelation f x :=
  (Fintype.equivFin ι).symm.isTrivialRelation_comp.mp <| iff_forall_isTrivialRelation.mp ‹_› <| by
    simpa only [← (Fintype.equivFin ι).symm.sum_comp] using h

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Flat R M
ι : Type u_3
inst✝ : Fintype ι
f : ι → R
x : ι → M
h : ∑ i : ι, f i • x i = 0
⊢ ∑ i : Fin (Fintype.card ι), (f ∘ ⇑(Fintype.equivFin ι).symm) i • (x ∘ ⇑(Fintype.equivFin ι).symm) i = 0

Tactic:
simpa only [← (Fintype.equivFin ι).symm.sum_comp] using h

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem commute_int_add (n : ℤ) : Function.Commute f (n + ·)

Proof state:
f : CircleDeg1Lift
n : ℤ
⊢ Function.Commute ⇑f fun x => ↑n + x

Tactic:
simpa only [add_comm _ (n : ℝ)] using f.commute_add_int n

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem dist_div_eq_dist_mul_left (a b c : E) : dist (a / b) c = dist a (c * b)

Proof state:
E : Type u_2
inst✝ : SeminormedGroup E
a b c : E
⊢ dist (a / b) c = dist a (c * b)

Tactic:
rw [← dist_mul_right _ _ b, div_mul_cancel]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddTorsor.lean
theorem dist_vadd_right (v : V) (x : P) : dist x (v +ᵥ x) = ‖v‖

Proof state:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
v : V
x : P
⊢ dist x (v +ᵥ x) = ‖v‖

Tactic:
rw [dist_comm, dist_vadd_left]

Result:
no goals
-- Mathlib/LinearAlgebra/Projection.lean
theorem ofIsCompl_add (h : IsCompl p q) {φ₁ φ₂ : p →ₗ[R] F} {ψ₁ ψ₂ : q →ₗ[R] F} :
    ofIsCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂ :=
  ofIsCompl_eq _ (by simp) (by simp)

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ₁ φ₂ : ↥p →ₗ[R] F
ψ₁ ψ₂ : ↥q →ₗ[R] F
⊢ ∀ (u : ↥q), (ψ₁ + ψ₂) u = (ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂) ↑u

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ₁ φ₂ : ↥p →ₗ[R] F
ψ₁ ψ₂ : ↥q →ₗ[R] F
⊢ ∀ (u : ↥p), (φ₁ + φ₂) u = (ofIsCompl h φ₁ ψ₁ + ofIsCompl h φ₂ ψ₂) ↑u

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
@[simp]
lemma DilationEquiv.smulTorsor_ratio {c : P} {k : 𝕜} (hk : k ≠ 0) {x y : E}
    (h : dist x y ≠ 0) : ratio (smulTorsor c hk) = ‖k‖₊ :=
  Eq.symm <| ratio_unique_of_dist_ne_zero h <| by simp [dist_eq_norm, ← smul_sub, norm_smul]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : BoundedSMul 𝕜 E
P : Type u_3
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
x y : E
h : dist x y ≠ 0
⊢ dist ((smulTorsor c hk) x) ((smulTorsor c hk) y) = ↑‖k‖₊ * dist x y

Tactic:
simp [dist_eq_norm, ← smul_sub, norm_smul]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/SumCoeff.lean
theorem LSeriesSummable_of_sum_norm_bigO_and_nonneg
    {f : ℕ → ℝ} (hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ (n : ℝ) ^ r)
    (hf : ∀ n, 0 ≤ f n) (hr : 0 ≤ r) (hs : r < s.re) :
    LSeriesSummable (fun n ↦ f n) s :=
  LSeriesSummable_of_sum_norm_bigO (by simpa [abs_of_nonneg (hf _)]) hr hs

Proof state:
r : ℝ
s : ℂ
f : ℕ → ℝ
hO : (fun n => ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n => ↑n ^ r
hf : ∀ (n : ℕ), 0 ≤ f n
hr : 0 ≤ r
hs : r < s.re
⊢ (fun n => ∑ k ∈ Icc 1 n, ‖↑(f k)‖) =O[atTop] fun n => ↑n ^ r

Tactic:
simpa [abs_of_nonneg (hf _)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem clauses_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
    (performRupCheck f rupHints).1.clauses = f.clauses

Proof state:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (f.performRupCheck rupHints).fst.clauses = f.clauses

Tactic:
simp only [performRupCheck]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem restrict_extend_range (f : α → β) (g : α → γ) (g' : β → γ) :
    (range f).restrict (extend f g g') = fun x => g x.coe_prop.choose

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f).restrict (extend f g g') = fun x => g (Exists.choose ⋯)

Tactic:
exact restrict_dite _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f).restrict (extend f g g') = fun x => g (Exists.choose ⋯)

Tactic:
classical
exact restrict_dite _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((_ : α) × β)} {a : α} {h'}
    (hl : DistinctKeys l) (h : Perm l l') :
    getValue a l h' = getValue a l' ((containsKey_of_perm h).symm.trans h')

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((_ : α) × β)
a : α
h' : containsKey a l = true
hl : DistinctKeys l
h : l.Perm l'
⊢ getValue a l h' = getValue a l' ⋯

Tactic:
rw [← Option.some_inj, ← getValue?_eq_some_getValue, ← getValue?_eq_some_getValue,
  getValue?_of_perm hl h]

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem bddAbove_preimage (e : α ≃o β) {s : Set β} : BddAbove (e ⁻¹' s) ↔ BddAbove s

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set β
⊢ BddAbove (⇑e ⁻¹' s) ↔ BddAbove s

Tactic:
rw [← e.bddAbove_image, e.image_preimage]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
@[to_additive]
lemma smul_graphOn_univ (x : α × β) (f : F) :
    x • univ.graphOn f = univ.graphOn fun a ↦ x.2 / f x.1 * f a

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Group α
inst✝² : CommGroup β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
x : α × β
f : F
⊢ x • graphOn (⇑f) univ = graphOn (fun a => x.2 / f x.1 * f a) univ

Tactic:
simp [smul_graphOn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_empty {a : α} {c} : (empty c : Raw α β).contains a = false

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
c : Nat
⊢ (empty c).contains a = false

Tactic:
simp_to_raw using Raw₀.contains_empty

Result:
no goals
-- Mathlib/Topology/Hom/Open.lean
theorem cancel_left {g : β →CO γ} {f₁ f₂ : α →CO β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β →CO γ
f₁ f₂ : α →CO β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem integralSum_add (f g : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) (π : TaggedPrepartition I) :
    integralSum (f + g) vol π = integralSum f vol π + integralSum g vol π

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
I : Box ι
f g : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π : TaggedPrepartition I
⊢ integralSum (f + g) vol π = integralSum f vol π + integralSum g vol π

Tactic:
simp only [integralSum, Pi.add_apply, (vol _).map_add, Finset.sum_add_distrib]

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

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
v : β
⊢ get (m.insert k v) k ⋯ = v

Tactic:
simp_to_model [insert] using List.getValue_insertEntry_self

Result:
no goals
-- Mathlib/Data/Fintype/BigOperators.lean
/-- This lemma is specifically designed to be used backwards, whence the specialisation to `Fin n`
as the indexing type doesn't matter in practice. The more general forward direction lemma here is
`Fintype.card_piFinset`. -/
lemma card_piFinset_const {α : Type*} (s : Finset α) (n : ℕ) :
    #(piFinset fun _ : Fin n ↦ s) = #s ^ n

Proof state:
α : Type u_7
s : Finset α
n : ℕ
⊢ #(piFinset fun x => s) = #s ^ n

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_le_size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)} :
    m.1.size ≤ (insertMany m l).1.1.size

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
⊢ m.val.size ≤ (insertMany m l).val.val.size

Tactic:
simp_to_model [Const.insertMany] using List.length_le_length_insertListConst

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem norm_conj (x : ℤ√d) : (star x).norm = x.norm :=
  -- Porting note: replaced `simp` with `rw`
  -- See https://github.com/leanprover-community/mathlib4/issues/5026
  (Int.cast_inj (α := ℤ√d)).1 <| by rw [norm_eq_mul_conj, star_star, mul_comm, norm_eq_mul_conj]

Proof state:
d : ℤ
x : ℤ√d
⊢ ↑(star x).norm = ↑x.norm

Tactic:
rw [norm_eq_mul_conj, star_star, mul_comm, norm_eq_mul_conj]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean
theorem C_two_mul_complex_cosh (n : ℤ) : (C ℂ n).eval (2 * cosh θ) = 2 * cosh (n * θ)

Proof state:
θ : ℂ
n : ℤ
⊢ eval (2 * cosh θ) (C ℂ n) = 2 * cosh (↑n * θ)

Tactic:
simp [C_eq_two_mul_T_comp_half_mul_X]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@[simp]
lemma map_dblZ (P : Fin 3 → R) : (W'.map f).toJacobian.dblZ (f ∘ P) = f (W'.dblZ P)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (map W' f).toJacobian.dblZ (⇑f ∘ P) = f (W'.dblZ P)

Tactic:
simp only [dblZ, negY]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (⇑f ∘ P) z *
      ((⇑f ∘ P) y -
        (-(⇑f ∘ P) y - (map W' f).toJacobian.a₁ * (⇑f ∘ P) x * (⇑f ∘ P) z -
          (map W' f).toJacobian.a₃ * (⇑f ∘ P) z ^ 3)) =
    f (P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)))

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (⇑f ∘ P) z *
      ((⇑f ∘ P) y -
        (-(⇑f ∘ P) y - (map W' f).toJacobian.a₁ * (⇑f ∘ P) x * (⇑f ∘ P) z -
          (map W' f).toJacobian.a₃ * (⇑f ∘ P) z ^ 3)) =
    f (P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)))

Tactic:
map_simp

Result:
no goals
-- Mathlib/Algebra/FreeMonoid/Basic.lean
theorem reverse_reverse {a : FreeMonoid α} : reverse (reverse a) = a

Proof state:
α : Type u_1
a : FreeMonoid α
⊢ a.reverse.reverse = a

Tactic:
apply List.reverse_reverse

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem adjoin_eq_bot_iff : adjoin F S = ⊥ ↔ S ⊆ (⊥ : IntermediateField F E)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set E
⊢ adjoin F S = ⊥ ↔ S ⊆ ↑⊥

Tactic:
rw [eq_bot_iff, adjoin_le_iff]

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- The `n`-smooth numbers agree with the `Finset.range n`-factored numbers. -/
lemma smoothNumbers_eq_factoredNumbers (n : ℕ) :
    smoothNumbers n = factoredNumbers (Finset.range n)

Proof state:
n : ℕ
⊢ n.smoothNumbers = factoredNumbers (Finset.range n)

Tactic:
simp only [smoothNumbers, ne_eq, mem_primeFactorsList', and_imp, factoredNumbers,
  Finset.mem_range]

Result:
no goals
-- Mathlib/Order/Filter/IndicatorFunction.lean
theorem mulIndicator_eventuallyEq (hf : f =ᶠ[l ⊓ 𝓟 s] g) (hs : s =ᶠ[l] t) :
    mulIndicator s f =ᶠ[l] mulIndicator t g :=
  (eventually_inf_principal.1 hf).mp <| hs.mem_iff.mono fun x hst hfg =>
    by_cases
      (fun hxs : x ∈ s => by simp only [*, hst.1 hxs, mulIndicator_of_mem])
      (fun hxs => by simp only [mulIndicator_of_not_mem, hxs, mt hst.2 hxs, not_false_eq_true])

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f g : α → M
l : Filter α
hf : f =ᶠ[l ⊓ 𝓟 s] g
hs : s =ᶠ[l] t
x : α
hst : x ∈ s ↔ x ∈ t
hfg : x ∈ s → f x = g x
hxs : x ∈ s
⊢ s.mulIndicator f x = t.mulIndicator g x

Tactic:
simp only [*, hst.1 hxs, mulIndicator_of_mem]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s t : Set α
f g : α → M
l : Filter α
hf : f =ᶠ[l ⊓ 𝓟 s] g
hs : s =ᶠ[l] t
x : α
hst : x ∈ s ↔ x ∈ t
hfg : x ∈ s → f x = g x
hxs : x ∉ s
⊢ s.mulIndicator f x = t.mulIndicator g x

Tactic:
simp only [mulIndicator_of_not_mem, hxs, mt hst.2 hxs, not_false_eq_true]

Result:
no goals
-- Mathlib/RingTheory/RingHom/FinitePresentation.lean
theorem finitePresentation_stableUnderComposition : StableUnderComposition @FinitePresentation

Proof state:
⊢ StableUnderComposition @FinitePresentation

Tactic:
introv R hf hg

Result:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FinitePresentation
hg : g.FinitePresentation
⊢ (g.comp f).FinitePresentation

Proof state:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FinitePresentation
hg : g.FinitePresentation
⊢ (g.comp f).FinitePresentation

Tactic:
exact hg.comp hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_pos_iff {w : Nat} {x : BitVec w} :
    0 ≤ BitVec.toInt x ↔ 2 * x.toNat < 2 ^ w

Proof state:
w : Nat
x : BitVec w
⊢ 0 ≤ x.toInt ↔ 2 * x.toNat < 2 ^ w

Tactic:
simp [toInt_eq_toNat_cond]

Result:
w : Nat
x : BitVec w
⊢ (0 ≤ if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)) ↔ 2 * x.toNat < 2 ^ w

Proof state:
w : Nat
x : BitVec w
⊢ (0 ≤ if 2 * x.toNat < 2 ^ w then ↑x.toNat else ↑x.toNat - ↑(2 ^ w)) ↔ 2 * x.toNat < 2 ^ w

Tactic:
omega

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem lsub_lt_ord {ι} {f : ι → Ordinal} {c : Ordinal} (hι : #ι < c.cof) :
    (∀ i, f i < c) → lsub.{u, u} f < c :=
  lsub_lt_ord_lift (by rwa [(#ι).lift_id])

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

Tactic:
rwa [(#ι).lift_id]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem index_iInf_le {ι : Type*} [Fintype ι] (f : ι → Subgroup G) :
    (⨅ i, f i).index ≤ ∏ i, (f i).index

Proof state:
G : Type u_1
inst✝¹ : Group G
ι : Type u_3
inst✝ : Fintype ι
f : ι → Subgroup G
⊢ (⨅ i, f i).index ≤ ∏ i : ι, (f i).index

Tactic:
simp_rw [← relindex_top_right, relindex_iInf_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_map (f : α → β) (as : Array α) (i : Nat) :
    (as.map f)[i]? = as[i]?.map f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
as : Array α
i : Nat
⊢ (map f as)[i]? = Option.map f as[i]?

Tactic:
simp [getElem?_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/ByCases.lean
theorem ite_some_none_eq_some [Decidable P] :
    (if P then some x else none) = some y ↔ P ∧ x = y

Proof state:
P : Prop
α✝ : Type u_1
x y : α✝
inst✝ : Decidable P
⊢ (if P then some x else none) = some y ↔ P ∧ x = y

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
theorem denote_mkFullAdderOut (assign : α → Bool) (aig : AIG α) (input : FullAdderInput aig) :
    ⟦mkFullAdderOut aig input, assign⟧
      =
    ((⟦aig, input.lhs, assign⟧ ^^ ⟦aig, input.rhs, assign⟧) ^^ ⟦aig, input.cin, assign⟧)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦assign, mkFullAdderOut aig input⟧ =
    (⟦assign, { aig := aig, ref := input.lhs }⟧ ^^ ⟦assign, { aig := aig, ref := input.rhs }⟧ ^^
      ⟦assign, { aig := aig, ref := input.cin }⟧)

Tactic:
simp only [mkFullAdderOut, Ref.cast_eq, denote_mkXorCached, denote_projected_entry, Bool.bne_assoc,
  Bool.bne_left_inj]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (⟦assign, { aig := aig, ref := input.lhs }⟧ !=
      (⟦assign, { aig := aig, ref := input.rhs }⟧ !=
        ⟦assign,
          { aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig,
            ref := { gate := input.cin.gate, hgate := ⋯ } }⟧)) =
    (⟦assign, { aig := aig, ref := input.lhs }⟧ !=
      (⟦assign, { aig := aig, ref := input.rhs }⟧ != ⟦assign, { aig := aig, ref := input.cin }⟧))

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ (⟦assign, { aig := aig, ref := input.lhs }⟧ !=
      (⟦assign, { aig := aig, ref := input.rhs }⟧ !=
        ⟦assign,
          { aig := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig,
            ref := { gate := input.cin.gate, hgate := ⋯ } }⟧)) =
    (⟦assign, { aig := aig, ref := input.lhs }⟧ !=
      (⟦assign, { aig := aig, ref := input.rhs }⟧ != ⟦assign, { aig := aig, ref := input.cin }⟧))

Tactic:
rw [LawfulOperator.denote_mem_prefix (f := mkXorCached)]

Result:
no goals