harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Ring/Basic.lean
lemma noZeroDivisors_iff_isDomain_or_subsingleton [Ring α] :
    NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α

Proof state:
α : Type u_2
inst✝ : Ring α
⊢ NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α

Tactic:
rw [← isCancelMulZero_iff_noZeroDivisors, isCancelMulZero_iff_isDomain_or_subsingleton]

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem isReflection_of_mem_leftInvSeq (ω : List B) {t : W} (ht : t ∈ lis ω) :
    cs.IsReflection t

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
t : W
ht : t ∈ cs.leftInvSeq ω
⊢ cs.IsReflection t

Tactic:
simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse, mem_reverse] at ht

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
t : W
ht : t ∈ cs.rightInvSeq ω.reverse
⊢ cs.IsReflection t

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
t : W
ht : t ∈ cs.rightInvSeq ω.reverse
⊢ cs.IsReflection t

Tactic:
exact cs.isReflection_of_mem_rightInvSeq ω.reverse ht

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem natCast_mul_comp {n : ℕ} : ((n : R[X]) * p).comp r = n * p.comp r

Proof state:
R : Type u
inst✝ : Semiring R
p r : R[X]
n : ℕ
⊢ (↑n * p).comp r = ↑n * p.comp r

Tactic:
rw [← C_eq_natCast, C_mul_comp]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.smul_measure {f : α → β} (h : Integrable f μ) {c : ℝ≥0∞} (hc : c ≠ ∞) :
    Integrable f (c • μ)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : MemLp f 1 μ
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ MemLp f 1 (c • μ)

Tactic:
exact h.smul_measure hc

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : Integrable f μ
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ Integrable f (c • μ)

Tactic:
rw [← memLp_one_iff_integrable] at h ⊢

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : MemLp f 1 μ
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ MemLp f 1 (c • μ)
-- Mathlib/Analysis/BoxIntegral/Partition/Additive.lean
theorem map_split_add (f : ι →ᵇᵃ[I₀] M) (hI : ↑I ≤ I₀) (i : ι) (x : ℝ) :
    (I.splitLower i x).elim' 0 f + (I.splitUpper i x).elim' 0 f = f I

Proof state:
ι : Type u_1
M : Type u_2
inst✝ : AddCommMonoid M
I₀ : WithTop (Box ι)
I : Box ι
f : ι →ᵇᵃ[I₀] M
hI : ↑I ≤ I₀
i : ι
x : ℝ
⊢ Option.elim' 0 (⇑f) (I.splitLower i x) + Option.elim' 0 (⇑f) (I.splitUpper i x) = f I

Tactic:
rw [← f.sum_partition_boxes hI (isPartitionSplit I i x), sum_split_boxes]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem glued_cover_cocycle_snd (x y z : 𝒰.J) :
    gluedCoverT' 𝒰 x y z ≫ gluedCoverT' 𝒰 y z x ≫ gluedCoverT' 𝒰 z x y ≫ pullback.snd _ _ =
      pullback.snd _ _

Proof state:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.snd (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) =
    pullback.snd (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z))

Tactic:
apply pullback.hom_ext <;> simp [pullback.condition]

Result:
no goals
-- Mathlib/Data/Finset/Filter.lean
theorem filter_congr_decidable (s : Finset α) (p : α → Prop) (h : DecidablePred p)
    [DecidablePred p] : @filter α p h s = s.filter p

Proof state:
α : Type u_1
s : Finset α
p : α → Prop
h inst✝ : DecidablePred p
⊢ filter p s = filter p s

Tactic:
congr

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
@[simp] lemma div_ratCast_re (z : ℂ) (x : ℚ) : (z / x).re = z.re / x

Proof state:
z : ℂ
x : ℚ
⊢ (z / ↑x).re = z.re / ↑x

