harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
lemma isIntegralCurve_comp_sub {dt : ℝ} :
    IsIntegralCurve γ v ↔ IsIntegralCurve (γ ∘ (· - dt)) v

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
dt : ℝ
⊢ IsIntegralCurve γ v ↔ IsIntegralCurve (γ ∘ fun x => x - dt) v

Tactic:
simpa using isIntegralCurve_comp_add (dt := -dt)

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem haveLebesgueDecomposition_spec (μ ν : Measure α) [h : HaveLebesgueDecomposition μ ν] :
    Measurable (μ.rnDeriv ν) ∧
      μ.singularPart ν ⟂ₘ ν ∧ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ Measurable (μ.rnDeriv ν) ∧ μ.singularPart ν ⟂ₘ ν ∧ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
rw [singularPart, rnDeriv, dif_pos h, dif_pos h]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ Measurable (Classical.choose ⋯).2 ∧
    (Classical.choose ⋯).1 ⟂ₘ ν ∧ μ = (Classical.choose ⋯).1 + ν.withDensity (Classical.choose ⋯).2

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ Measurable (Classical.choose ⋯).2 ∧
    (Classical.choose ⋯).1 ⟂ₘ ν ∧ μ = (Classical.choose ⋯).1 + ν.withDensity (Classical.choose ⋯).2

Tactic:
exact Classical.choose_spec h.lebesgue_decomposition

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_mul_inv_cancel'_right (a b : G) : a * (b * a⁻¹) = b

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b : G
⊢ a * (b * a⁻¹) = b

Tactic:
rw [← div_eq_mul_inv, mul_div_cancel a b]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem single_multiset_sum [AddCommMonoid M] (s : Multiset M) (a : α) :
    single a s.sum = (s.map (single a)).sum :=
  Multiset.induction_on s (single_zero _) fun a s ih => by
    rw [Multiset.sum_cons, single_add, ih, Multiset.map_cons, Multiset.sum_cons]

Proof state:
α : Type u_1
M : Type u_8
inst✝ : AddCommMonoid M
s✝ : Multiset M
a✝ : α
a : M
s : Multiset M
ih : single a✝ s.sum = (Multiset.map (single a✝) s).sum
⊢ single a✝ (a ::ₘ s).sum = (Multiset.map (single a✝) (a ::ₘ s)).sum

Tactic:
rw [Multiset.sum_cons, single_add, ih, Multiset.map_cons, Multiset.sum_cons]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
theorem mul_inv_cancel (a : G) : a * a⁻¹ = 1

Proof state:
G : Type u_1
inst✝ : Group G
a : G
⊢ a * a⁻¹ = 1

Tactic:
rw [← inv_mul_cancel a⁻¹, inv_eq_of_mul (inv_mul_cancel a)]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem uIcc_injective_left (a : α) : Injective (uIcc a)

Proof state:
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Injective (uIcc a)

Tactic:
simpa only [uIcc_comm] using uIcc_injective_right a

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem DFinsupp.inner_sum {ι : Type*} [DecidableEq ι] {α : ι → Type*}
    [∀ i, AddZeroClass (α i)] [∀ (i) (x : α i), Decidable (x ≠ 0)] (f : ∀ i, α i → E)
    (l : Π₀ i, α i) (x : E) : ⟪x, l.sum f⟫ = l.sum fun i a => ⟪x, f i a⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
α : ι → Type u_5
inst✝¹ : (i : ι) → AddZeroClass (α i)
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f : (i : ι) → α i → E
l : Π₀ (i : ι), α i
x : E
⊢ ⟪x, l.sum f⟫_𝕜 = l.sum fun i a => ⟪x, f i a⟫_𝕜

