harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/Restrict.lean
lemma le_preimage_resLE_iff {U : Y.Opens} {V : X.Opens} (e : V ≤ f ⁻¹ᵁ U)
    (O : U.toScheme.Opens) (W : V.toScheme.Opens) :
    W ≤ (f.resLE U V e) ⁻¹ᵁ O ↔ V.ι ''ᵁ W ≤ f ⁻¹ᵁ U.ι ''ᵁ O

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
⊢ W ≤ resLE f U V e ⁻¹ᵁ O ↔ V.ι ''ᵁ W ≤ f ⁻¹ᵁ U.ι ''ᵁ O

Tactic:
simp [resLE_preimage, ← image_le_image_iff V.ι, image_preimage_eq_opensRange_inter, V.ι_image_le]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk_pow (n : ℕ) (a : M) (b : S) : mk a b ^ n = mk (a ^ n) (b ^ n)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
n : ℕ
a : M
b : ↥S
⊢ mk a b ^ n = mk (a ^ n) (b ^ n)

Tactic:
induction n <;> simp [pow_succ, *, ← mk_mul, ← mk_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem idxOf_toArray [BEq α] {as : List α} {a : α} :
    as.toArray.idxOf a = as.idxOf a

Proof state:
α : Type u_1
inst✝ : BEq α
as : List α
a : α
⊢ Array.idxOf a as.toArray = idxOf a as

Tactic:
rw [Array.idxOf, findIdx_toArray, idxOf]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem eigenspace_zero (f : End R M) : f.eigenspace 0 = LinearMap.ker f

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
⊢ f.eigenspace 0 = LinearMap.ker f

Tactic:
simp only [eigenspace, ← Nat.cast_one (R := ℕ∞), genEigenspace_zero_nat, pow_one]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
lemma surjective_π_iff_span_eq_top :
    Function.Surjective solution.π ↔
      Submodule.span A (Set.range solution.var) = ⊤

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ Function.Surjective ⇑solution.π ↔ Submodule.span A (Set.range solution.var) = ⊤

Tactic:
rw [← LinearMap.range_eq_top, range_π]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
@[simp] lemma smul_mk'_self {m : M} {r : R} :
    (m : R) • mk' S r m = algebraMap R S r

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
m : ↥M
r : R
⊢ ↑m • mk' S r m = (algebraMap R S) r

Tactic:
rw [smul_mk', mk'_mul_cancel_left]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_right_comm : a ∆ b ∆ c = a ∆ c ∆ b

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a ∆ b ∆ c = a ∆ c ∆ b

Tactic:
simp_rw [symmDiff_assoc, symmDiff_comm]

Result:
no goals
-- Mathlib/Analysis/Complex/Angle.lean
@[simp] lemma angle_mul_left (ha : a ≠ 0) (x y : ℂ) : angle (a * x) (a * y) = angle x y

Proof state:
a : ℂ
ha : a ≠ 0
x y : ℂ
⊢ angle (a * x) (a * y) = angle x y

Tactic:
obtain rfl | hx := eq_or_ne x 0 <;> obtain rfl | hy := eq_or_ne y 0 <;>
  simp [angle_eq_abs_arg, mul_div_mul_left, *]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem uniformity_basis_dist :
    (𝓤 α).HasBasis (fun ε : ℝ => 0 < ε) fun ε => { p : α × α | dist p.1 p.2 < ε }

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ (𝓤 α).HasBasis (fun ε => 0 < ε) fun ε => {p | dist p.1 p.2 < ε}

Tactic:
exact UniformSpace.hasBasis_ofFun (exists_gt _) _ _ _ _ _

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem dropn_nil (n) : drop (nil : WSeq α) n = nil

Proof state:
α : Type u
n : ℕ
⊢ nil.drop n = nil

Tactic:
induction n <;> simp [*, drop]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem length_toList {t : Ordnode α} (h : Sized t) : (toList t).length = t.size

Proof state:
α : Type u_1
t : Ordnode α
h : t.Sized
⊢ t.toList.length = t.size

Tactic:
rw [length_toList', size_eq_realSize h]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem comp_hom_eq_id (α : X ≅ Y) {f : Y ⟶ X} : f ≫ α.hom = 𝟙 Y ↔ f = α.inv

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Y ⟶ X
⊢ f ≫ α.hom = 𝟙 Y ↔ f = α.inv

Tactic:
rw [← eq_comp_inv, id_comp]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/EpiMono.lean
theorem mono_iff_ker_eq_bot : Mono f ↔ LinearMap.ker f.hom = ⊥ :=
  ⟨fun _ => ker_eq_bot_of_mono _, fun hf =>
    ConcreteCategory.mono_of_injective _ <| by convert LinearMap.ker_eq_bot.1 hf⟩

Proof state:
R : Type u
inst✝ : Ring R
X Y : ModuleCat R
f : X ⟶ Y
hf : LinearMap.ker (Hom.hom f) = ⊥
⊢ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
convert LinearMap.ker_eq_bot.1 hf

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
lemma levyProkhorovDist_self (μ : Measure Ω) :
    levyProkhorovDist μ μ = 0

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ : Measure Ω
⊢ levyProkhorovDist μ μ = 0

Tactic:
simp only [levyProkhorovDist, levyProkhorovEDist_self, zero_toReal]

Result:
no goals
-- Mathlib/Data/Finset/Filter.lean
theorem filter_const (p : Prop) [Decidable p] (s : Finset α) :
    (s.filter fun _a => p) = if p then s else ∅

Proof state:
α : Type u_1
p : Prop
inst✝ : Decidable p
s : Finset α
⊢ filter (fun _a => p) s = if p then s else ∅

Tactic:
split_ifs <;> simp [*]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
theorem arrow_mk_iso_iff
    (P : AffineTargetMorphismProperty) [P.toProperty.RespectsIso]
    {X Y X' Y' : Scheme} {f : X ⟶ Y} {f' : X' ⟶ Y'}
    (e : Arrow.mk f ≅ Arrow.mk f') {h : IsAffine Y} :
    letI : IsAffine Y' := isAffine_of_isIso (Y := Y) e.inv.right
    P f ↔ P f'

Proof state:
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y X' Y' : Scheme
f : X ⟶ Y
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
h : IsAffine Y
⊢ P f ↔ P f'

Tactic:
rw [← P.toProperty_apply, ← P.toProperty_apply, P.toProperty.arrow_mk_iso_iff e]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem root_right_of_root_gcd [CommSemiring k] [DecidableEq R] {ϕ : R →+* k} {f g : R[X]} {α : k}
    (hα : (EuclideanDomain.gcd f g).eval₂ ϕ α = 0) : g.eval₂ ϕ α = 0

Proof state:
R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
⊢ eval₂ ϕ α g = 0

Tactic:
obtain ⟨p, hp⟩ := EuclideanDomain.gcd_dvd_right f g

Result:
case intro
R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : g = EuclideanDomain.gcd f g * p
⊢ eval₂ ϕ α g = 0

Proof state:
case intro
R : Type u
k : Type y
inst✝² : Field R
inst✝¹ : CommSemiring k
inst✝ : DecidableEq R
ϕ : R →+* k
f g : R[X]
α : k
hα : eval₂ ϕ α (EuclideanDomain.gcd f g) = 0
p : R[X]
hp : g = EuclideanDomain.gcd f g * p
⊢ eval₂ ϕ α g = 0

Tactic:
rw [hp, Polynomial.eval₂_mul, hα, zero_mul]

Result:
no goals
-- Mathlib/Algebra/Algebra/Tower.lean
theorem _root_.AlgHom.map_algebraMap (f : A →ₐ[S] B) (r : R) :
    f (algebraMap R A r) = algebraMap R B r

Proof state:
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra S B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
r : R
⊢ f ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
rw [algebraMap_apply R S A r, f.commutes, ← algebraMap_apply R S B]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
/-- A diagonal matrix is positive semidefinite iff its diagonal entries are nonnegative. -/
lemma posSemidef_diagonal_iff [StarOrderedRing R] [DecidableEq n] {d : n → R} :
    PosSemidef (diagonal d) ↔ (∀ i : n, 0 ≤ d i) :=
  ⟨fun ⟨_, hP⟩ i ↦ by simpa using hP (Pi.single i 1), .diagonal⟩

Proof state:
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : DecidableEq n
d : n → R
x✝ : (diagonal d).PosSemidef
i : n
left✝ : (diagonal d).IsHermitian
hP : ∀ (x : n → R), 0 ≤ star x ⬝ᵥ diagonal d *ᵥ x
⊢ 0 ≤ d i

Tactic:
simpa using hP (Pi.single i 1)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem isLeft_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
    isLeft (x.map f g) = isLeft x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
x : α ⊕ γ
⊢ (Sum.map f g x).isLeft = x.isLeft

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem HasSum.mul_left (a₂) (h : HasSum f a₁) : HasSum (fun i ↦ a₂ * f i) (a₂ * a₁)

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : HasSum f a₁
⊢ HasSum (fun i => a₂ * f i) (a₂ * a₁)

Tactic:
simpa only using h.map (AddMonoidHom.mulLeft a₂) (continuous_const.mul continuous_id)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem insert_of_not_mem {l : List α} (h : a ∉ l) : l.insert a = a :: l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : ¬a ∈ l
⊢ List.insert a l = a :: l

Tactic:
simp [List.insert, h]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem toNonUnitalSubring_injective {R : Type u} {A : Type v} [CommRing R] [NonUnitalRing A]
    [Module R A] [Star A] :
    Function.Injective (toNonUnitalSubring : NonUnitalStarSubalgebra R A → NonUnitalSubring A) :=
  fun S T h => ext fun x => by rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]

Proof state:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : NonUnitalRing A
inst✝¹ : Module R A
inst✝ : Star A
S T : NonUnitalStarSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toNonUnitalSubring, ← mem_toNonUnitalSubring, h]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem measurableSet_bot_iff {s : Set α} : MeasurableSet[⊥] s ↔ s = ∅ ∨ s = univ :=
  let b : MeasurableSpace α :=
    { MeasurableSet' := fun s => s = ∅ ∨ s = univ
      measurableSet_empty := Or.inl rfl
      measurableSet_compl

Proof state:
α : Type u_1
s : Set α
⊢ ∀ (s : Set α), (fun s => s = ∅ ∨ s = univ) s → (fun s => s = ∅ ∨ s = univ) sᶜ

Tactic:
simp +contextual [or_imp]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem ball_one_div_singleton : ball 1 δ / {x} = ball x⁻¹ δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ ball 1 δ / {x} = ball x⁻¹ δ

Tactic:
rw [ball_div_singleton, one_div]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
lemma rootForm_symmetric :
    LinearMap.IsSymm P.RootForm

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
⊢ LinearMap.IsSymm P.RootForm

Tactic:
simp [LinearMap.IsSymm, mul_comm, rootForm_apply_apply]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem nndist_one_left (a : E) : nndist 1 a = ‖a‖₊

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ nndist 1 a = ‖a‖₊

Tactic:
simp [nndist_eq_nnnorm_div]

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem d_eq_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) :
    φ P.d = φ P.a * -(x * y * z)

Proof state:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.d = φ P.a * -(x * y * z)

Tactic:
injection eq_sum_three_roots ha h3

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
lemma ofCauchy_div (f g) : (⟨f / g⟩ : ℝ) = (⟨f⟩ : ℝ) / (⟨g⟩ : ℝ)

Proof state:
f g : Cauchy abs
⊢ { cauchy := f / g } = { cauchy := f } / { cauchy := g }

Tactic:
simp_rw [div_eq_mul_inv, ofCauchy_mul, ofCauchy_inv]

Result:
no goals
-- Mathlib/Algebra/Vertex/HVertexOperator.lean
theorem coeff_comp (g : Γ' ×ₗ Γ) :
    (comp A B).coeff g = A.coeff (ofLex g).2 ∘ₗ B.coeff (ofLex g).1

Proof state:
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : OrderedCancelAddCommMonoid Γ
inst✝⁷ : OrderedCancelAddCommMonoid Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
g : Lex (Γ' × Γ)
⊢ (A.comp B).coeff g = A.coeff (ofLex g).2 ∘ₗ B.coeff (ofLex g).1

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
@[simp] lemma expect_dite_eq' (i : ι) (f : ∀ j, j = i → M) :
    𝔼 j ∈ s, (if h : j = i 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 : ι) → j = i → M
⊢ (𝔼 j ∈ s, if h : j = i 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/Asymptotics/Theta.lean
theorem IsTheta.isBoundedUnder_le_iff (h : f' =Θ[l] g') :
    IsBoundedUnder (· ≤ ·) l (norm ∘ f') ↔ IsBoundedUnder (· ≤ ·) l (norm ∘ g')

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
h : f' =Θ[l] g'
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f') ↔ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ g')

Tactic:
simp only [← isBigO_const_of_ne (one_ne_zero' ℝ), h.isBigO_congr_left]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_lt_top {x : ℝ≥0∞} : x⁻¹ < ∞ ↔ 0 < x

Proof state:
x : ℝ≥0∞
⊢ x⁻¹ < ⊤ ↔ 0 < x

Tactic:
simp only [lt_top_iff_ne_top, inv_ne_top, pos_iff_ne_zero]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_id (s : Set α) : id '' s = s

Proof state:
α : Type u_1
s : Set α
⊢ id '' s = s

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/PrimeFin.lean
lemma mem_primeFactors_of_ne_zero (hn : n ≠ 0) : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n

Proof state:
n p : ℕ
hn : n ≠ 0
⊢ p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n

Tactic:
simp [hn]

Result:
no goals
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_eq_zero_iff (hs : s.Finite) : uniformOn s t = 0 ↔ s ∩ t = ∅

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
⊢ (uniformOn s) t = 0 ↔ s ∩ t = ∅

Tactic:
simp [uniformOn, cond_apply hs.measurableSet, Measure.count_apply_eq_top, Set.not_infinite.2 hs,
  Measure.count_apply_finite _ (hs.inter_of_left _)]

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem frontier_setOf_le_im (a : ℝ) : frontier { z : ℂ | a ≤ z.im } = { z | z.im = a }

Proof state:
a : ℝ
⊢ frontier {z | a ≤ z.im} = {z | z.im = a}

Tactic:
simpa only [frontier_Ici] using frontier_preimage_im (Ici a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_ofFn (f : Fin n → α) : (ofFn f).size = n

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
⊢ (ofFn f).size = n

Tactic:
simp [ofFn]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/AbelianImages.lean
theorem PreservesCoimage.iso_hom_π :
    F.map (Abelian.coimage.π f) ≫ (PreservesCoimage.iso F f).hom = Abelian.coimage.π (F.map f)

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasKernels C
inst✝⁷ : HasCokernels C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
inst✝⁴ : HasKernels D
inst✝³ : HasCokernels D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair F
inst✝ : PreservesColimitsOfShape WalkingParallelPair F
X Y : C
f : X ⟶ Y
⊢ F.map (coimage.π f) ≫ (iso F f).hom = coimage.π (F.map f)

Tactic:
simp [iso]

Result:
no goals
-- Mathlib/Data/Nat/Basic.lean
@[simp] protected lemma pow_le_one_iff (hn : n ≠ 0) : a ^ n ≤ 1 ↔ a ≤ 1

Proof state:
a n : ℕ
hn : n ≠ 0
⊢ a ^ n ≤ 1 ↔ a ≤ 1

Tactic:
rw [← not_lt, one_lt_pow_iff hn, not_lt]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/MapDomain.lean
theorem mapDomain_one {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [Zero α] [Zero α₂]
    {F : Type*} [FunLike F α α₂] [ZeroHomClass F α α₂] (f : F) :
    (mapDomain f (1 : AddMonoidAlgebra β α) : AddMonoidAlgebra β α₂) =
      (1 : AddMonoidAlgebra β α₂)

Proof state:
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : Zero α
inst✝² : Zero α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
inst✝ : ZeroHomClass F α α₂
f : F
⊢ mapDomain (⇑f) 1 = 1

Tactic:
simp_rw [one_def, mapDomain_single, map_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem toList_unattach {p : α → Prop} {l : Array { x // p x }} :
    l.unattach.toList = l.toList.unattach

Proof state:
α : Type u_1
p : α → Prop
l : Array { x // p x }
⊢ l.unattach.toList = l.toList.unattach

Tactic:
simp [unattach]

Result:
no goals
-- Mathlib/Data/Matrix/Basic.lean
@[simp] lemma entryLinearMap_comp_mapMatrix (f : α ≃ₗ[R] β) (i : m) (j : n) :
    entryLinearMap R _ i j ∘ₗ f.mapMatrix.toLinearMap =
      f.toLinearMap ∘ₗ entryLinearMap R _ i j

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
β : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid α
inst✝² : AddCommMonoid β
inst✝¹ : Module R α
inst✝ : Module R β
f : α ≃ₗ[R] β
i : m
j : n
⊢ entryLinearMap R β i j ∘ₗ ↑f.mapMatrix = ↑f ∘ₗ entryLinearMap R α i j

Tactic:
simp only [mapMatrix_toLinearMap, LinearMap.entryLinearMap_comp_mapMatrix]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
theorem _root_.Filter.EventuallyEq.mlieBracket_vectorField_eq
    (hV : V₁ =ᶠ[𝓝 x] V) (hW : W₁ =ᶠ[𝓝 x] W) :
    mlieBracket I V₁ W₁ x = mlieBracket I V W x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁴ : TopologicalSpace H
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
V W V₁ W₁ : (x : M) → TangentSpace I x
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
⊢ mlieBracket I V₁ W₁ x = mlieBracket I V W x

Tactic:
rw [← mlieBracketWithin_univ, ← mlieBracketWithin_univ,
  hV.mlieBracketWithin_vectorField_eq_nhds hW]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem orthogonal_disjoint : Disjoint K Kᗮ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ Disjoint K Kᗮ

Tactic:
simp [disjoint_iff, K.inf_orthogonal_eq_bot]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.tendsto_right_iff (hlb : lb.HasBasis pb sb) :
    Tendsto f la lb ↔ ∀ i, pb i → ∀ᶠ x in la, f x ∈ sb i

Proof state:
α : Type u_1
β : Type u_2
ι' : Sort u_5
la : Filter α
lb : Filter β
pb : ι' → Prop
sb : ι' → Set β
f : α → β
hlb : lb.HasBasis pb sb
⊢ Tendsto f la lb ↔ ∀ (i : ι'), pb i → ∀ᶠ (x : α) in la, f x ∈ sb i

Tactic:
simp only [Tendsto, hlb.ge_iff, mem_map', Filter.Eventually]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem unattach_replicate {p : α → Prop} {n : Nat} {x : { x // p x }} :
    (List.replicate n x).unattach = List.replicate n x.1

Proof state:
α : Type u_1
p : α → Prop
n : Nat
x : { x // p x }
⊢ (replicate n x).unattach = replicate n x.val

Tactic:
simp [unattach, -map_subtype]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_ite_eq_of_mem [DecidableEq α] (s : Finset α) (a : α) (b : α → β) (h : a ∈ s) :
    (∏ x ∈ s, if a = x then b x else 1) = b a

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
a : α
b : α → β
h : a ∈ s
⊢ (∏ x ∈ s, if a = x then b x else 1) = b a

Tactic:
simp only [prod_ite_eq, if_pos h]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem _root_.Matrix.posSemidef_intCast_iff
    [StarOrderedRing R] [DecidableEq n] [Nonempty n] [Nontrivial R] (d : ℤ) :
    PosSemidef (d : Matrix n n R) ↔ 0 ≤ d :=
  posSemidef_diagonal_iff.trans <| by simp [Pi.le_def]

Proof state:
n : Type u_2
R : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : DecidableEq n
inst✝¹ : Nonempty n
inst✝ : Nontrivial R
d : ℤ
⊢ n → 0 ≤ ↑d ↔ 0 ≤ d

Tactic:
simp [Pi.le_def]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem ext_getElem! [Inhabited α] (hl : length l₁ = length l₂) (h : ∀ n : ℕ, l₁[n]! = l₂[n]!) :
    l₁ = l₂ :=
  ext_getElem hl fun n h₁ h₂ ↦ by simpa only [← getElem!_pos] using h n

Proof state:
α : Type u
l₁ l₂ : List α
inst✝ : Inhabited α
hl : l₁.length = l₂.length
h : ∀ (n : ℕ), l₁[n]! = l₂[n]!
n : ℕ
h₁ : n < l₁.length
h₂ : n < l₂.length
⊢ l₁[n] = l₂[n]

Tactic:
simpa only [← getElem!_pos] using h n

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Control/Lawful/MonadLift.lean
theorem monadLift_seqRight [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) :
    monadLift (x *> y) = (monadLift x : n α) *> (monadLift y : n β)

Proof state:
m : Type u_1 → Type u_2
n : Type u_1 → Type u_3
inst✝⁵ : Monad m
inst✝⁴ : Monad n
inst✝³ : MonadLiftT m n
inst✝² : LawfulMonadLiftT m n
α β : Type u_1
inst✝¹ : LawfulMonad m
inst✝ : LawfulMonad n
x : m α
y : m β
⊢ monadLift (x *> y) = monadLift x *> monadLift y

Tactic:
simp only [seqRight_eq, monadLift_map, monadLift_seq]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_mul_const_Ico_of_neg (a b : α) {c : α} (h : c < 0) :
    (fun x => x * c) ⁻¹' Ico a b = Ioc (b / c) (a / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : c < 0
⊢ (fun x => x * c) ⁻¹' Ico a b = Ioc (b / c) (a / c)

Tactic:
simp [← Ici_inter_Iio, ← Ioi_inter_Iic, h, inter_comm]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem head?_rotate {l : List α} {n : ℕ} (h : n < l.length) : head? (l.rotate n) = l[n]?

Proof state:
α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ (l.rotate n).head? = l[n]?

Tactic:
rw [head?_eq_getElem?, getElem?_rotate (n.zero_le.trans_lt h), Nat.zero_add, Nat.mod_eq_of_lt h]

Result:
no goals
-- Mathlib/Order/Filter/FilterProduct.lean
theorem const_max [LinearOrder β] (x y : β) : (↑(max x y : β) : β*) = max ↑x ↑y

Proof state:
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrder β
x y : β
⊢ ↑(x ⊔ y) = ↑x ⊔ ↑y

Tactic:
rw [max_def, map₂_const]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem quot_out [Monoid M] (a : Associates M) : Associates.mk (Quot.out a) = a

Proof state:
M : Type u_1
inst✝ : Monoid M
a : Associates M
⊢ Associates.mk (Quot.out a) = a

Tactic:
rw [← quot_mk_eq_mk, Quot.out_eq]

Result:
no goals
-- Mathlib/Algebra/Homology/Localization.lean
lemma mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso :
    (HomologicalComplex.quasiIso C c).IsInvertedBy
      (F.mapHomologicalComplex c ⋙ HomologicalComplexUpToQuasiIso.Q)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_6, u_2} D
F : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : CategoryWithHomology C
inst✝³ : CategoryWithHomology D
inst✝² : (HomologicalComplex.quasiIso D c).HasLocalization
inst✝¹ : F.Additive
inst✝ : F.PreservesHomology
⊢ (HomologicalComplex.quasiIso C c).IsInvertedBy (F.mapHomologicalComplex c ⋙ HomologicalComplexUpToQuasiIso.Q)

Tactic:
apply (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism c).inverts

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Quotient.lean
theorem _root_.QuotientGroup.out_conj_pow_minimalPeriod_mem (a : α) (q : α ⧸ H) :
    q.out⁻¹ * a ^ Function.minimalPeriod (a • ·) q * q.out ∈ H

Proof state:
α : Type u
inst✝ : Group α
H : Subgroup α
a : α
q : α ⧸ H
⊢ (Quotient.out q)⁻¹ * a ^ minimalPeriod (fun x => a • x) q * Quotient.out q ∈ H

Tactic:
rw [mul_assoc, ← QuotientGroup.eq, QuotientGroup.out_eq', ← smul_eq_mul, Quotient.mk_smul_out,
  eq_comm, pow_smul_eq_iff_minimalPeriod_dvd]

Result:
no goals