harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dimension/Finrank.lean
theorem LinearMap.finrank_range_of_inj {f : M →ₗ[R] N} (hf : Function.Injective f) :
    finrank R (LinearMap.range f) = finrank R M

Proof state:
R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Injective ⇑f
⊢ finrank R ↥(range f) = finrank R M

Tactic:
rw [(LinearEquiv.ofInjective f hf).finrank_eq]

Result:
no goals
-- Mathlib/Topology/Order/LawsonTopology.lean
lemma lawsonClosed_iff_scottClosed_of_isLowerSet (s : Set α) (h : IsLowerSet s) :
    IsClosed[L] s ↔ IsClosed[S] s

Proof state:
α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsClosed s ↔ IsClosed s

Tactic:
rw [← @isOpen_compl_iff, ← isOpen_compl_iff,
  (lawsonOpen_iff_scottOpen_of_isUpperSet' L S _ (isUpperSet_compl.mpr h))]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem _root_.Wbtw.angle₃₁₂_eq_zero_of_ne {p₁ p₂ p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) (hp₂p₁ : p₂ ≠ p₁) :
    ∠ p₃ p₁ p₂ = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : Wbtw ℝ p₁ p₂ p₃
hp₂p₁ : p₂ ≠ p₁
⊢ ∠ p₃ p₁ p₂ = 0

Tactic:
rw [← h.angle₂₁₃_eq_zero_of_ne hp₂p₁, angle_comm]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Coherence.lean
lemma insert_id_lhs {C : Type*} [Category C] {X Y : C} (f g : X ⟶ Y) (w : f ≫ 𝟙 _ = g) :
    f = g

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
w : f ≫ 𝟙 Y = g
⊢ f = g

Tactic:
simpa using w

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem isCycleOn_one : (1 : Perm α).IsCycleOn s ↔ s.Subsingleton

Proof state:
α : Type u_2
s : Set α
⊢ IsCycleOn 1 s ↔ s.Subsingleton

Tactic:
simp [IsCycleOn, Set.bijOn_id, Set.Subsingleton]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@[simp] lemma sum_eq_zero : sum f = 0 ↔ ∀ i, f i = 0

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
f : ι → Measure α
⊢ sum f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
simp +contextual [Measure.ext_iff, forall_swap (α := ι)]

Result:
no goals
-- Mathlib/Order/Category/PartOrd.lean
lemma hom_inv_apply {X Y : PartOrd} (e : X ≅ Y) (s : Y) : e.hom (e.inv s) = s

Proof state:
X Y : PartOrd
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem MemLp.inner_const {f : α → E} (hf : MemLp f p μ) (c : E) : MemLp (fun a => ⟪f a, c⟫) p μ :=
  hf.of_le_mul (c := ‖c‖) (AEStronglyMeasurable.inner hf.1 aestronglyMeasurable_const)
    (Eventually.of_forall fun x => by rw [mul_comm]; exact norm_inner_le_norm _ _)

Proof state:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : MemLp f p μ
c : E
x : α
⊢ ‖inner (f x) c‖ ≤ ‖f x‖ * ‖c‖

Tactic:
exact norm_inner_le_norm _ _

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : MemLp f p μ
c : E
x : α
⊢ ‖inner (f x) c‖ ≤ ‖c‖ * ‖f x‖

Tactic:
rw [mul_comm]

Result:
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : MemLp f p μ
c : E
x : α
⊢ ‖inner (f x) c‖ ≤ ‖f x‖ * ‖c‖
-- Mathlib/Algebra/Group/Hom/Defs.lean
theorem comp_one [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : N →* P) :
    f.comp (1 : M →* N) = 1

Proof state:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
⊢ f.comp 1 = 1

Tactic:
ext

Result:
case h
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
x✝ : M
⊢ (f.comp 1) x✝ = 1 x✝

Proof state:
case h
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
x✝ : M
⊢ (f.comp 1) x✝ = 1 x✝

Tactic:
simp only [map_one, coe_comp, Function.comp_apply, one_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Basic.lean
@[reassoc (attr := simp)]
lemma _root_.CategoryTheory.Iso.hom_inv_id_triangle_hom₂ {A B : Triangle C} (e : A ≅ B) :
    e.hom.hom₂ ≫ e.inv.hom₂ = 𝟙 _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ e.hom.hom₂ ≫ e.inv.hom₂ = 𝟙 A.obj₂

Tactic:
rw [← comp_hom₂, e.hom_inv_id, id_hom₂]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem mem_dualCoannihilator {Φ : Submodule R (Module.Dual R M)} (x : M) :
    x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, (φ x : R) = 0

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Φ : Submodule R (Dual R M)
x : M
⊢ x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, φ x = 0

Tactic:
simp_rw [dualCoannihilator, mem_comap, mem_dualAnnihilator, Module.Dual.eval_apply]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Lemmas.lean
lemma antilipschitzWith_mul_right {a : α} (ha : a ≠ 0) : AntilipschitzWith (‖a‖₊⁻¹) (· * a) :=
  AntilipschitzWith.of_le_mul_dist fun _ _ ↦ by
    simp [dist_eq_norm, ← _root_.sub_mul, ← mul_comm (‖a‖), ha]

Proof state:
α : Type u_1
inst✝ : NormedDivisionRing α
a : α
ha : a ≠ 0
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ ≤ ↑‖a‖₊⁻¹ * dist (x✝¹ * a) (x✝ * a)

Tactic:
simp [dist_eq_norm, ← _root_.sub_mul, ← mul_comm (‖a‖), ha]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem center_zero (z : ℍ) : center z 0 = z :=
  ext' rfl <| by rw [center_im, Real.cosh_zero, mul_one]

Proof state:
z : ℍ
⊢ (z.center 0).im = z.im

Tactic:
rw [center_im, Real.cosh_zero, mul_one]

Result:
no goals
-- Mathlib/Data/List/Perm/Basic.lean
theorem map_append_flatMap_perm (l : List α) (f : α → β) (g : α → List β) :
    l.map f ++ l.flatMap g ~ l.flatMap fun x => f x :: g x

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β
g : α → List β
⊢ map f l ++ flatMap g l ~ flatMap (fun x => f x :: g x) l

Tactic:
simpa [← map_eq_flatMap] using flatMap_append_perm l (fun x => [f x]) g

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem comap_unop_mul :
    comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (M * N) =
      comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) N *
        comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
⊢ comap (↑(opLinearEquiv R).symm) (M * N) = comap (↑(opLinearEquiv R).symm) N * comap (↑(opLinearEquiv R).symm) M

Tactic:
simp_rw [← map_equiv_eq_comap_symm, map_op_mul]

Result:
no goals
-- Mathlib/Data/Finset/Order.lean
theorem Directed.finset_le {r : α → α → Prop} [IsTrans α r] {ι} [hι : Nonempty ι] {f : ι → α}
    (D : Directed r f) (s : Finset ι) : ∃ z, ∀ i ∈ s, r (f i) (f z) :=
  show ∃ z, ∀ i ∈ s.1, r (f i) (f z) from
    Multiset.induction_on s.1 (let ⟨z⟩ := hι; ⟨z, fun _ ↦ by simp⟩)
      fun i _ ⟨j, H⟩ ↦
      let ⟨k, h₁, h₂⟩ := D i j
      ⟨k, fun _ h ↦ (Multiset.mem_cons.1 h).casesOn (fun h ↦ h.symm ▸ h₁)
        fun h ↦ _root_.trans (H _ h) h₂⟩

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsTrans α r
ι : Type u_1
hι : Nonempty ι
f : ι → α
D : Directed r f
s : Finset ι
z x✝ : ι
⊢ x✝ ∈ 0 → r (f x✝) (f z)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem comap_le_comap_iff {f : F} (hf : range f = ⊤) {p p'} : comap f p ≤ comap f p' ↔ p ≤ p' :=
  ⟨fun H ↦ by rwa [SetLike.le_def, (range_eq_top.1 hf).forall], comap_mono⟩

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : F
hf : range f = ⊤
p p' : Submodule R₂ M₂
H : comap f p ≤ comap f p'
⊢ p ≤ p'

Tactic:
rwa [SetLike.le_def, (range_eq_top.1 hf).forall]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem modEq_iff_int_modEq {a b z : ℤ} : a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z]

Proof state:
a b z : ℤ
⊢ a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z]

Tactic:
simp [ModEq, dvd_iff_exists_eq_mul_left, Int.modEq_iff_dvd]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Pi.lean
theorem integral_fintype_prod_eq_prod (ι : Type*) [Fintype ι] {E : ι → Type*}
    (f : (i : ι) → E i → 𝕜) [∀ i, MeasureSpace (E i)] [∀ i, SigmaFinite (volume : Measure (E i))] :
    ∫ x : (i : ι) → E i, ∏ i, f i (x i) = ∏ i, ∫ x, f i x

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
ι : Type u_2
inst✝² : Fintype ι
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
inst✝¹ : (i : ι) → MeasureSpace (E i)
inst✝ : ∀ (i : ι), SigmaFinite volume
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ ∫ (x : (b : Fin (card ι)) → E (e b)), ∏ i : ι, f i ((MeasurableEquiv.piCongrLeft E e) x i) =
    ∏ i : ι, ∫ (x : E i), f i x

Tactic:
simp_rw [← e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Equiv.piCongrLeft_apply_apply,
  MeasureTheory.integral_fin_nat_prod_eq_prod]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
ι : Type u_2
inst✝² : Fintype ι
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
inst✝¹ : (i : ι) → MeasureSpace (E i)
inst✝ : ∀ (i : ι), SigmaFinite volume
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ ∫ (x : (i : ι) → E i), ∏ i : ι, f i (x i) = ∏ i : ι, ∫ (x : E i), f i x

Tactic:
rw [← (volume_measurePreserving_piCongrLeft _ e).integral_comp']

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
ι : Type u_2
inst✝² : Fintype ι
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
inst✝¹ : (i : ι) → MeasureSpace (E i)
inst✝ : ∀ (i : ι), SigmaFinite volume
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ ∫ (x : (b : Fin (card ι)) → E (e b)), ∏ i : ι, f i ((MeasurableEquiv.piCongrLeft E e) x i) =
    ∏ i : ι, ∫ (x : E i), f i x

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
ι : Type u_2
inst✝² : Fintype ι
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
inst✝¹ : (i : ι) → MeasureSpace (E i)
inst✝ : ∀ (i : ι), SigmaFinite volume
⊢ ∫ (x : (i : ι) → E i), ∏ i : ι, f i (x i) = ∏ i : ι, ∫ (x : E i), f i x

Tactic:
let e := (equivFin ι).symm

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
ι : Type u_2
inst✝² : Fintype ι
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
inst✝¹ : (i : ι) → MeasureSpace (E i)
inst✝ : ∀ (i : ι), SigmaFinite volume
e : Fin (card ι) ≃ ι := (equivFin ι).symm
⊢ ∫ (x : (i : ι) → E i), ∏ i : ι, f i (x i) = ∏ i : ι, ∫ (x : E i), f i x
-- Mathlib/Algebra/Polynomial/Div.lean
theorem modByMonic_one (p : R[X]) : p %ₘ 1 = 0 :=
  (modByMonic_eq_zero_iff_dvd (by convert monic_one (R := R))).2 (one_dvd _)

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ Monic 1

Tactic:
convert monic_one (R := R)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem getElem_zero_flatten {L : Array (Array α)} (h) :
    (flatten L)[0] = (L.findSome? fun l => l[0]?).get (getElem_zero_flatten.proof h)

Proof state:
α : Type u_1
L : Array (Array α)
h : 0 < L.flatten.size
t : L.flatten[0]? = findSome? (fun l => l[0]?) L
⊢ L.flatten[0] = (findSome? (fun l => l[0]?) L).get ⋯

Tactic:
simp [← t]

Result:
no goals

Proof state:
α : Type u_1
L : Array (Array α)
h : 0 < L.flatten.size
⊢ L.flatten[0] = (findSome? (fun l => l[0]?) L).get ⋯

Tactic:
have t := getElem?_zero_flatten L

Result:
α : Type u_1
L : Array (Array α)
h : 0 < L.flatten.size
t : L.flatten[0]? = findSome? (fun l => l[0]?) L
⊢ L.flatten[0] = (findSome? (fun l => l[0]?) L).get ⋯
-- Mathlib/Order/Filter/Prod.lean
theorem prod_top : f ×ˢ (⊤ : Filter β) = f.comap Prod.fst

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
⊢ f ×ˢ ⊤ = comap Prod.fst f

Tactic:
rw [prod_eq_inf, comap_top, inf_top_eq]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
theorem Pi.multipliable {f : ι → ∀ x, π x} : Multipliable f ↔ ∀ x, Multipliable fun i ↦ f i x

Proof state:
α : Type u_1
ι : Type u_4
π : α → Type u_5
inst✝¹ : (x : α) → CommMonoid (π x)
inst✝ : (x : α) → TopologicalSpace (π x)
f : ι → (x : α) → π x
⊢ Multipliable f ↔ ∀ (x : α), Multipliable fun i => f i x

Tactic:
simp only [Multipliable, Pi.hasProd, Classical.skolem]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Basic.lean
theorem finrank_submodule (v : ℙ K V) : finrank K v.submodule = 1

Proof state:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ finrank K ↥(Submodule.span K {v.rep}) = 1

Tactic:
exact finrank_span_singleton v.rep_nonzero

Result:
no goals

Proof state:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ finrank K ↥v.submodule = 1

Tactic:
rw [submodule_eq]

Result:
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ finrank K ↥(Submodule.span K {v.rep}) = 1
-- Mathlib/Data/Fin/Fin2.lean
@[simp] lemma rev_castSucc {n} (i : Fin2 n) : rev (castSucc i) = fs (rev i)

Proof state:
n : ℕ
i : Fin2 n
⊢ i.castSucc.rev = i.rev.fs

Tactic:
induction i <;> simp_all [rev, castSucc, last]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
@[simp] lemma expect_dite_eq (i : ι) (f : ∀ j, i = j → M) :
    𝔼 j ∈ s, (if h : i = j then f j h else 0) = if i ∈ s then f i rfl /ℚ #s else 0

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
⊢ (𝔼 j ∈ s, if h : i = j then f j h else 0) = if i ∈ s then (↑(#s))⁻¹ • f i ⋯ else 0

Tactic:
split_ifs <;> simp [expect, *]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem _root_.Function.Injective.sOppSide_map_iff {s : AffineSubspace R P} {x y : P}
    {f : P →ᵃ[R] P'} (hf : Function.Injective f) :
    (s.map f).SOppSide (f x) (f y) ↔ s.SOppSide x y

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : StrictOrderedCommRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
s : AffineSubspace R P
x y : P
f : P →ᵃ[R] P'
hf : Function.Injective ⇑f
⊢ (map f s).SOppSide (f x) (f y) ↔ s.SOppSide x y

Tactic:
simp_rw [SOppSide, hf.wOppSide_map_iff, mem_map_iff_mem_of_injective hf]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem piecewise_insert_self {j : α} [∀ i, Decidable (i ∈ insert j s)] :
    (insert j s).piecewise f g j = f j

Proof state:
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g j = f j

Tactic:
simp [piecewise]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem integerSetEquivNorm_apply_fst {n : ℕ}
    (a : {a : integerSet K // mixedEmbedding.norm (a : mixedSpace K) = n}) :
    ((integerSetEquivNorm K n a).1 : Ideal (𝓞 K)) =
      span {(preimageOfMemIntegerSet a.val : 𝓞 K)}

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
a : { a // mixedEmbedding.norm ↑a = ↑n }
⊢ ↑↑((integerSetEquivNorm K n) a).1 = Ideal.span {↑(preimageOfMemIntegerSet ↑a)}

Tactic:
simp_rw [integerSetEquivNorm, Equiv.prodSubtypeFstEquivSubtypeProd, Equiv.instTrans_trans,
  Equiv.prodCongrLeft, Equiv.trans_apply, Equiv.subtypeEquiv_apply, Equiv.coe_fn_mk,
  Equiv.subtypeSubtypeEquivSubtypeInter_apply_coe, integerSetEquiv_apply_fst]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_setWidth' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
    getLsbD (setWidth' ge x) i = getLsbD x i

Proof state:
m n : Nat
ge : m ≥ n
x : BitVec n
i : Nat
⊢ (setWidth' ge x).getLsbD i = x.getLsbD i

Tactic:
simp [getLsbD, toNat_setWidth']

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma OverArrows.yonedaCollectionPresheafToA_val_fst (s : yoneda.obj X ⟶ A)
    (p : OverArrows (yonedaCollectionPresheafToA F) s) : p.val.fst = s

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : yoneda.obj X ⟶ A
p : OverArrows (yonedaCollectionPresheafToA F) s
⊢ YonedaCollection.fst p.val = s

Tactic:
simpa [YonedaCollection.yonedaEquivFst_eq] using p.app_val

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Graded/Internal.lean
theorem tmul_coe_mul_zero_coe_tmul {j₁ : ι} (a₁ : A) (b₁ : ℬ j₁) (a₂ : 𝒜 0) (b₂ : B) :
    (a₁ ᵍ⊗ₜ[R] (b₁ : B) * (a₂ : A) ᵍ⊗ₜ[R] b₂ : 𝒜 ᵍ⊗[R] ℬ) =
      ((a₁ * a₂ : A) ᵍ⊗ₜ (b₁ * b₂ : B))

Proof state:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring ι
inst✝⁸ : DecidableEq ι
inst✝⁷ : CommRing R
inst✝⁶ : Ring A
inst✝⁵ : Ring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst✝² : GradedAlgebra 𝒜
inst✝¹ : GradedAlgebra ℬ
inst✝ : Module ι (Additive ℤˣ)
j₁ : ι
a₁ : A
b₁ : ↥(ℬ j₁)
a₂ : ↥(𝒜 0)
b₂ : B
⊢ a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂)

Tactic:
rw [tmul_coe_mul_coe_tmul, mul_zero, uzpow_zero, one_smul]

Result:
no goals
-- Mathlib/Topology/Order/Lattice.lean
lemma ContinuousAt.finset_sup' (hne : s.Nonempty) (hs : ∀ i ∈ s, ContinuousAt (f i) x) :
    ContinuousAt (s.sup' hne f) x

Proof state:
L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
s : Finset ι
f : ι → X → L
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousAt (f i) x
⊢ ContinuousAt (s.sup' hne f) x

Tactic:
simpa only [← Finset.sup'_apply] using finset_sup'_apply hne hs

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra.lean
theorem algebraMap_leftInverse :
    Function.LeftInverse algebraMapInv (algebraMap R <| FreeAlgebra R X) := fun x ↦ by
  simp [algebraMapInv]

Proof state:
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : R
⊢ algebraMapInv ((algebraMap R (FreeAlgebra R X)) x) = x

Tactic:
simp [algebraMapInv]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem mul_inv_rev (A B : Matrix n n α) : (A * B)⁻¹ = B⁻¹ * A⁻¹

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (A * B)⁻¹ = B⁻¹ * A⁻¹

Tactic:
simp only [inv_def]

Result:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ Ring.inverse (A * B).det • (A * B).adjugate = Ring.inverse B.det • B.adjugate * Ring.inverse A.det • A.adjugate

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ Ring.inverse (A * B).det • (A * B).adjugate = Ring.inverse B.det • B.adjugate * Ring.inverse A.det • A.adjugate

Tactic:
rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib,
  Ring.mul_inverse_rev]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem map_filter {f : α ≃ β} {p : α → Prop} [DecidablePred p] :
    (s.filter p).map f.toEmbedding = (s.map f.toEmbedding).filter (p ∘ f.symm)

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
p : α → Prop
inst✝ : DecidablePred p
⊢ map f.toEmbedding (filter p s) = filter (p ∘ ⇑f.symm) (map f.toEmbedding s)

Tactic:
simp only [filter_map, Function.comp_def, Equiv.toEmbedding_apply, Equiv.symm_apply_apply]

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem ofFinsupp_eq_one {a} :
    (⟨a⟩ : SkewMonoidAlgebra k G) = 1 ↔ a = Finsupp.single 1 1

Proof state:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
inst✝¹ : One G
inst✝ : One k
a : G →₀ k
⊢ { toFinsupp := a } = 1 ↔ a = Finsupp.single 1 1

Tactic:
rw [← ofFinsupp_one, ofFinsupp_inj]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
@[simp]
lemma uIcc_of_le (h : a ≤ b) : [[a, b]] = Icc a b

Proof state:
α : Type u_1
inst✝ : Lattice α
a b : α
h : a ≤ b
⊢ [[a, b]] = Icc a b

Tactic:
rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
lemma congr_φH {γ₁ γ₂ : RightHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) : γ₁.φH = γ₂.φH

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ₁ γ₂ : RightHomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
⊢ γ₁.φH = γ₂.φH

Tactic:
rw [eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/DotProduct.lean
lemma conjTranspose_mul_self_mulVec_eq_zero (A : Matrix m n R) (v : n → R) :
    (Aᴴ * A) *ᵥ v = 0 ↔ A *ᵥ v = 0

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
v : n → R
⊢ (Aᴴ * A) *ᵥ v = 0 ↔ A *ᵥ v = 0

Tactic:
simpa only [← Matrix.col_mulVec, col_eq_zero] using
  conjTranspose_mul_self_mul_eq_zero A (col (Fin 1) v)

Result:
no goals
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
lemma HurwitzZeta.completedCosZeta_zero (s : ℂ) :
    completedCosZeta 0 s = completedRiemannZeta s

Proof state:
s : ℂ
⊢ completedCosZeta 0 s = completedRiemannZeta s

Tactic:
rw [completedRiemannZeta, completedHurwitzZetaEven, completedCosZeta, hurwitzEvenFEPair_zero_symm]

Result:
no goals
-- Mathlib/Algebra/Homology/HasNoLoop.lean
lemma hasNoLoop_up' {α : Type*} [AddZeroClass α] [IsRightCancelAdd α] [IsLeftCancelAdd α]
    (a : α) (ha : a ≠ 0) :
    (up' a).HasNoLoop where
  not_rel_self i (hi : _ = _) :=
    ha (add_left_cancel (by rw [add_zero, hi]))

Proof state:
α : Type u_2
inst✝² : AddZeroClass α
inst✝¹ : IsRightCancelAdd α
inst✝ : IsLeftCancelAdd α
a : α
ha : a ≠ 0
i : α
hi : i + a = i
⊢ ?m.1880 i hi + a = ?m.1880 i hi + 0

Tactic:
rw [add_zero, hi]

Result:
no goals
-- Mathlib/Topology/Clopen.lean
theorem continuous_boolIndicator_iff_isClopen (U : Set X) :
    Continuous U.boolIndicator ↔ IsClopen U

Proof state:
X : Type u
inst✝ : TopologicalSpace X
U : Set X
⊢ Continuous U.boolIndicator ↔ IsClopen U

Tactic:
rw [continuous_bool_rng true, preimage_boolIndicator_true]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem continuousInv_iInf {ts' : ι' → TopologicalSpace G}
    (h' : ∀ i, @ContinuousInv G (ts' i) _) : @ContinuousInv G (⨅ i, ts' i) _

Proof state:
G : Type w
ι' : Sort u_1
inst✝ : Inv G
ts' : ι' → TopologicalSpace G
h' : ∀ (i : ι'), ContinuousInv G
⊢ ContinuousInv G

Tactic:
exact continuousInv_sInf (Set.forall_mem_range.mpr h')

Result:
no goals
-- Mathlib/Data/Part.lean
theorem union_mem_union [Union α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :
    ma ∪ mb ∈ a ∪ b

Proof state:
α : Type u_1
inst✝ : Union α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1 ∈ a, ∃ a ∈ b, a_1 ∪ a = ma ∪ mb

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Union α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ∪ mb ∈ a ∪ b

Tactic:
simp [union_def]

Result:
α : Type u_1
inst✝ : Union α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1 ∈ a, ∃ a ∈ b, a_1 ∪ a = ma ∪ mb
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem abs_sin_eq_of_two_zsmul_eq {θ ψ : Angle} (h : (2 : ℤ) • θ = (2 : ℤ) • ψ) :
    |sin θ| = |sin ψ|

Proof state:
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ |θ.sin| = |ψ.sin|

Tactic:
exact abs_sin_eq_of_two_nsmul_eq h

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
/-- The norm, relative to `ℤ`, of `ζ - 1` in a `p ^ (k + 1)`-th cyclotomic extension of `ℚ` is
`p` if `p ≠ 2`. -/
lemma norm_toInteger_sub_one_of_prime_ne_two [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hodd : p ≠ 2) :
    Algebra.norm ℤ (hζ.toInteger - 1) = p

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hodd : p ≠ 2
⊢ (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p

Tactic:
simpa only [pow_zero, pow_one] using
  hζ.norm_toInteger_pow_sub_one_of_prime_ne_two (Nat.zero_le _) hodd

Result:
no goals