Tactic:
simp +contextual only [DFinsupp.sum, inner_sum, smul_eq_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem circleMap_not_mem_ball (c : ℂ) (R : ℝ) (θ : ℝ) : circleMap c R θ ∉ ball c R

Proof state:
c : ℂ
R θ : ℝ
⊢ circleMap c R θ ∉ ball c R

Tactic:
simp [dist_eq, le_abs_self]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_mul_right_Icc' (a b : α) {c : α} (h : 0 < c) :
    (fun x => x * c) '' Icc a b = Icc (a * c) (b * c) :=
  ((Units.mk0 c h.ne').mulRight.image_eq_preimage _).trans (by simp [h, division_def])

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : 0 < c
⊢ ⇑(Equiv.symm (Units.mk0 c ⋯).mulRight) ⁻¹' Icc a b = Icc (a * c) (b * c)

Tactic:
simp [h, division_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftLeft_eq' {x : BitVec w₁} {y : BitVec w₂} : x <<< y = x <<< y.toNat

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x <<< y = x <<< y.toNat

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem projectLeftAssign_property : (projectLeftAssign assign) x = (assign <| .inl x)

Proof state:
aig✝ : AIG Nat
assign : aig✝.CNFVar → Bool
x : Nat
⊢ projectLeftAssign assign x = assign (Sum.inl x)

Tactic:
simp [projectLeftAssign]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_nil (n : ℕ) : ([] : List α).rotate n = []

Proof state:
α : Type u
n : ℕ
⊢ [].rotate n = []

Tactic:
simp [rotate]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem coe_iSup_of_directed {ι} [Nonempty ι] {S : ι → Subgroup G} (hS : Directed (· ≤ ·) S) :
    ((⨆ i, S i : Subgroup G) : Set G) = ⋃ i, S i :=
  Set.ext fun x ↦ by simp [mem_iSup_of_directed hS]

Proof state:
G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : G
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
simp [mem_iSup_of_directed hS]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Free.lean
theorem _root_.Module.finrank_eq_card_chooseBasisIndex [Module.Finite R M] :
    finrank R M = Fintype.card (ChooseBasisIndex R M)

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ finrank R M = Fintype.card (ChooseBasisIndex R M)

Tactic:
simp [finrank, rank_eq_card_chooseBasisIndex]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem map_mul_left (z) : k.toMap (g (f.sec z).2) * f.map hy k z = k.toMap (g (f.sec z).1)

Proof state:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
z : N
⊢ k.toMap (g ↑(f.sec z).2) * (f.map hy k) z = k.toMap (g (f.sec z).1)

Tactic:
rw [mul_comm, f.map_mul_right]

Result:
no goals
-- Mathlib/CategoryTheory/Action/Monoidal.lean
theorem rightDual_ρ [RightRigidCategory V] (h : H) : Xᘁ.ρ h = (X.ρ (h⁻¹ : H))ᘁ

Proof state:
V : Type (u + 1)
inst✝³ : LargeCategory V
inst✝² : MonoidalCategory V
H : Type u
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ Xᘁ.ρ h = X.ρ h⁻¹ᘁ

Tactic:
rw [← SingleObj.inv_as_inv]

Result:
V : Type (u + 1)
inst✝³ : LargeCategory V
inst✝² : MonoidalCategory V
H : Type u
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ Xᘁ.ρ h = X.ρ (inv h)ᘁ

case x
V : Type (u + 1)
inst✝³ : LargeCategory V
inst✝² : MonoidalCategory V
H : Type u
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ SingleObj H

case y
V : Type (u + 1)
inst✝³ : LargeCategory V
inst✝² : MonoidalCategory V
H : Type u
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ SingleObj H

Proof state:
V : Type (u + 1)
inst✝³ : LargeCategory V
inst✝² : MonoidalCategory V
H : Type u
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ Xᘁ.ρ h = X.ρ (inv h)ᘁ

case x
V : Type (u + 1)
inst✝³ : LargeCategory V
inst✝² : MonoidalCategory V
H : Type u
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ SingleObj H

case y
V : Type (u + 1)
inst✝³ : LargeCategory V
inst✝² : MonoidalCategory V
H : Type u
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ SingleObj H

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem filter_apply (a : α) :
    (p.filter s h) a = s.indicator p a * (∑' a', (s.indicator p) a')⁻¹

Proof state:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
⊢ (p.filter s h) a = s.indicator (⇑p) a * (∑' (a' : α), s.indicator (⇑p) a')⁻¹

Tactic:
rw [filter, normalize_apply]

Result:
no goals
-- Mathlib/Data/Finsupp/Pointwise.lean
lemma support_mul_subset_left {g₁ g₂ : α →₀ β} :
    (g₁ * g₂).support ⊆ g₁.support := fun x hx => by
  aesop

Proof state:
α : Type u₁
β : Type u₂
inst✝ : MulZeroClass β
g₁ g₂ : α →₀ β
x : α
hx : x ∈ (g₁ * g₂).support
⊢ x ∈ g₁.support

Tactic:
aesop

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem isLUB_l_image {s : Set α} {a : α} (h : IsLUB s a) : IsLUB (l '' s) (l a) :=
  ⟨gc.monotone_l.mem_upperBounds_image h.left, fun b hb =>
    gc.l_le <| h.right <| by rwa [gc.upperBounds_l_image] at hb⟩

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
a : α
h : IsLUB s a
b : β
hb : b ∈ upperBounds (l '' s)
⊢ u b ∈ upperBounds s

Tactic:
rwa [gc.upperBounds_l_image] at hb

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_iff_append {a : α} {l : List α} : a ∈ l ↔ ∃ s t : List α, l = s ++ a :: t :=
  ⟨append_of_mem, fun ⟨s, t, e⟩ => e ▸ by simp⟩

Proof state:
α : Type u_1
a : α
l : List α
x✝ : ∃ s t, l = s ++ a :: t
s t : List α
e : l = s ++ a :: t
⊢ a ∈ s ++ a :: t

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_singleton (e : α) : ({e} : Set α).encard = 1

Proof state:
α : Type u_1
e : α
⊢ {e}.encard = 1

Tactic:
rw [encard, ENat.card_eq_coe_fintype_card, Fintype.card_ofSubsingleton, Nat.cast_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List ((a : α) × β a)} {k : α}
    (h' : (l.map Sigma.fst).contains k = false) :
    (m.insertMany l).1.getKey? k = m.getKey? k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List ((a : α) × β a)
k : α
h' : (List.map Sigma.fst l).contains k = false
⊢ (m.insertMany l).val.getKey? k = m.getKey? k

Tactic:
simp_to_model [insertMany] using List.getKey?_insertList_of_contains_eq_false

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h'} :
    get (m.erase k) a h' = get m a (mem_of_mem_erase h h')

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

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

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma Nonempty.smul_zero (hs : s.Nonempty) : s • (0 : Finset β) = 0 :=
  s.smul_zero_subset.antisymm <| by simpa [mem_smul] using hs

Proof state:
α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Zero β
inst✝ : SMulZeroClass α β
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ s • 0

Tactic:
simpa [mem_smul] using hs

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem sum_smul_vsub_const_eq_weightedVSub (w : ι → k) (p₁ : ι → P) (p₂ : P)
    (h : ∑ i ∈ s, w i = 0) : (∑ i ∈ s, w i • (p₁ i -ᵥ p₂)) = s.weightedVSub p₁ w

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
p₂ : P
h : ∑ i ∈ s, w i = 0
⊢ ∑ i ∈ s, w i • (p₁ i -ᵥ p₂) = (s.weightedVSub p₁) w

Tactic:
rw [sum_smul_vsub_eq_weightedVSub_sub, s.weightedVSub_apply_const _ _ h, sub_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
theorem Gamma_two : Gamma 2 = 1

Proof state:
⊢ Gamma 2 = 1

Tactic:
simp [Nat.factorial_one]

Result:
no goals
-- Mathlib/Tactic/Module.lean
theorem add_eq_eval₁ [AddMonoid M] [SMul R M] (a₁ : R × M) {a₂ : R × M} {l₁ l₂ l : NF R M}
    (h : l₁.eval + (a₂ ::ᵣ l₂).eval = l.eval) :
    (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

Proof state:
R : Type u_2
M : Type u_3
inst✝¹ : AddMonoid M
inst✝ : SMul R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : l₁.eval + (a₂ ::ᵣ l₂).eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h, add_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem MeasurePreserving.lintegral_map_equiv [MeasurableSpace β] {ν : Measure β}
    (f : β → ℝ≥0∞) (g : α ≃ᵐ β) (hg : MeasurePreserving g μ ν) :
    ∫⁻ a, f a ∂ν = ∫⁻ a, f (g a) ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSpace β
ν : Measure β
f : β → ℝ≥0∞
g : α ≃ᵐ β
hg : MeasurePreserving (⇑g) μ ν
⊢ ∫⁻ (a : β), f a ∂ν = ∫⁻ (a : α), f (g a) ∂μ

Tactic:
rw [← MeasureTheory.lintegral_map_equiv f g, hg.map_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem sat_def (a : α → Bool) (f : CNF α) : Sat a f ↔ (eval a f = true)

Proof state:
α : Type u_1
a : α → Bool
f : CNF α
⊢ Sat a f ↔ eval a f = true

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem testAgainstNN_zero (μ : FiniteMeasure Ω) : μ.testAgainstNN 0 = 0

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
⊢ μ.testAgainstNN 0 = 0

Tactic:
simpa only [zero_mul] using μ.testAgainstNN_const 0

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
@[simp] lemma hasFPowerSeriesWithinAt_univ :
    HasFPowerSeriesWithinAt f p univ x ↔ HasFPowerSeriesAt f p x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
⊢ HasFPowerSeriesWithinAt f p univ x ↔ HasFPowerSeriesAt f p x

Tactic:
simp only [HasFPowerSeriesWithinAt, hasFPowerSeriesWithinOnBall_univ, HasFPowerSeriesAt]

Result:
no goals
-- Mathlib/Data/Finset/Grade.lean
@[simp] lemma covBy_cons (s : Multiset α) (a : α) : s ⋖ a ::ₘ s :=
  ⟨lt_cons_self _ _, fun t hst hts ↦ (covBy_succ _).2 (card_lt_card hst) <| by
    simpa using card_lt_card hts⟩

Proof state:
α : Type u_1
s : Multiset α
a : α
t : Multiset α
hst : s < t
hts : t < a ::ₘ s
⊢ t.card < succ s.card

Tactic:
simpa using card_lt_card hts

Result:
no goals
-- Mathlib/Order/Cover.lean
theorem not_wcovBy_iff (h : a ≤ b) : ¬a ⩿ b ↔ ∃ c, a < c ∧ c < b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
h : a ≤ b
⊢ ¬a ⩿ b ↔ ∃ c, a < c ∧ c < b

Tactic:
simp_rw [WCovBy, h, true_and, not_forall, exists_prop, not_not]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma toAffine_of_Z_ne_zero {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P z ≠ 0) :
    toAffine W P = .some ((nonsingular_of_Z_ne_zero hPz).mp hP)

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z ≠ 0
⊢ toAffine W P = Affine.Point.some ⋯

Tactic:
rw [toAffine, dif_pos ⟨hP, hPz⟩]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
lemma image_of_range_union_range_eq_univ {α β γ γ' δ δ' : Type*}
    {h : β → α} {f : γ → β} {f₁ : γ' → α} {f₂ : γ → γ'} {g : δ → β} {g₁ : δ' → α} {g₂ : δ → δ'}
    (hf : h ∘ f = f₁ ∘ f₂) (hg : h ∘ g = g₁ ∘ g₂) (hfg : range f ∪ range g = univ) (s : Set β) :
    h '' s = f₁ '' (f₂ '' (f ⁻¹' s)) ∪ g₁ '' (g₂ '' (g ⁻¹' s))

Proof state:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = f₁ '' (f₂ '' (f ⁻¹' s)) ∪ g₁ '' (g₂ '' (g ⁻¹' s))

Tactic:
rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
  image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]

Result:
no goals
-- Mathlib/Data/Rat/Sqrt.lean
theorem sqrt_intCast (z : ℤ) : Rat.sqrt (z : ℚ) = Int.sqrt z

Proof state:
z : ℤ
⊢ sqrt ↑z = ↑(Int.sqrt z)

Tactic:
simp only [sqrt, num_intCast, den_intCast, Nat.sqrt_one, mkRat_one]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_conjTranspose [Star α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α)
    (D : Matrix o m α) : (fromBlocks A B C D)ᴴ = fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝ : Star α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D)ᴴ = fromBlocks Aᴴ Cᴴ Bᴴ Dᴴ

Tactic:
simp only [conjTranspose, fromBlocks_transpose, fromBlocks_map]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem toLp_eq_toLp_iff {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) :
    hf.toLp f = hg.toLp g ↔ f =ᵐ[μ] g

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hf : MemLp f p μ
hg : MemLp g p μ
⊢ toLp f hf = toLp g hg ↔ f =ᶠ[ae μ] g

Tactic:
simp [toLp]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_div (s : Finset ι) (f : ι → M) (a : M) : (𝔼 i ∈ s, f i) / a = 𝔼 i ∈ s, f i / a

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : Semifield M
inst✝ : CharZero M
s : Finset ι
f : ι → M
a : M
⊢ (𝔼 i ∈ s, f i) / a = 𝔼 i ∈ s, f i / a

Tactic:
simp_rw [div_eq_mul_inv, expect_mul]

Result:
no goals
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem ΓSpecIso_obj_hom {X : Scheme.{u}} (U : X.Opens) :
    (Scheme.ΓSpecIso Γ(X, U)).hom = (Spec.map U.topIso.inv).appTop ≫
      U.toScheme.toSpecΓ.appTop ≫ U.topIso.hom

Proof state:
X : Scheme
U : X.Opens
⊢ (Scheme.ΓSpecIso Γ(X, U)).hom =
    Scheme.Hom.appTop (Spec.map U.topIso.inv) ≫ Scheme.Hom.appTop (↑U).toSpecΓ ≫ U.topIso.hom

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Compactification/OnePointEquiv.lean
@[simp]
lemma equivProjectivization_symm_apply_mk (x y : K) (h : (x, y) ≠ 0) :
    (equivProjectivization K).symm (mk K ⟨x, y⟩ h) = if y = 0 then ∞ else y⁻¹ * x

Proof state:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
x y : K
h : (x, y) ≠ 0
⊢ (equivProjectivization K).symm (mk K (x, y) h) = if y = 0 then ∞ else ↑(y⁻¹ * x)

Tactic:
simp [equivProjectivization]

Result:
no goals
-- Mathlib/Algebra/Order/Disjointed.lean
protected lemma Monotone.disjointed_add_one_sup {f : ι → α} (hf : Monotone f) (i : ι) :
    disjointed f (i + 1) ⊔ f i = f (i + 1)

Proof state:
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
hf : Monotone f
i : ι
⊢ disjointed f (i + 1) ⊔ f i = f (i + 1)

Tactic:
simpa only [succ_eq_add_one i] using hf.disjointed_succ_sup i

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasStrictDerivAt.div_const (hc : HasStrictDerivAt c c' x) (d : 𝕜') :
    HasStrictDerivAt (fun x => c x / d) (c' / d) x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasStrictDerivAt c c' x
d : 𝕜'
⊢ HasStrictDerivAt (fun x => c x / d) (c' / d) x

Tactic:
simpa only [div_eq_mul_inv] using hc.mul_const d⁻¹

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_lt_iff_lt_sub_right {a b c : Nat} : a + b < c ↔ a < c - b

Proof state:
a b c : Nat
⊢ a + b < c ↔ a < c - b

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factors_self {X : C} (P : Subobject X) : P.Factors P.arrow :=
  (factors_iff _ _).mpr ⟨𝟙 (P : C), by simp⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Subobject X
⊢ 𝟙 (underlying.obj P) ≫ (representative.obj P).arrow = P.arrow

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Images.lean
theorem coimage_image_factorisation : coimage.π f ≫ coimageImageComparison f ≫ image.ι f = f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ coimage.π f ≫ coimageImageComparison f ≫ image.ι f = f

Tactic:
simp [coimageImageComparison]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem reverse_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) :
    (p.append q).reverse = q.reverse.append p.reverse

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).reverse = q.reverse.append p.reverse

Tactic:
simp [reverse]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
@[reassoc (attr := simp)]
lemma ιTensorObj₃'_tensorHom (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃)
    (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) :
    ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ tensorHom (tensorHom f₁ f₂) f₃ j =
      ((f₁ i₁ ⊗ f₂ i₂) ⊗ f₃ i₃) ≫ ιTensorObj₃' Y₁ Y₂ Y₃ i₁ i₂ i₃ j h

Proof state:
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₁.HasTensor X₂
inst✝² : (tensorObj X₁ X₂).HasTensor X₃
inst✝¹ : Y₁.HasTensor Y₂
inst✝ : (tensorObj Y₁ Y₂).HasTensor Y₃
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ tensorHom (tensorHom f₁ f₂) f₃ j =
    ((f₁ i₁ ⊗ f₂ i₂) ⊗ f₃ i₃) ≫ ιTensorObj₃' Y₁ Y₂ Y₃ i₁ i₂ i₃ j h

Tactic:
rw [ιTensorObj₃'_eq _ _ _ i₁ i₂ i₃ j h _  rfl,
  ιTensorObj₃'_eq _ _ _ i₁ i₂ i₃ j h _  rfl, assoc, ι_tensorHom,
  ← tensorHom_id, ← tensorHom_id, ← MonoidalCategory.tensor_comp_assoc, id_comp,
  ι_tensorHom, ← MonoidalCategory.tensor_comp_assoc, comp_id]

Result:
no goals
-- Mathlib/GroupTheory/Coset/Card.lean
theorem card_quotient_dvd_card (s : Subgroup α) : Nat.card (α ⧸ s) ∣ Nat.card α

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card (α ⧸ s) ∣ Nat.card α

Tactic:
simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_right ℕ]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernelSubobjectMap_arrow (sq : Arrow.mk f ⟶ Arrow.mk f') :
    kernelSubobjectMap sq ≫ (kernelSubobject f').arrow = (kernelSubobject f).arrow ≫ sq.left

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasKernel f'
sq : Arrow.mk f ⟶ Arrow.mk f'
⊢ kernelSubobjectMap sq ≫ (kernelSubobject f').arrow = (kernelSubobject f).arrow ≫ sq.left

Tactic:
simp [kernelSubobjectMap]

Result:
no goals