harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/Embedding/TruncLE.lean
lemma truncLE'Map_f_eq {i : ι} (hi : ¬ e.BoundaryLE i) {i' : ι'} (h : e.f i = i') :
    (truncLE'Map φ e).f i =
      (K.truncLE'XIso e h hi).hom ≫ φ.f i' ≫ (L.truncLE'XIso e h hi).inv :=
  Quiver.Hom.op_inj
    (by simpa using truncGE'Map_f_eq ((opFunctor C c').map φ.op) e.op (by simpa) h)

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ ((truncLE'Map φ e).f i).op = ((K.truncLE'XIso e h hi).hom ≫ φ.f i' ≫ (L.truncLE'XIso e h hi).inv).op

Tactic:
simpa using truncGE'Map_f_eq ((opFunctor C c').map φ.op) e.op (by simpa) h

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ ¬e.op.BoundaryGE i

Tactic:
simpa

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderIso.lean
theorem preimage_Ici (e : α ≃o β) (b : β) : e ⁻¹' Ici b = Ici (e.symm b)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ⇑e ⁻¹' Ici b ↔ x ∈ Ici (e.symm b)

Tactic:
simp [← e.le_iff_le]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
⊢ ⇑e ⁻¹' Ici b = Ici (e.symm b)

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ⇑e ⁻¹' Ici b ↔ x ∈ Ici (e.symm b)
-- Mathlib/Probability/Kernel/Integral.lean
theorem setIntegral_deterministic' (hg : Measurable g)
    (hf : StronglyMeasurable f) {s : Set β} (hs : MeasurableSet s) [Decidable (g a ∈ s)] :
    ∫ x in s, f x ∂deterministic g hg a = if g a ∈ s then f (g a) else 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : β → E
a : α
inst✝¹ : CompleteSpace E
g : α → β
hg : Measurable g
hf : StronglyMeasurable f
s : Set β
hs : MeasurableSet s
inst✝ : Decidable (g a ∈ s)
⊢ ∫ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0

Tactic:
rw [deterministic_apply, setIntegral_dirac' hf _ hs]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/EverywherePos.lean
protected lemma _root_.IsCompact.everywherePosSubset (hs : IsCompact s) :
    IsCompact (μ.everywherePosSubset s)

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
u : Set α
u_open : IsOpen u
hu : μ.everywherePosSubset s = s \ u
⊢ IsCompact (μ.everywherePosSubset s)

Tactic:
rw [hu]

Result:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
u : Set α
u_open : IsOpen u
hu : μ.everywherePosSubset s = s \ u
⊢ IsCompact (s \ u)

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
u : Set α
u_open : IsOpen u
hu : μ.everywherePosSubset s = s \ u
⊢ IsCompact (s \ u)

Tactic:
exact hs.diff u_open

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
⊢ IsCompact (μ.everywherePosSubset s)

Tactic:
rcases exists_isOpen_everywherePosSubset_eq_diff μ s with ⟨u, u_open, hu⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsCompact s
u : Set α
u_open : IsOpen u
hu : μ.everywherePosSubset s = s \ u
⊢ IsCompact (μ.everywherePosSubset s)
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma ae_ae_of_ae_compProd [SFinite μ] [IsSFiniteKernel κ] {p : α × β → Prop}
    (h : ∀ᵐ x ∂(μ ⊗ₘ κ), p x) :
    ∀ᵐ a ∂μ, ∀ᵐ b ∂κ a, p (a, b)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
p : α × β → Prop
h : ∀ᵐ (x : α × β) ∂μ ⊗ₘ κ, p x
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)

Tactic:
convert Kernel.ae_ae_of_ae_compProd h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem cast_natAdd_zero {n n' : Nat} (i : Fin n) (h : 0 + n = n') :
    (natAdd 0 i).cast h = i.cast ((Nat.zero_add _).symm.trans h)