Tactic:
rw [div_ratCast]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem mono_pre_nat (m : Set X → ℝ≥0∞) : Monotone fun k : ℕ => pre m k⁻¹ :=
  fun k l h => le_pre.2 fun _ hs => pre_le (hs.trans <| by simpa)

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
m : Set X → ℝ≥0∞
k l : ℕ
h : k ≤ l
x✝ : Set X
hs : diam x✝ ≤ (↑l)⁻¹
⊢ (↑l)⁻¹ ≤ (↑k)⁻¹

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Sigma.fst)
    {h'} :
    (m.insertMany l).getKey k' h' = k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Sigma.fst l
h' : k' ∈ m.insertMany l
⊢ (m.insertMany l).getKey k' h' = k

Tactic:
simp_to_raw using Raw₀.getKey_insertMany_list_of_mem

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombination_subtype_eq_filter (w : ι → k) (p : ι → P) (pred : ι → Prop)
    [DecidablePred pred] :
    ((s.subtype pred).affineCombination k (fun i => p i) fun i => w i) =
      {x ∈ s | pred x}.affineCombination k 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
pred : ι → Prop
inst✝ : DecidablePred pred
⊢ ((affineCombination k (Finset.subtype pred s) fun i => p ↑i) fun i => w ↑i) =
    (affineCombination k (filter (fun x => pred x) s) p) w

Tactic:
rw [affineCombination_apply, affineCombination_apply, weightedVSubOfPoint_subtype_eq_filter]

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem Chain.iff_mem {a : α} {l : List α} :
    Chain R a l ↔ Chain (fun x y => x ∈ a :: l ∧ y ∈ l ∧ R x y) a l :=
  ⟨fun p => by
    induction p with
    | nil => exact nil
    | @cons _ _ _ r _ IH =>
      constructor
      · exact ⟨mem_cons_self _ _, mem_cons_self _ _, r⟩
      · exact IH.imp fun a b ⟨am, bm, h⟩ => ⟨mem_cons_of_mem _ am, mem_cons_of_mem _ bm, h⟩,
    Chain.imp fun _ _ h => h.2.2⟩

Proof state:
case cons
α : Type u
R : α → α → Prop
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
IH : Chain (fun x y => x ∈ b✝ :: l✝ ∧ y ∈ l✝ ∧ R x y) b✝ l✝
⊢ Chain (fun x y => x ∈ a✝¹ :: b✝ :: l✝ ∧ y ∈ b✝ :: l✝ ∧ R x y) a✝¹ (b✝ :: l✝)

Tactic:
constructor

Result:
case cons.a
α : Type u
R : α → α → Prop
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
IH : Chain (fun x y => x ∈ b✝ :: l✝ ∧ y ∈ l✝ ∧ R x y) b✝ l✝
⊢ a✝¹ ∈ a✝¹ :: b✝ :: l✝ ∧ b✝ ∈ b✝ :: l✝ ∧ R a✝¹ b✝

case cons.a
α : Type u
R : α → α → Prop
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
IH : Chain (fun x y => x ∈ b✝ :: l✝ ∧ y ∈ l✝ ∧ R x y) b✝ l✝
⊢ Chain (fun x y => x ∈ a✝¹ :: b✝ :: l✝ ∧ y ∈ b✝ :: l✝ ∧ R x y) b✝ l✝

Proof state:
case nil
α : Type u
R : α → α → Prop
a : α
l : List α
a✝ : α
⊢ Chain (fun x y => x ∈ [a✝] ∧ y ∈ [] ∧ R x y) a✝ []

Tactic:
exact nil

Result:
no goals

Proof state:
case cons.a
α : Type u
R : α → α → Prop
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
IH : Chain (fun x y => x ∈ b✝ :: l✝ ∧ y ∈ l✝ ∧ R x y) b✝ l✝
⊢ a✝¹ ∈ a✝¹ :: b✝ :: l✝ ∧ b✝ ∈ b✝ :: l✝ ∧ R a✝¹ b✝

Tactic:
exact ⟨mem_cons_self _ _, mem_cons_self _ _, r⟩

Result:
no goals

Proof state:
case cons.a
α : Type u
R : α → α → Prop
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
IH : Chain (fun x y => x ∈ b✝ :: l✝ ∧ y ∈ l✝ ∧ R x y) b✝ l✝
⊢ Chain (fun x y => x ∈ a✝¹ :: b✝ :: l✝ ∧ y ∈ b✝ :: l✝ ∧ R x y) b✝ l✝

Tactic:
exact IH.imp fun a b ⟨am, bm, h⟩ => ⟨mem_cons_of_mem _ am, mem_cons_of_mem _ bm, h⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reverse_leadingCoeff (f : R[X]) : f.reverse.leadingCoeff = f.trailingCoeff

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.leadingCoeff = f.trailingCoeff

Tactic:
rw [leadingCoeff, reverse_natDegree, ← revAt_le f.natTrailingDegree_le_natDegree,
  coeff_reverse, revAt_invol, trailingCoeff]

Result:
no goals
-- Mathlib/Data/Finset/Fold.lean
theorem fold_hom {op' : γ → γ → γ} [Std.Commutative op'] [Std.Associative op'] {m : β → γ}
    (hm : ∀ x y, m (op x y) = op' (m x) (m y)) :
    (s.fold op' (m b) fun x => m (f x)) = m (s.fold op b f)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x => m (f x)) s.val) = Multiset.fold op' (m b) (Multiset.map (m ∘ f) s.val)

Tactic:
simp only [Function.comp_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ fold op' (m b) (fun x => m (f x)) s = m (fold op b f s)

Tactic:
rw [fold, fold, ← Multiset.fold_hom op hm, Multiset.map_map]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x => m (f x)) s.val) = Multiset.fold op' (m b) (Multiset.map (m ∘ f) s.val)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKeyD_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α}
    {f : Option β → Option β} :
    (Const.alter m k f).getKeyD k fallback =
      if (f (Const.get? m k)).isSome then k else fallback

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k fallback : α
f : Option β → Option β
⊢ (alter m k f).getKeyD k fallback = if (f (get? m k)).isSome = true then k else fallback

Tactic:
simp [getKeyD_alter]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
@[simp]
lemma outsidePart_add : (p + q).outsidePart = p.outsidePart + q

Proof state:
p q : DyckWord
h : p ≠ 0
⊢ List.drop (p.firstReturn + 1) ↑(p + q) =
    ↑({ toList := List.drop (p.firstReturn + 1) ↑p, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ } + q)

Tactic:
exact drop_append_of_le_length (firstReturn_lt_length h)

Result:
no goals

Proof state:
p q : DyckWord
h : p ≠ 0
⊢ (p + q).outsidePart = p.outsidePart + q

Tactic:
simp_rw [outsidePart, firstReturn_add, add_eq_zero', h, false_and, dite_false, ite_false,
  DyckWord.ext_iff, drop]

Result:
p q : DyckWord
h : p ≠ 0
⊢ List.drop (p.firstReturn + 1) ↑(p + q) =
    ↑({ toList := List.drop (p.firstReturn + 1) ↑p, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ } + q)
-- Mathlib/Algebra/Order/Group/PosPart.lean
/-- See also `leOnePart_le_one`. -/
@[to_additive "See also `negPart_nonpos`."]
lemma leOnePart_le_one' : a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : Group α
a : α
⊢ a⁻ᵐ ≤ 1 ↔ a⁻¹ ≤ 1

Tactic:
simp [leOnePart]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addXYZ_neg {P : Fin 3 → R} (hP : W'.Equation P) :
    W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![0, 1, 0]

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![0, 1, 0]

Tactic:
erw [addXYZ, addX_neg, addY_neg hP, addZ_neg, smul_fin3, mul_zero, mul_one]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem dist_le_mul_of_le (hf : LipschitzWith K f) (hr : dist x y ≤ r) : dist (f x) (f y) ≤ K * r :=
  (hf.dist_le_mul x y).trans <| by gcongr

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ
hf : LipschitzWith K f
hr : dist x y ≤ r
⊢ ↑K * dist x y ≤ ↑K * r

Tactic:
gcongr

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem intNorm_idealSetEquiv_apply (a : idealSet K J) :
    intNorm (idealSetEquiv K J a).val = mixedEmbedding.norm (a : mixedSpace K)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
⊢ ↑(intNorm ↑((idealSetEquiv K J) a)) = mixedEmbedding.norm ↑a

Tactic:
rw [intNorm_coe, idealSetEquiv_apply]

Result:
no goals
-- Mathlib/Order/Filter/Cofinite.lean
lemma Set.Finite.cofinite_inf_principal_diff {s t : Set α} (ht : t.Finite) :
    cofinite ⊓ 𝓟 (s \ t) = cofinite ⊓ 𝓟 s

Proof state:
α : Type u_2
s t : Set α
ht : t.Finite
⊢ cofinite ⊓ 𝓟 (s \ t) = cofinite ⊓ 𝓟 s

Tactic:
rw [diff_eq, ← inf_principal, ← inf_assoc, inf_right_comm, ht.cofinite_inf_principal_compl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.isEmpty_eq {l l' : List α} (h : Perm l l') : l.isEmpty = l'.isEmpty

Proof state:
α : Type u_1
l l' : List α
h : l ~ l'
⊢ l.isEmpty = l'.isEmpty

Tactic:
cases l <;> cases l' <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem any_eq (s : String) (p : Char → Bool) : any s p = s.1.any p

Proof state:
s : String
p : Char → Bool
⊢ s.any p = s.data.any p

Tactic:
simpa using anyAux_of_valid p [] s.1 []

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem _root_.Orthonormal.exists_hilbertBasis_extension {s : Set E}
    (hs : Orthonormal 𝕜 ((↑) : s → E)) :
    ∃ (w : Set E) (b : HilbertBasis w 𝕜 E), s ⊆ w ∧ ⇑b = ((↑) : w → E) :=
  let ⟨w, hws, hw_ortho, hw_max⟩ := exists_maximal_orthonormal hs
  ⟨w, HilbertBasis.mkOfOrthogonalEqBot hw_ortho
    (by simpa only [Subtype.range_coe_subtype, Set.setOf_mem_eq,
      maximal_orthonormal_iff_orthogonalComplement_eq_bot hw_ortho] using hw_max),
    hws, HilbertBasis.coe_mkOfOrthogonalEqBot _ _⟩

Proof state:
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
w : Set E
hws : w ⊇ s
hw_ortho : Orthonormal 𝕜 Subtype.val
hw_max : ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w
⊢ (span 𝕜 (Set.range Subtype.val))ᗮ = ⊥

Tactic:
simpa only [Subtype.range_coe_subtype, Set.setOf_mem_eq,
maximal_orthonormal_iff_orthogonalComplement_eq_bot hw_ortho] using hw_max

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem coe_eq_zero {f : α →₀ M} : (f : α → M) = 0 ↔ f = 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
⊢ ⇑f = 0 ↔ f = 0

Tactic:
rw [← coe_zero, DFunLike.coe_fn_eq]

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp]
lemma WithTop.toDual_le_toDual_iff {x y : WithTop α} : x.toDual ≤ y.toDual ↔ y ≤ x

Proof state:
α : Type u_1
inst✝ : LE α
x y : WithTop α
⊢ WithTop.toDual x ≤ WithTop.toDual y ↔ y ≤ x

Tactic:
cases x <;> cases y <;> simp [le_toDual]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
@[simp] lemma affineIndependent_vadd {p : ι → P} {v : V} :
    AffineIndependent k (v +ᵥ p) ↔ AffineIndependent k p

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
ι : Type u_4
p : ι → P
v : V
⊢ AffineIndependent k (v +ᵥ p) ↔ AffineIndependent k p

Tactic:
simp +contextual [AffineIndependent, weightedVSub_vadd]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem of_lift {α β} [inst : CSLift α β] {a b : α} {a' b' : β}
    [h1 : CSLiftVal a a'] [h2 : CSLiftVal b b'] (h : a' = b') : a = b :=
  inst.2 <| by rwa [← h1.1, ← h2.1]

Proof state:
α β : Type u_2
inst : CSLift α β
a b : α
a' b' : β
h1 : CSLiftVal a a'
h2 : CSLiftVal b b'
h : a' = b'
⊢ CSLift.lift a = CSLift.lift b

Tactic:
rwa [← h1.1, ← h2.1]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_map (f : α → β) {l} {i : Nat} {h : i < (map f l).length} :
    (map f l)[i] = f (l[i]'(length_map l f ▸ h)) :=
  Option.some.inj <| by rw [← getElem?_eq_getElem, getElem?_map, getElem?_eq_getElem]; rfl

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
i : Nat
h : i < (map f l).length
⊢ Option.map f (some l[i]) = some (f l[i])

α : Type u_1
β : Type u_2
f : α → β
l : List α
i : Nat
h : i < (map f l).length
⊢ i < l.length

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
i : Nat
h : i < (map f l).length
⊢ some (map f l)[i] = some (f l[i])

Tactic:
rw [← getElem?_eq_getElem, getElem?_map, getElem?_eq_getElem]

Result:
α : Type u_1
β : Type u_2
f : α → β
l : List α
i : Nat
h : i < (map f l).length
⊢ Option.map f (some l[i]) = some (f l[i])

α : Type u_1
β : Type u_2
f : α → β
l : List α
i : Nat
h : i < (map f l).length
⊢ i < l.length
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma rightHomologyIso_hom_comp_homologyι :
    S.rightHomologyIso.hom ≫ S.homologyι = S.rightHomologyι

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.rightHomologyIso.hom ≫ S.rightHomologyIso.inv ≫ S.rightHomologyι = S.rightHomologyι

Tactic:
simp only [Iso.hom_inv_id_assoc]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.rightHomologyIso.hom ≫ S.homologyι = S.rightHomologyι

Tactic:
dsimp only [homologyι]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.rightHomologyIso.hom ≫ S.rightHomologyIso.inv ≫ S.rightHomologyι = S.rightHomologyι
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_concat_zero : (concat x b).getLsbD 0 = b

Proof state:
w✝ : Nat
x : BitVec w✝
b : Bool
⊢ (x.concat b).getLsbD 0 = b

Tactic:
simp [getLsbD_concat]

Result:
no goals
-- Mathlib/Data/Finset/Density.lean
@[simp] lemma dens_union_of_disjoint (h : Disjoint s t) : dens (s ∪ t) = dens s + dens t

Proof state:
α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ (s ∪ t).dens = s.dens + t.dens

Tactic:
rw [← disjUnion_eq_union s t h, dens_disjUnion _ _ _]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem setLIntegral_eq_tsum (h : IsFundamentalDomain G s μ) (f : α → ℝ≥0∞) (t : Set α) :
    ∫⁻ x in t, f x ∂μ = ∑' g : G, ∫⁻ x in t ∩ g • s, f x ∂μ :=
  calc
    ∫⁻ x in t, f x ∂μ = ∑' g : G, ∫⁻ x in g • s, f x ∂μ.restrict t :=
      h.lintegral_eq_tsum_of_ac restrict_le_self.absolutelyContinuous _
    _ = ∑' g : G, ∫⁻ x in t ∩ g • s, f x ∂μ

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
h : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
t : Set α
⊢ ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂μ.restrict t = ∑' (g : G), ∫⁻ (x : α) in t ∩ g • s, f x ∂μ

Tactic:
simp only [h.restrict_restrict, inter_comm]

Result:
no goals
-- Mathlib/Data/Finset/PImage.lean
theorem mem_toFinset {o : Part α} [Decidable o.Dom] {x : α} : x ∈ o.toFinset ↔ x ∈ o

Proof state:
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
x : α
⊢ x ∈ o.toFinset ↔ x ∈ o

Tactic:
simp [toFinset]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Bounded.lean
@[to_additive isBounded_iff_forall_norm_le]
lemma isBounded_iff_forall_norm_le' : Bornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C

Proof state:
E : Type u_2
inst✝ : SeminormedGroup E
s : Set E
⊢ Bornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C

Tactic:
simpa only [Set.subset_def, mem_closedBall_one_iff] using isBounded_iff_subset_closedBall (1 : E)

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem scalar_eq [Nontrivial A] (k : 𝕜) : σ (↑ₐ k) = {k}

Proof state:
𝕜 : Type u
A : Type v
inst✝³ : Field 𝕜
inst✝² : Ring A
inst✝¹ : Algebra 𝕜 A
inst✝ : Nontrivial A
k : 𝕜
⊢ σ (↑ₐ k) = {k}

Tactic:
rw [← add_zero (↑ₐ k), ← singleton_add_eq, zero_eq, Set.singleton_add_singleton, add_zero]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem coe_equiv_snd_eq_one_iff_mem {g : G} (h1 : 1 ∈ T) :
    ((hST.equiv g).snd : G) = 1 ↔ g ∈ S

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
⊢ ↑(hST.equiv g).2 = 1 ↔ g ∈ S

Tactic:
rw [equiv_snd_eq_inv_mul, inv_mul_eq_one, equiv_fst_eq_self_iff_mem _ h1]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.toSubtype_eq_desc [DecidablePred p] :
    biproduct.toSubtype f p =
      biproduct.desc fun j => if h : p j then biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0 :=
  biproduct.hom_ext' _ _ (by simp)

Proof state:
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
⊢ ∀ (j : J), ι f j ≫ toSubtype f p = ι f j ≫ desc fun j => if h : p j then ι (Subtype.restrict p f) ⟨j, h⟩ else 0

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Assoc.lean
theorem inl_pushoutAssoc_inv [HasPushout (g₃ ≫ (pushout.inr _ _ : X₂ ⟶ Y₁)) g₄]
    [HasPushout g₁ (g₂ ≫ (pushout.inl _ _ : X₂ ⟶ Y₂))] :
    pushout.inl _ _ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv = pushout.inl _ _ ≫ pushout.inl _ _

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv =
    pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄

Tactic:
rw [Iso.comp_inv_eq, Category.assoc, inl_inl_pushoutAssoc_hom]

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem frontier_setOf_le_re_and_le_im (a b : ℝ) :
    frontier { z | a ≤ re z ∧ b ≤ im z } = { z | a ≤ re z ∧ im z = b ∨ re z = a ∧ b ≤ im z }

Proof state:
a b : ℝ
⊢ frontier {z | a ≤ z.re ∧ b ≤ z.im} = {z | a ≤ z.re ∧ z.im = b ∨ z.re = a ∧ b ≤ z.im}

Tactic:
simpa only [closure_Ici, frontier_Ici] using frontier_reProdIm (Ici a) (Ici b)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_setIfInBounds (as : Array α) (index : Nat) (val : α) :
    (as.setIfInBounds index val).size = as.size

Proof state:
α : Type u_1
as : Array α
index : Nat
val : α
h : index < as.size
⊢ (as.setIfInBounds index val).size = as.size

Tactic:
simp [setIfInBounds, h]

Result:
no goals

Proof state:
α : Type u_1
as : Array α
index : Nat
val : α
⊢ (as.setIfInBounds index val).size = as.size

Tactic:
if h : index < as.size  then
  simp [setIfInBounds, h]
else
  simp [setIfInBounds, h]

Result:
no goals

Proof state:
α : Type u_1
as : Array α
index : Nat
val : α
h : ¬index < as.size
⊢ (as.setIfInBounds index val).size = as.size

Tactic:
simp [setIfInBounds, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_empty {a : α} {fallback : β} {c} :
    getD (empty c : Raw₀ α (fun _ => β)) a fallback = fallback

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
a : α
fallback : β
c : Nat
⊢ getD (empty c) a fallback = fallback

Tactic:
simp [getD, empty]

Result:
no goals