harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
theorem comp_ι_sq_zero (g : ExteriorAlgebra R M →ₐ[R] A) (m : M) : g (ι R m) * g (ι R m) = 0

Proof state:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : ExteriorAlgebra R M →ₐ[R] A
m : M
⊢ g ((ι R) m) * g ((ι R) m) = 0

Tactic:
rw [← map_mul, ι_sq_zero, map_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem all_zero {f : (i : Nat) → i < 0 → Bool} : all 0 f = true

Proof state:
f : (i : Nat) → i < 0 → Bool
⊢ all 0 f = true

Tactic:
simp [all]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem piecewise_empty (f g : α →ₛ β) : piecewise ∅ MeasurableSet.empty f g = g :=
  coe_injective <| by simp

Proof state:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
f g : α →ₛ β
⊢ ⇑(piecewise ∅ ⋯ f g) = ⇑g

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_div_mul_left_eq_div (a b c : G) : c * a / (c * b) = a / b

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

Tactic:
rw [div_eq_mul_inv, mul_inv_rev, mul_comm b⁻¹ c⁻¹, mul_comm c a, mul_assoc, ← mul_assoc c,
  mul_inv_cancel, one_mul, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem vecMulVec_eq [Mul α] [AddCommMonoid α] [Unique ι] (w : m → α) (v : n → α) :
    vecMulVec w v = col ι w * row ι v

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝² : Mul α
inst✝¹ : AddCommMonoid α
inst✝ : Unique ι
w : m → α
v : n → α
i✝ : m
j✝ : n
⊢ vecMulVec w v i✝ j✝ = (col ι w * row ι v) i✝ j✝

Tactic:
simp [vecMulVec, mul_apply]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝² : Mul α
inst✝¹ : AddCommMonoid α
inst✝ : Unique ι
w : m → α
v : n → α
⊢ vecMulVec w v = col ι w * row ι v

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝² : Mul α
inst✝¹ : AddCommMonoid α
inst✝ : Unique ι
w : m → α
v : n → α
i✝ : m
j✝ : n
⊢ vecMulVec w v i✝ j✝ = (col ι w * row ι v) i✝ j✝
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem ball_div_singleton : ball x δ / {y} = ball (x / y) δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ ball x δ / {y} = ball (x / y) δ

Tactic:
simp_rw [div_eq_mul_inv, inv_singleton, ball_mul_singleton]

Result:
no goals
-- Mathlib/Data/Multiset/Basic.lean
theorem empty_toList {s : Multiset α} : s.toList.isEmpty ↔ s = 0

Proof state:
α : Type u_1
s : Multiset α
⊢ s.toList.isEmpty = true ↔ s = 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Flag.lean
theorem flag_le_ker_dual (b : Basis (Fin n) R M) (k : Fin n) :
    b.flag k.castSucc ≤ LinearMap.ker (b.dualBasis k)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
⊢ b.flag k.castSucc ≤ LinearMap.ker (b.dualBasis k)

Tactic:
nontriviality R

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
a✝ : Nontrivial R
⊢ b.flag k.castSucc ≤ LinearMap.ker (b.dualBasis k)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
k : Fin n
a✝ : Nontrivial R
⊢ b.flag k.castSucc ≤ LinearMap.ker (b.dualBasis k)

Tactic:
rw [coe_dualBasis, b.flag_le_ker_coord_iff]

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem inl_mul_inr [Semiring R] [AddCommMonoid M] [Module R M] [Module Rᵐᵒᵖ M] (r : R) (m : M) :
    (inl r * inr m : tsze R M) = inr (r • m) :=
  ext (mul_zero r) <|
    show r • m + (0 : Rᵐᵒᵖ) • (0 : M) = r • m by rw [smul_zero, add_zero]

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
r : R
m : M
⊢ r •> m + 0 •> 0 = r •> m

Tactic:
rw [smul_zero, add_zero]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_top' : a ∆ ⊤ = ￢a

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ a ∆ ⊤ = ￢a

Tactic:
simp [symmDiff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
@[simp]
lemma Hom.id_eq (X : WalkingReflexivePair) :
    Hom.id X = 𝟙 X

Proof state:
X : WalkingReflexivePair
⊢ id X = 𝟙 X

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem ker_eq_bot_iff (f : G →* M) : f.ker = ⊥ ↔ Function.Injective f :=
  ⟨fun h x y hxy => by rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy, fun h =>
    bot_unique fun _ hx => h (hx.trans f.map_one.symm)⟩

Proof state:
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
h : f.ker = ⊥
x y : G
hxy : f x = f y
⊢ x = y

Tactic:
rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
    (hl : DistinctKeys l) : containsKey a (eraseKey k l) = (!(k == a) && containsKey a l)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
⊢ containsKey a (eraseKey k l) = (!k == a && containsKey a l)

Tactic:
simp [containsKey_eq_isSome_getEntry?, getEntry?_eraseKey hl, apply_ite]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isSuffixOf_replicate {a : α} :
    isSuffixOf l (replicate n a) = (decide (l.length ≤ n) && l.all (· == a))

Proof state:
α : Type u_1
inst✝ : BEq α
l : List α
n : Nat
a : α
⊢ l.isSuffixOf (replicate n a) = (decide (l.length ≤ n) && l.all fun x => x == a)

Tactic:
simp [isSuffixOf, all_eq]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem prod_def {f : Filter α} {g : Filter β} :
    f ×ˢ g = f.lift fun s => g.lift' fun t => s ×ˢ t

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = f.lift fun s => g.lift' fun t => s ×ˢ t

Tactic:
simpa only [Filter.lift', Filter.lift, (f.basis_sets.prod g.basis_sets).eq_biInf,
  iInf_prod, iInf_and] using iInf_congr fun i => iInf_comm

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem fractionalIdealLatticeBasis_apply (i : ChooseBasisIndex ℤ I) :
    fractionalIdealLatticeBasis K I i = (mixedEmbedding K) (basisOfFractionalIdeal K I i)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
i : ChooseBasisIndex ℤ ↥↑↑I
⊢ (fractionalIdealLatticeBasis K I) i = (mixedEmbedding K) ((basisOfFractionalIdeal K I) i)

Tactic:
simp only [fractionalIdealLatticeBasis, Basis.coe_reindex, Basis.coe_mk, Function.comp_apply,
  Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem sign (h : IsThreeCycle σ) : sign σ = 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ Perm.sign σ = 1

Tactic:
rw [Equiv.Perm.sign_of_cycleType, h.cycleType]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ (-1) ^ ({3}.sum + {3}.card) = 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ (-1) ^ ({3}.sum + {3}.card) = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem intCast_def' (z : ℤ) : (z : A ⊗[R] B) = (1 : A) ⊗ₜ (z : B)

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
z : ℤ
⊢ ↑z = 1 ⊗ₜ[R] ↑z

Tactic:
rw [intCast_def, ← zsmul_one, smul_tmul, zsmul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Raw.lean
theorem WF.insertMany [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {m : Raw α β}
    {l : ρ} (h : m.WF) : (m.insertMany l).WF

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
ρ : Type w
inst✝ : ForIn Id ρ ((a : α) × β a)
m : Raw α β
l : ρ
h : m.WF
⊢ (m.insertMany l).WF

Tactic:
simpa [Raw.insertMany, h.size_buckets_pos] using
  (Raw₀.insertMany ⟨m, h.size_buckets_pos⟩ l).2 _ WF.insert₀ h

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem ofMulEquivOfLocalizations_comp {k : N ≃* P} {j : P ≃* Q} :
    (f.ofMulEquivOfLocalizations (k.trans j)).toMap =
      j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMap

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
Q : Type u_4
inst✝ : CommMonoid Q
k : N ≃* P
j : P ≃* Q
⊢ (f.ofMulEquivOfLocalizations (k.trans j)).toMap = j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMap

Tactic:
ext

Result:
case h
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
Q : Type u_4
inst✝ : CommMonoid Q
k : N ≃* P
j : P ≃* Q
x✝ : M
⊢ (f.ofMulEquivOfLocalizations (k.trans j)).toMap x✝ = (j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMap) x✝

Proof state:
case h
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
Q : Type u_4
inst✝ : CommMonoid Q
k : N ≃* P
j : P ≃* Q
x✝ : M
⊢ (f.ofMulEquivOfLocalizations (k.trans j)).toMap x✝ = (j.toMonoidHom.comp (f.ofMulEquivOfLocalizations k).toMap) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem neg_one_mul (a : α) : -1 * a = -a

Proof state:
α : Type u
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ -1 * a = -a

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem norm_le (C0 : (0 : ℝ) ≤ C) : ‖f‖ ≤ C ↔ ∀ x : α, ‖f x‖ ≤ C

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
C : ℝ
C0 : 0 ≤ C
⊢ ‖f‖ ≤ C ↔ ∀ (x : α), ‖f x‖ ≤ C

Tactic:
simpa using @dist_le _ _ _ _ f 0 _ C0

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem smul_mem [Monoid R] [DistribMulAction R A] [StarModule R A] (r : R) {x : A}
    (h : x ∈ skewAdjoint A) : r • x ∈ skewAdjoint A

Proof state:
R : Type u_1
A : Type u_2
inst✝⁶ : Star R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : Monoid R
inst✝¹ : DistribMulAction R A
inst✝ : StarModule R A
r : R
x : A
h : x ∈ skewAdjoint A
⊢ r • x ∈ skewAdjoint A

Tactic:
rw [mem_iff, star_smul, star_trivial, mem_iff.mp h, smul_neg r]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_apply' (hs : MeasurableSet s) : μ.restrict s t = μ (t ∩ s)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ (μ.restrict s) t = μ (t ∩ s)

Tactic:
rw [← toOuterMeasure_apply,
  Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict hs,
  OuterMeasure.restrict_apply s t _, toOuterMeasure_apply]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem foldr_fixed' {f : α → β → β} {b : β} (hf : ∀ a, f a b = b) : ∀ l : List α, foldr f b l = b
  | [] => rfl
  | a :: l => by rw [foldr_cons, foldr_fixed' hf l, hf a]

Proof state:
α : Type u
β : Type v
f : α → β → β
b : β
hf : ∀ (a : α), f a b = b
a : α
l : List α
⊢ foldr f b (a :: l) = b

Tactic:
rw [foldr_cons, foldr_fixed' hf l, hf a]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem eval₂Hom_bind₁ (f : R →+* S) (g : τ → S) (h : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
    eval₂Hom f g (bind₁ h φ) = eval₂Hom f (fun i => eval₂Hom f g (h i)) φ

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : τ → S
h : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ (eval₂Hom f g) ((bind₁ h) φ) = (eval₂Hom f fun i => (eval₂Hom f g) (h i)) φ

Tactic:
rw [hom_bind₁, eval₂Hom_comp_C]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
lemma Topology.isInducing_sigmaMap {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)}
    (h₁ : Injective f₁) : IsInducing (Sigma.map f₁ f₂) ↔ ∀ i, IsInducing (f₂ i)

Proof state:
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h₁ : Injective f₁
⊢ IsInducing (Sigma.map f₁ f₂) ↔ ∀ (i : ι), IsInducing (f₂ i)

Tactic:
simp only [isInducing_iff_nhds, Sigma.forall, Sigma.nhds_mk, Sigma.map_mk,
  ← map_sigma_mk_comap h₁, map_inj sigma_mk_injective]

Result:
no goals
-- Mathlib/Topology/Connected/Clopen.lean
theorem nonempty_inter [PreconnectedSpace α] {s t : Set α} :
    IsOpen s → IsOpen t → s ∪ t = univ → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s t : Set α
⊢ IsOpen s → IsOpen t → s ∪ t = univ → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty

Tactic:
simpa only [univ_inter, univ_subset_iff] using @PreconnectedSpace.isPreconnected_univ α _ _ s t

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem mem_inter_iff [BEq α] [LawfulBEq α] {x : α} {l₁ l₂ : List α} :
    x ∈ l₁ ∩ l₂ ↔ x ∈ l₁ ∧ x ∈ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
l₁ l₂ : List α
⊢ x ∈ l₁ ∩ l₂ ↔ x ∈ l₁ ∧ x ∈ l₂

Tactic:
cases l₁ <;> simp [List.inter_def, mem_filter]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
theorem Trident.condition (j₁ j₂ : J) (t : Trident f) : t.ι ≫ f j₁ = t.ι ≫ f j₂

Proof state:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Trident f
⊢ t.ι ≫ f j₁ = t.ι ≫ f j₂

Tactic:
rw [t.app_zero, t.app_zero]

Result:
no goals
-- Mathlib/Tactic/NormNum/OfScientific.lean
theorem isRat_ofScientific_of_true [DivisionRing α] :
    {m e : ℕ} → {n : ℤ} → {d : ℕ} →
    IsRat (mkRat m (10 ^ e) : α) n d → IsRat (OfScientific.ofScientific m true e : α) n d
  | _, _, _, _, ⟨_, eq⟩ => ⟨‹_›, by
    rwa [← Rat.cast_ofScientific, ← Rat.ofScientific_eq_ofScientific, Rat.ofScientific_true_def]⟩

Proof state:
α : Type u_1
inst✝ : DivisionRing α
x✝¹ x✝ : ℕ
num✝ : ℤ
denom✝ : ℕ
inv✝ : Invertible ↑denom✝
eq : ↑(mkRat (↑x✝¹) (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
⊢ OfScientific.ofScientific x✝¹ true x✝ = ↑num✝ * ⅟↑denom✝

Tactic:
rwa [← Rat.cast_ofScientific, ← Rat.ofScientific_eq_ofScientific, Rat.ofScientific_true_def]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem mul_lt_iff_lt_one_right' [MulRightStrictMono α]
    [MulRightReflectLT α] {a : α} (b : α) : a * b < b ↔ a < 1 :=
  Iff.trans (by rw [one_mul]) (mul_lt_mul_iff_right b)

Proof state:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : MulRightStrictMono α
inst✝ : MulRightReflectLT α
a b : α
⊢ a * b < b ↔ a * b < 1 * b

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem d_of_eq (h : P.toPoly = Q.toPoly) : P.d = Q.d

Proof state:
R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ P.d = Q.d

Tactic:
rw [← coeff_eq_d, h, coeff_eq_d]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem one_coeff_eq_of_pos (n : ℕ) (hn : 0 < n) : coeff (1 : 𝕎 R) n = 0 :=
  show (aeval _ (wittOne p n) : R) = 0 by simp only [hn, wittOne_pos_eq_zero, map_zero]

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n : ℕ
hn : 0 < n
⊢ (aeval (Function.uncurry fun i => (![] i).coeff)) (wittOne p n) = 0

Tactic:
simp only [hn, wittOne_pos_eq_zero, map_zero]

Result:
no goals
-- Mathlib/ModelTheory/Basic.lean
theorem symm_comp_self_toEmbedding (f : M ≃[L] N) :
    f.symm.toEmbedding.comp f.toEmbedding = Embedding.refl L M

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃[L] N
⊢ f.symm.toEmbedding.comp f.toEmbedding = Embedding.refl L M

Tactic:
rw [← comp_toEmbedding, symm_comp_self, refl_toEmbedding]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_smul_real_left (x y : E) (r : ℝ) : ⟪(r : 𝕜) • x, y⟫ = r • ⟪x, y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
r : ℝ
⊢ ⟪↑r • x, y⟫_𝕜 = r • ⟪x, y⟫_𝕜

Tactic:
rw [inner_smul_left, conj_ofReal, Algebra.smul_def]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Restrict.lean
theorem AffineMap.restrict.linear_aux {φ : P₁ →ᵃ[k] P₂} {E : AffineSubspace k P₁}
    {F : AffineSubspace k P₂} (hEF : E.map φ ≤ F) : E.direction ≤ F.direction.comap φ.linear

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
⊢ E.direction ≤ Submodule.comap φ.linear F.direction

Tactic:
rw [← Submodule.map_le_iff_le_comap, ← AffineSubspace.map_direction]

Result:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
⊢ (AffineSubspace.map φ E).direction ≤ F.direction

Proof state:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
⊢ (AffineSubspace.map φ E).direction ≤ F.direction

Tactic:
exact AffineSubspace.direction_le hEF

Result:
no goals
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
/-- The residue of `ζ(s)` at `s = 1` is equal to 1. -/
lemma riemannZeta_residue_one : Tendsto (fun s ↦ (s - 1) * riemannZeta s) (𝓝[≠] 1) (𝓝 1)

Proof state:
⊢ Tendsto (fun s => (s - 1) * riemannZeta s) (𝓝[≠] 1) (𝓝 1)

Tactic:
exact hurwitzZetaEven_residue_one 0

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_mul_of_div_eq' (h : a / b = c) : a = b * c

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c : G
h : a / b = c
⊢ a = b * c

Tactic:
simp [h.symm]

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
/-- A small set of games is bounded below. -/
lemma bddBelow_of_small (s : Set Game.{u}) [Small.{u} s] : BddBelow s

Proof state:
s : Set Game
inst✝ : Small.{u, u + 1} ↑s
⊢ BddBelow s

Tactic:
simpa using bddBelow_range_of_small (Subtype.val : s → Game.{u})

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_liftAt_one {n m : ℕ} {φ : L.BoundedFormula α n} {v : α → M} {xs : Fin (n + 1) → M}
    (hmn : m ≤ n) :
    (φ.liftAt 1 m).Realize v xs ↔
      φ.Realize v (xs ∘ fun i => if ↑i < m then castSucc i else i.succ)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n m : ℕ
φ : L.BoundedFormula α n
v : α → M
xs : Fin (n + 1) → M
hmn : m ≤ n
⊢ (liftAt 1 m φ).Realize v xs ↔ φ.Realize v (xs ∘ fun i => if ↑i < m then i.castSucc else i.succ)

Tactic:
simp [realize_liftAt (add_le_add_right hmn 1), castSucc]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_succ_left (n : ℕ) :
    descPochhammer R (n + 1) = X * (descPochhammer R n).comp (X - 1)

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ descPochhammer R (n + 1) = X * (descPochhammer R n).comp (X - 1)

Tactic:
rw [descPochhammer]

Result:
no goals
-- Mathlib/Algebra/Group/Commute/Hom.lean
theorem SemiconjBy.map [MulHomClass F M N] (h : SemiconjBy a x y) (f : F) :
    SemiconjBy (f a) (f x) (f y)

Proof state:
F : Type u_1
M : Type u_2
N : Type u_3
inst✝³ : Mul M
inst✝² : Mul N
a x y : M
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
h : SemiconjBy a x y
f : F
⊢ SemiconjBy (f a) (f x) (f y)

Tactic:
simpa only [SemiconjBy, map_mul] using congr_arg f h

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem extend_one : γ.extend 1 = y

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ γ.extend 1 = y

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/EpsilonNFA.lean
theorem isPath_nil : M.IsPath s t [] ↔ s = t

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
⊢ M.IsPath s t [] ↔ s = t

Tactic:
rw [isPath_iff]

Result:
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
⊢ (t = s ∧ [] = [] ∨ ∃ t_1 a x, t_1 ∈ M.step s a ∧ M.IsPath t_1 t x ∧ [] = a :: x) ↔ s = t

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
s t : σ
⊢ (t = s ∧ [] = [] ∨ ∃ t_1 a x, t_1 ∈ M.step s a ∧ M.IsPath t_1 t x ∧ [] = a :: x) ↔ s = t

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem _root_.MeasureTheory.AEStronglyMeasurable.compProd_mk_left {δ : Type*} [TopologicalSpace δ]
    {f : β × γ → δ} (hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)) :
    ∀ᵐ x ∂κ a, AEStronglyMeasurable (fun y => f (x, y)) (η (a, x))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
δ : Type u_5
inst✝ : TopologicalSpace δ
f : β × γ → δ
hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ ∀ᵐ (x : β) ∂κ a, AEStronglyMeasurable (fun y => f (x, y)) (η (a, x))

Tactic:
filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with x hx using
  ⟨fun y => hf.mk f (x, y), hf.stronglyMeasurable_mk.comp_measurable measurable_prod_mk_left, hx⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem posSemidef_submatrix_equiv {M : Matrix n n R} (e : m ≃ n) :
    (M.submatrix e e).PosSemidef ↔ M.PosSemidef :=
  ⟨fun h => by simpa using h.submatrix e.symm, fun h => h.submatrix _⟩

Proof state:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
e : m ≃ n
h : (M.submatrix ⇑e ⇑e).PosSemidef
⊢ M.PosSemidef

Tactic:
simpa using h.submatrix e.symm

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma add_smul_of_not_equiv {P Q : Fin 3 → R} (h : ¬P ≈ Q) {u v : R} (hu : IsUnit u)
    (hv : IsUnit v) : W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : ¬P ≈ Q
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ W'.add (u • P) (v • Q) = (u * v) ^ 2 • W'.add P Q

Tactic:
rw [add_of_not_equiv <| h.comp (smul_equiv_smul P Q hu hv).mp, addXYZ_smul, add_of_not_equiv h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replace_cons_self [LawfulBEq α] {a : α} : (a::as).replace a b = b::as

Proof state:
α : Type u_1
inst✝¹ : BEq α
as : List α
b : α
inst✝ : LawfulBEq α
a : α
⊢ (a :: as).replace a b = b :: as

Tactic:
simp [replace_cons]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_add_mul_right_right (m n k : ℕ) : Coprime m (n + k * m) ↔ Coprime m n

Proof state:
m n k : ℕ
⊢ m.Coprime (n + k * m) ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_add_mul_right_right]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma polynomial_ne_zero [Nontrivial R] : W'.polynomial ≠ 0

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ { a := 0, b := 1, c := { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly,
        d := { a := -1, b := -W'.a₂, c := -W'.a₄, d := -W'.a₆ }.toPoly }.toPoly ≠
    0

Tactic:
exact Cubic.ne_zero_of_b_ne_zero one_ne_zero

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ W'.polynomial ≠ 0

Tactic:
rw [polynomial_eq]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ { a := 0, b := 1, c := { a := 0, b := 0, c := W'.a₁, d := W'.a₃ }.toPoly,
        d := { a := -1, b := -W'.a₂, c := -W'.a₄, d := -W'.a₆ }.toPoly }.toPoly ≠
    0
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma preNormEDS'_one : preNormEDS' b c d 1 = 1

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS' b c d 1 = 1

Tactic:
rw [preNormEDS']

Result:
no goals