Proof state:
n n' : Nat
i : Fin n
h : 0 + n = n'
⊢ Fin.cast h (natAdd 0 i) = Fin.cast ⋯ i

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuousWithinAt_univ_iff :
    LowerSemicontinuousWithinAt f univ x ↔ LowerSemicontinuousAt f x

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_2
inst✝ : Preorder β
f : α → β
x : α
⊢ LowerSemicontinuousWithinAt f univ x ↔ LowerSemicontinuousAt f x

Tactic:
simp [LowerSemicontinuousWithinAt, LowerSemicontinuousAt, nhdsWithin_univ]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
/-- An auxiliary lemma en route to `RootPairing.finrank_corootSpan_eq`. -/
private lemma finrank_corootSpan_le :
    finrank R P.corootSpan ≤ finrank R P.rootSpan

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ finrank R ↥(Submodule.map P.Polarization P.rootSpan) ≤ finrank R ↥P.rootSpan

Tactic:
exact Submodule.finrank_map_le P.Polarization P.rootSpan

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ finrank R ↥P.corootSpan ≤ finrank R ↥P.rootSpan

Tactic:
rw [← finrank_rootSpan_map_polarization_eq_finrank_corootSpan]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ finrank R ↥(Submodule.map P.Polarization P.rootSpan) ≤ finrank R ↥P.rootSpan
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem cardQuot_mul_of_coprime
    {I J : Ideal S} (coprime : IsCoprime I J) : cardQuot (I * J) = cardQuot I * cardQuot J

Proof state:
S : Type u_1
inst✝ : CommRing S
I J : Ideal S
coprime : IsCoprime I J
⊢ cardQuot (I * J) = cardQuot I * cardQuot J

Tactic:
rw [cardQuot_apply, cardQuot_apply, cardQuot_apply,
  Nat.card_congr (Ideal.quotientMulEquivQuotientProd I J coprime).toEquiv,
  Nat.card_prod]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem ext_of_Ioc_finite {α : Type*} [TopologicalSpace α] {m : MeasurableSpace α}
    [SecondCountableTopology α] [LinearOrder α] [OrderTopology α] [BorelSpace α] (μ ν : Measure α)
    [IsFiniteMeasure μ] (hμν : μ univ = ν univ) (h : ∀ ⦃a b⦄, a < b → μ (Ioc a b) = ν (Ioc a b)) :
    μ = ν

Proof state:
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ univ = ν univ
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (⇑OrderDual.ofDual ⁻¹' Ioc b a) = ν (⇑OrderDual.ofDual ⁻¹' Ioc b a)

Tactic:
exact h hab

Result:
no goals

Proof state:
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ univ = ν univ
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
⊢ μ = ν

Tactic:
refine @ext_of_Ico_finite αᵒᵈ _ _ _ _ _ ‹_› μ ν _ hμν fun a b hab => ?_

Result:
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ univ = ν univ
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (Ico a b) = ν (Ico a b)

Proof state:
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ univ = ν univ
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (Ico a b) = ν (Ico a b)

Tactic:
erw [dual_Ico (α := α)]

Result:
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
hμν : μ univ = ν univ
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (⇑OrderDual.ofDual ⁻¹' Ioc b a) = ν (⇑OrderDual.ofDual ⁻¹' Ioc b a)
-- Mathlib/LinearAlgebra/CliffordAlgebra/Star.lean
theorem star_smul (r : R) (x : CliffordAlgebra Q) : star (r • x) = r • star x

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r : R
x : CliffordAlgebra Q
⊢ star (r • x) = r • star x

Tactic:
rw [star_def, star_def, map_smul, map_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.zero_lt_iff_zero_neq (a : BitVec w) : (0#w < a) ↔ (a ≠ 0#w)

Proof state:
w : Nat
a : BitVec w
⊢ 0#w < a ↔ a ≠ 0#w

Tactic:
constructor <;>
  simp_all only [BitVec.lt_def, BitVec.toNat_ofNat, Nat.zero_mod, ne_eq, BitVec.toNat_eq] <;>
  omega

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem dmuld : sqrtd (d := d) * sqrtd (d := d) = d

Proof state:
d : ℤ
⊢ sqrtd * sqrtd = ↑d

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_zero_eval_zero : (descPochhammer R 0).eval 0 = 1

Proof state:
R : Type u
inst✝ : Ring R
⊢ eval 0 (descPochhammer R 0) = 1

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Category/Cat.lean
lemma leftUnitor_hom_app {B C : Cat} (F : B ⟶ C) (X : B) : (λ_ F).hom.app X = eqToHom (by simp) :=
  rfl

Proof state:
B C : Cat
F : B ⟶ C
X : ↑B
⊢ (𝟙 B ≫ F).obj X = F.obj X

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Sum/Interval.lean
lemma Ico_inr_inr :
    Ico (inrₗ b₁ : α ⊕ₗ β) (inrₗ b₂) = (Ico b₁ b₂).map (Embedding.inr.trans toLex.toEmbedding)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Ico (inrₗ b₁) (inrₗ b₂) = map (Embedding.inr.trans toLex.toEmbedding) (Ico b₁ b₂)

Tactic:
rw [← Finset.map_map]

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Ico (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ico b₁ b₂))

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : OrderTop α
inst✝² : OrderBot β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
b₁ b₂ : β
⊢ Ico (inrₗ b₁) (inrₗ b₂) = map toLex.toEmbedding (map Embedding.inr (Ico b₁ b₂))

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Choose/Sum.lean
theorem add_pow' (h : Commute x y) (n : ℕ) :
    (x + y) ^ n = ∑ m ∈ antidiagonal n, n.choose m.1 • (x ^ m.1 * y ^ m.2)

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ n = ∑ m ∈ antidiagonal n, n.choose m.1 • (x ^ m.1 * y ^ m.2)

Tactic:
simp_rw [Nat.sum_antidiagonal_eq_sum_range_succ fun m p ↦ n.choose m • (x ^ m * y ^ p),
  nsmul_eq_mul, cast_comm, h.add_pow]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem MeasurableSet.const (p : Prop) : MeasurableSet { _a : α | p }

Proof state:
α : Type u_1
m : MeasurableSpace α
p : Prop
⊢ MeasurableSet {_a | p}

Tactic:
by_cases p <;> simp [*]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean
theorem foldl_algebraMap (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) (r : R) :
    foldl Q f hf n (algebraMap R _ r) = r • n

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
r : R
⊢ ((foldl Q f hf) n) ((algebraMap R (CliffordAlgebra Q)) r) = r • n

Tactic:
rw [← foldr_reverse, reverse.commutes, foldr_algebraMap]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
@[simp]
lemma evalEval_polynomialX_zero : W'.polynomialX.evalEval 0 0 = -W'.a₄

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ evalEval 0 0 W'.polynomialX = -W'.a₄

Tactic:
simp only [evalEval_polynomialX, zero_add, zero_sub, mul_zero, zero_pow <| Nat.succ_ne_zero _]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range'_ne_empty_iff (s : Nat) {n step : Nat} : range' s n step ≠ #[] ↔ n ≠ 0

Proof state:
s n step : Nat
⊢ range' s n step ≠ #[] ↔ n ≠ 0

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_eq_get! [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] {h} :
    m.get a h = m.get! a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h✝ : m.WF
a : α
inst✝ : Inhabited (β a)
h : a ∈ m
⊢ m.get a h = m.get! a

Tactic:
simp_to_raw using Raw₀.get_eq_get!

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem iUnion_Ioc_add_intCast : ⋃ n : ℤ, Ioc (a + n) (a + n + 1) = Set.univ

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
a : α
⊢ ⋃ n, Ioc (a + ↑n) (a + ↑n + 1) = univ

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
  iUnion_Ioc_add_zsmul zero_lt_one a

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem FG.range {N : Type*} [L.Structure N] (h : FG L M) (f : M →[L] N) : f.range.FG

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : FG L M
f : M →[L] N
⊢ (map f ⊤).FG

Tactic:
exact (fg_def.1 h).map f

Result:
no goals

Proof state:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : FG L M
f : M →[L] N
⊢ f.range.FG

Tactic:
rw [Hom.range_eq_map]

Result:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
h : FG L M
f : M →[L] N
⊢ (map f ⊤).FG
-- Mathlib/Order/PropInstances.lean
theorem Prop.isCompl_iff {P Q : Prop} : IsCompl P Q ↔ ¬(P ↔ Q)

Proof state:
P Q : Prop
⊢ IsCompl P Q ↔ ¬(P ↔ Q)

Tactic:
rw [_root_.isCompl_iff, Prop.disjoint_iff, Prop.codisjoint_iff, not_iff]

Result:
P Q : Prop
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Proof state:
P Q : Prop
⊢ ¬(P ∧ Q) ∧ (P ∨ Q) ↔ (¬P ↔ Q)

Tactic:
by_cases P <;> by_cases Q <;> simp [*]

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

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

Tactic:
rw [coeff_reverse, revAt_le (zero_le f.natDegree), tsub_zero, leadingCoeff]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
@[to_additive] lemma commute_coe_inv : Commute (a : α) ↑a⁻¹

Proof state:
α : Type u
inst✝ : Monoid α
a : αˣ
⊢ Commute ↑a ↑a⁻¹

Tactic:
rw [Commute, SemiconjBy, inv_mul, mul_inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_eq_getD_get? [LawfulBEq α] (h : m.1.WF) {a : α} {fallback : β a} :
    m.getD a fallback = (m.get? a).getD fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
a : α
fallback : β a
⊢ m.getD a fallback = (m.get? a).getD fallback

Tactic:
simp_to_model using List.getValueCastD_eq_getValueCast?

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
@[simp] lemma measurableAtom_of_measurableSingletonClass [MeasurableSingletonClass β] (x : β) :
    measurableAtom x = {x} :=
  Subset.antisymm (measurableAtom_subset (measurableSet_singleton x) rfl) (by simp)

Proof state:
β : Type u_2
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSingletonClass β
x : β
⊢ {x} ⊆ measurableAtom x

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/ResidueField.lean
@[simp]
lemma residueFieldCongr_trans {x y z : X} (e : x = y) (e' : y = z) :
    X.residueFieldCongr e ≪≫ X.residueFieldCongr e' = X.residueFieldCongr (e.trans e')

Proof state:
X : Scheme
x y z : ↑↑X.toPresheafedSpace
e : x = y
e' : y = z
⊢ residueFieldCongr e ≪≫ residueFieldCongr e' = residueFieldCongr ⋯

Tactic:
subst e e'

Result:
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ residueFieldCongr ⋯ ≪≫ residueFieldCongr ⋯ = residueFieldCongr ⋯

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ residueFieldCongr ⋯ ≪≫ residueFieldCongr ⋯ = residueFieldCongr ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem Left.mul_pos [PosMulStrictMono α] (ha : 0 < a) (hb : 0 < b) : 0 < a * b

Proof state:
α : Type u_3
a b : α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b

Tactic:
simpa only [mul_zero] using mul_lt_mul_of_pos_left hb ha

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem Equiv.Perm.decomposeFin_symm_apply_one {n : ℕ} (e : Perm (Fin (n + 1))) (p : Fin (n + 2)) :
    Equiv.Perm.decomposeFin.symm (p, e) 1 = swap 0 p (e 0).succ

Proof state:
n : ℕ
e : Perm (Fin (n + 1))
p : Fin (n + 2)
⊢ (decomposeFin.symm (p, e)) 1 = (swap 0 p) (e 0).succ

Tactic:
rw [← Fin.succ_zero_eq_one, Equiv.Perm.decomposeFin_symm_apply_succ e p 0]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
lemma ediam_def : G.ediam = ⨆ p : α × α, G.edist p.1 p.2

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ G.ediam = ⨆ p, G.edist p.1 p.2

Tactic:
rw [ediam, iSup_prod]

Result:
no goals
-- Mathlib/Order/Compare.lean
theorem eq_iff_eq_of_cmp_eq_cmp (h : cmp x y = cmp x' y') : x = y ↔ x' = y'

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x = y ↔ x' = y'

Tactic:
rw [le_antisymm_iff, le_antisymm_iff, le_iff_le_of_cmp_eq_cmp h,
    le_iff_le_of_cmp_eq_cmp (cmp_eq_cmp_symm.1 h)]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem vadd_mem_of_mem_direction {s : AffineSubspace k P} {v : V} (hv : v ∈ s.direction) {p : P}
    (hp : p ∈ s) : v +ᵥ p ∈ s

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
s : AffineSubspace k P
v : V
hv : ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂
p : P
hp : p ∈ s
⊢ v +ᵥ p ∈ s

Tactic:
rcases hv with ⟨p₁, hp₁, p₂, hp₂, hv⟩

Result:
case intro.intro.intro.intro
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
s : AffineSubspace k P
v : V
p : P
hp : p ∈ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : v = p₁ -ᵥ p₂
⊢ v +ᵥ p ∈ s

Proof state:
case h.e'_1.h.e'_5
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
s : AffineSubspace k P
v : V
p : P
hp : p ∈ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : v = p₁ -ᵥ p₂
⊢ p₁ -ᵥ p₂ = 1 • (p₁ -ᵥ p₂)

Tactic:
rw [one_smul]

Result:
no goals

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
s : AffineSubspace k P
v : V
hv : v ∈ s.direction
p : P
hp : p ∈ s
⊢ v +ᵥ p ∈ s

Tactic:
rw [mem_direction_iff_eq_vsub ⟨p, hp⟩] at hv

Result:
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
s : AffineSubspace k P
v : V
hv : ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂
p : P
hp : p ∈ s
⊢ v +ᵥ p ∈ s

Proof state:
case intro.intro.intro.intro
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
s : AffineSubspace k P
v : V
p : P
hp : p ∈ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : v = p₁ -ᵥ p₂
⊢ v +ᵥ p ∈ s

Tactic:
rw [hv]

Result:
case intro.intro.intro.intro
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
s : AffineSubspace k P
v : V
p : P
hp : p ∈ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : v = p₁ -ᵥ p₂
⊢ (p₁ -ᵥ p₂) +ᵥ p ∈ s

Proof state:
case intro.intro.intro.intro
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
s : AffineSubspace k P
v : V
p : P
hp : p ∈ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : v = p₁ -ᵥ p₂
⊢ (p₁ -ᵥ p₂) +ᵥ p ∈ s

Tactic:
convert s.smul_vsub_vadd_mem 1 hp₁ hp₂ hp

Result:
case h.e'_1.h.e'_5
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
s : AffineSubspace k P
v : V
p : P
hp : p ∈ s
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
hp₂ : p₂ ∈ s
hv : v = p₁ -ᵥ p₂
⊢ p₁ -ᵥ p₂ = 1 • (p₁ -ᵥ p₂)
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem bot_left : (⊥ : Subalgebra R S).LinearDisjoint B

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
B : Subalgebra R S
⊢ ⊥.LinearDisjoint B

Tactic:
rw [Subalgebra.LinearDisjoint, Algebra.toSubmodule_bot]

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
B : Subalgebra R S
⊢ Submodule.LinearDisjoint 1 (toSubmodule B)

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
B : Subalgebra R S
⊢ Submodule.LinearDisjoint 1 (toSubmodule B)

Tactic:
exact Submodule.LinearDisjoint.one_left _

Result:
no goals