harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/BilinearForm/Properties.lean
theorem symmCompOfNondegenerate_left_apply (B₁ : BilinForm K V) {B₂ : BilinForm K V}
    (b₂ : B₂.Nondegenerate) (v w : V) : B₂ (symmCompOfNondegenerate B₁ B₂ b₂ w) v = B₁ w v

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B₁ B₂ : BilinForm K V
b₂ : B₂.Nondegenerate
v w : V
⊢ (B₂ ((B₁.symmCompOfNondegenerate B₂ b₂) w)) v = (B₁ w) v

Tactic:
conv_lhs => rw [comp_symmCompOfNondegenerate_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_smul_left {m : MeasurableSpace α} (T : Set α → F →L[ℝ] F') (c : ℝ)
    (f : α →ₛ F) : setToSimpleFunc (fun s => c • T s) f = c • setToSimpleFunc T f

Proof state:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
c : ℝ
f : α →ₛ F
⊢ setToSimpleFunc (fun s => c • T s) f = c • setToSimpleFunc T f

Tactic:
simp_rw [setToSimpleFunc, ContinuousLinearMap.smul_apply, smul_sum]

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

Proof state:
case h.e'_3.h.e'_16
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₁)
b₂ : B
⊢ a₁ = a₁ * ↑GradedMonoid.GOne.one

Tactic:
rw [SetLike.coe_gOne, mul_one]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[aesop norm apply (rule_sets := [CStarAlgebra])]
lemma posPart_nonneg (a : A) :
    0 ≤ a⁺ :=
  cfcₙ_nonneg (fun x _ ↦ by positivity)

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
x : ℝ
x✝ : x ∈ quasispectrum ℝ a
⊢ 0 ≤ x⁺

Tactic:
positivity

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem wittMul_zero : wittMul p 0 = X (0, 0) * X (1, 0)

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittMul p 0) = (map (Int.castRingHom ℚ)) (X (0, 0) * X (1, 0))

Tactic:
simp only [wittMul, wittStructureRat, rename_X, xInTermsOfW_zero, map_X, wittPolynomial_zero,
  map_mul, bind₁_X_right, map_wittStructureInt]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittMul p 0 = X (0, 0) * X (1, 0)

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittMul p 0) = (map (Int.castRingHom ℚ)) (X (0, 0) * X (1, 0))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getMsbD i = false

Proof state:
i : Nat
x : BitVec 0
⊢ x.getMsbD i = false

Tactic:
simp [getMsbD_zero_length]

Result:
no goals

Proof state:
w i : Nat
h : w = 0
x : BitVec w
⊢ x.getMsbD i = false

Tactic:
subst h

Result:
i : Nat
x : BitVec 0
⊢ x.getMsbD i = false
-- Mathlib/Data/Fintype/Order.lean
lemma Finite.exists_minimal_le [Finite α] (h : p a) : ∃ b, b ≤ a ∧ Minimal p b

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
p : α → Prop
inst✝ : Finite α
h : p a
⊢ ∃ b ≤ a, Minimal p b

Tactic:
obtain ⟨b, ⟨hba, hb⟩, hbmin⟩ :=
  Set.Finite.exists_minimal_wrt id {x | x ≤ a ∧ p x} (Set.toFinite _) ⟨a, rfl.le, h⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
a : α
p : α → Prop
inst✝ : Finite α
h : p a
b : α
hbmin : ∀ a' ∈ {x | x ≤ a ∧ p x}, id a' ≤ id b → id b = id a'
hba : b ≤ a
hb : p b
⊢ ∃ b ≤ a, Minimal p b

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : PartialOrder α
a : α
p : α → Prop
inst✝ : Finite α
h : p a
b : α
hbmin : ∀ a' ∈ {x | x ≤ a ∧ p x}, id a' ≤ id b → id b = id a'
hba : b ≤ a
hb : p b
⊢ ∃ b ≤ a, Minimal p b

Tactic:
exact ⟨b, hba, hb, fun x hx hxb ↦ (hbmin x ⟨hxb.trans hba, hx⟩ hxb).le⟩

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Pairwise.lean
theorem pairwise_pair : #[a, b].Pairwise R ↔ R a b

Proof state:
α✝ : Type u_1
a b : α✝
R : α✝ → α✝ → Prop
⊢ Pairwise R #[a, b] ↔ R a b

Tactic:
unfold Pairwise

Result:
α✝ : Type u_1
a b : α✝
R : α✝ → α✝ → Prop
⊢ List.Pairwise R #[a, b].toList ↔ R a b

Proof state:
α✝ : Type u_1
a b : α✝
R : α✝ → α✝ → Prop
⊢ List.Pairwise R #[a, b].toList ↔ R a b

Tactic:
exact List.pairwise_pair

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_sub_pi_div_two (θ : Angle) : cos (θ - ↑(π / 2)) = sin θ

Proof state:
case h
x✝ : ℝ
⊢ (↑x✝ - ↑(π / 2)).cos = (↑x✝).sin

Tactic:
exact Real.cos_sub_pi_div_two _

Result:
no goals

Proof state:
θ : Angle
⊢ (θ - ↑(π / 2)).cos = θ.sin

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ (↑x✝ - ↑(π / 2)).cos = (↑x✝).sin
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive one_add_zsmul]
lemma zpow_one_add (a : G) (n : ℤ) : a ^ (1 + n) = a * a ^ n

Proof state:
G : Type u_3
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ (1 + n) = a * a ^ n

Tactic:
rw [zpow_add, zpow_one]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem neg_of_int : ∀ n, ((-n : ℤ) : ZNum) = -n
  | (_ + 1 : ℕ) => rfl
  | 0 => by rw [Int.cast_neg]
  | -[_+1] => (zneg_zneg _).symm

Proof state:
⊢ ↑(-0) = -↑0

Tactic:
rw [Int.cast_neg]

Result:
no goals
-- Mathlib/RingTheory/Localization/Integral.lean
theorem integerNormalization_map_to_map (p : S[X]) :
    ∃ b : M, (integerNormalization M p).map (algebraMap R S) = (b : R) • p :=
  let ⟨b, hb⟩ := integerNormalization_spec M p
  ⟨b,
    Polynomial.ext fun i => by
      rw [coeff_map, coeff_smul]
      exact hb i⟩

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
b : ↥M
hb : ∀ (i : ℕ), (algebraMap R S) ((integerNormalization M p).coeff i) = ↑b • p.coeff i
i : ℕ
⊢ (algebraMap R S) ((integerNormalization M p).coeff i) = ↑b • p.coeff i

Tactic:
exact hb i

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
b : ↥M
hb : ∀ (i : ℕ), (algebraMap R S) ((integerNormalization M p).coeff i) = ↑b • p.coeff i
i : ℕ
⊢ (Polynomial.map (algebraMap R S) (integerNormalization M p)).coeff i = (↑b • p).coeff i

Tactic:
rw [coeff_map, coeff_smul]

Result:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
p : S[X]
b : ↥M
hb : ∀ (i : ℕ), (algebraMap R S) ((integerNormalization M p).coeff i) = ↑b • p.coeff i
i : ℕ
⊢ (algebraMap R S) ((integerNormalization M p).coeff i) = ↑b • p.coeff i
-- Mathlib/Data/Finset/Option.lean
theorem mem_toFinset {a : α} {o : Option α} : a ∈ o.toFinset ↔ a ∈ o

Proof state:
α : Type u_1
a : α
o : Option α
⊢ a ∈ o.toFinset ↔ a ∈ o

Tactic:
cases o <;> simp [eq_comm]

Result:
no goals
-- Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
lemma ConcreteCategory.forget₂_comp_apply {C : Type u} {D : Type u'} [Category.{v} C]
    {FC : C → C → Type*} {CC : C → Type w} [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)]
    [ConcreteCategory.{w} C FC] [Category.{v'} D] {FD : D → D → Type*} {CD : D → Type w}
    [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory.{w} D FD] [HasForget₂ C D] {X Y Z : C}
    (f : X ⟶ Y) (g : Y ⟶ Z) (x : ToType ((forget₂ C D).obj X)) :
    ((forget₂ C D).map (f ≫ g) x) =
      (forget₂ C D).map g ((forget₂ C D).map f x)

Proof state:
C : Type u
D : Type u'
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_3
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : HasForget₂ C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : ToType ((forget₂ C D).obj X)
⊢ (hom ((forget₂ C D).map (f ≫ g))) x = (hom ((forget₂ C D).map g)) ((hom ((forget₂ C D).map f)) x)

Tactic:
rw [Functor.map_comp, ConcreteCategory.comp_apply]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
theorem r_zpow (i : ZMod n) (k : ℤ) : (r i)^k = r (i * k : ZMod n)

Proof state:
n : ℕ
i : ZMod n
k : ℤ
⊢ r i ^ k = r (i * ↑k)

Tactic:
cases k <;> simp [r_pow, neg_mul_eq_mul_neg]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem csSup_Iio [NoMinOrder α] [DenselyOrdered α] : sSup (Iio a) = a :=
  csSup_eq_of_forall_le_of_forall_lt_exists_gt nonempty_Iio (fun _ => le_of_lt) fun w hw => by
    simpa [and_comm] using exists_between hw

Proof state:
α : Type u_1
inst✝² : ConditionallyCompleteLattice α
a : α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
w : α
hw : w < a
⊢ ∃ a_1 ∈ Iio a, w < a_1

Tactic:
simpa [and_comm] using exists_between hw

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem midpoint_eq_left_iff {x y : P} : midpoint R x y = x ↔ x = y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ midpoint R x y = x ↔ x = y

Tactic:
rw [midpoint_eq_iff, pointReflection_self]

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
@[simp]
lemma finsuppScalarRight_apply_tmul_apply (m : M) (p : ι →₀ R) (i : ι) :
    finsuppScalarRight R M ι (m ⊗ₜ[R] p) i = p i • m

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : DecidableEq ι
m : M
p : ι →₀ R
i : ι
⊢ ((finsuppScalarRight R M ι) (m ⊗ₜ[R] p)) i = p i • m

Tactic:
simp [finsuppScalarRight]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem discreteTopology_iff_singleton_mem_nhds [TopologicalSpace α] :
    DiscreteTopology α ↔ ∀ x : α, {x} ∈ 𝓝 x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ DiscreteTopology α ↔ ∀ (x : α), {x} ∈ 𝓝 x

Tactic:
simp only [← singletons_open_iff_discrete, isOpen_iff_mem_nhds, mem_singleton_iff, forall_eq]

Result:
no goals
-- Mathlib/Analysis/Convex/Combination.lean
theorem convexHull_sub (s t : Set E) : convexHull R (s - t) = convexHull R s - convexHull R t

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s t : Set E
⊢ (convexHull R) (s - t) = (convexHull R) s - (convexHull R) t

Tactic:
simp_rw [sub_eq_add_neg, convexHull_add, ← convexHull_neg]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma _root_.Submodule.inf_genEigenspace (f : End R M) (p : Submodule R M) {k : ℕ∞} {μ : R}
    (hfp : ∀ x : M, x ∈ p → f x ∈ p) :
    p ⊓ f.genEigenspace μ k =
      (genEigenspace (LinearMap.restrict f hfp) μ k).map p.subtype

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
⊢ p ⊓ (f.genEigenspace μ) k = Submodule.map p.subtype ((genEigenspace (LinearMap.restrict f hfp) μ) k)

Tactic:
rw [f.genEigenspace_restrict _ _ _ hfp, Submodule.map_comap_eq, Submodule.range_subtype]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem testAgainstNN_mono (μ : FiniteMeasure Ω) {f g : Ω →ᵇ ℝ≥0} (f_le_g : (f : Ω → ℝ≥0) ≤ g) :
    μ.testAgainstNN f ≤ μ.testAgainstNN g

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : ⇑f ≤ ⇑g
⊢ μ.testAgainstNN f ≤ μ.testAgainstNN g

Tactic:
simp only [← ENNReal.coe_le_coe, testAgainstNN_coe_eq]

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : ⇑f ≤ ⇑g
⊢ ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ ≤ ∫⁻ (ω : Ω), ↑(g ω) ∂↑μ

Proof state:
case hfg.a
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : ⇑f ≤ ⇑g
x✝ : Ω
⊢ f x✝ ≤ g x✝

Tactic:
apply f_le_g

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : ⇑f ≤ ⇑g
⊢ ∫⁻ (ω : Ω), ↑(f ω) ∂↑μ ≤ ∫⁻ (ω : Ω), ↑(g ω) ∂↑μ

Tactic:
gcongr

Result:
case hfg.a
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : ⇑f ≤ ⇑g
x✝ : Ω
⊢ f x✝ ≤ g x✝
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reflect_C_mul (f : R[X]) (r : R) (N : ℕ) : reflect N (C r * f) = C r * reflect N f

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
N n✝ : ℕ
⊢ (reflect N (C r * f)).coeff n✝ = (C r * reflect N f).coeff n✝

Tactic:
simp only [coeff_reflect, coeff_C_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
N : ℕ
⊢ reflect N (C r * f) = C r * reflect N f

Tactic:
ext

Result:
case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
N n✝ : ℕ
⊢ (reflect N (C r * f)).coeff n✝ = (C r * reflect N f).coeff n✝
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
theorem sup'_id_eq_csSup (s : Finset α) (hs) : s.sup' hs id = sSup s

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Finset α
hs : s.Nonempty
⊢ s.sup' hs id = sSup ↑s

Tactic:
rw [sup'_eq_csSup_image s hs, Set.image_id]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_apply_left (a : α) : toIcoMod hp a a = a

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a = a + 0 • p

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ toIcoMod hp a a = a

Tactic:
rw [toIcoMod_eq_iff hp, Set.left_mem_Ico]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a < a + p ∧ ∃ z, a = a + z • p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ a < a + p ∧ ∃ z, a = a + z • p

Tactic:
exact ⟨lt_add_of_pos_right _ hp, 0, by simp⟩

Result:
no goals
-- Mathlib/Topology/Order.lean
lemma continuous_generateFrom_iff {t : TopologicalSpace α} {b : Set (Set β)} :
    Continuous[t, generateFrom b] f ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s)

Proof state:
α : Type u
β : Type v
f : α → β
t : TopologicalSpace α
b : Set (Set β)
⊢ Continuous f ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s)

Tactic:
rw [continuous_iff_coinduced_le, le_generateFrom_iff_subset_isOpen]

Result:
α : Type u
β : Type v
f : α → β
t : TopologicalSpace α
b : Set (Set β)
⊢ b ⊆ {s | IsOpen s} ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s)

Proof state:
α : Type u
β : Type v
f : α → β
t : TopologicalSpace α
b : Set (Set β)
⊢ b ⊆ {s | IsOpen s} ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s)

Tactic:
simp only [isOpen_coinduced, preimage_id', subset_def, mem_setOf]

Result:
no goals
-- Mathlib/Algebra/Lie/Derivation/AdjointAction.lean
/-- If the center of a Lie algebra is trivial, then the adjoint action is injective. -/
lemma injective_ad_of_center_eq_bot (h : LieAlgebra.center R L = ⊥) :
    Function.Injective (ad R L)

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : LieAlgebra.center R L = ⊥
⊢ Function.Injective ⇑(ad R L)

Tactic:
rw [← LieHom.ker_eq_bot, ad_ker_eq_center, h]

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
lemma union_add_distrib (s t u : Multiset α) : s ∪ t + u = s + u ∪ (t + u)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s + u - (t + u) = s - t

Tactic:
rw [t.add_comm, Multiset.sub_add_eq_sub_sub, Multiset.add_sub_cancel_right]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem map_hsymm (n : ℕ) (f : R →+* S) : map f (hsymm σ R n) = hsymm σ S n

Proof state:
S : Type u_4
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
n : ℕ
f : R →+* S
⊢ (map f) (hsymm σ R n) = hsymm σ S n

Tactic:
simp [hsymm, ← Multiset.prod_hom']

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
theorem sign_mul_abs (a : ℤ) : sign a * |a| = a

Proof state:
a : ℤ
⊢ a.sign * |a| = a

Tactic:
rw [abs_eq_natAbs, sign_mul_natAbs a]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
theorem card_dyckWord_semilength_eq_catalan (n : ℕ) :
    Fintype.card { p : DyckWord // p.semilength = n } = catalan n

Proof state:
n : ℕ
⊢ Fintype.card { x // x ∈ treesOfNumNodesEq n } = (treesOfNumNodesEq n).card

Tactic:
convert Fintype.card_coe _

Result:
no goals

Proof state:
n : ℕ
⊢ Fintype.card { p // p.semilength = n } = catalan n

Tactic:
rw [← Fintype.ofEquiv_card (equivTreesOfNumNodesEq n), ← treesOfNumNodesEq_card_eq_catalan]

Result:
n : ℕ
⊢ Fintype.card { x // x ∈ treesOfNumNodesEq n } = (treesOfNumNodesEq n).card
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem iSup₂_disjoint_iff {f : ∀ i, κ i → α} :
    Disjoint (⨆ (i) (j), f i j) a ↔ ∀ i j, Disjoint (f i j) a

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
a : α
f : (i : ι) → κ i → α
⊢ Disjoint (⨆ i, ⨆ j, f i j) a ↔ ∀ (i : ι) (j : κ i), Disjoint (f i j) a

Tactic:
simp_rw [iSup_disjoint_iff]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem LipschitzWith.div (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
    LipschitzWith (Kf + Kg) fun x => f x / g x

Proof state:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (Kf + Kg) fun x => f x / g x

Tactic:
simpa only [div_eq_mul_inv] using hf.mul hg.inv

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
    a.swapAt! i v = (a[i], a.set i v)

Proof state:
α : Type u_1
a : Array α
i : Nat
v : α
h : i < a.size
⊢ a.swapAt! i v = (a[i], a.set i v h)

Tactic:
simp [swapAt!, h]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_dite_of_true {p : α → Prop} {_ : DecidablePred p} (h : ∀ i ∈ s, p i) (f : ∀ i, p i → β)
    (g : ∀ i, ¬ p i → β) :
    ∏ i ∈ s, (if hi : p i then f i hi else g i hi) = ∏ i : s, f i.1 (h _ i.2)

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
inst✝ : CommMonoid β
p : α → Prop
x✝ : DecidablePred p
h : ∀ i ∈ s, p i
f : (i : α) → p i → β
g : (i : α) → ¬p i → β
⊢ (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i : { x // x ∈ s }, f ↑i ⋯

Tactic:
refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_ <;> aesop

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infDist_empty : infDist x ∅ = 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
⊢ infDist x ∅ = 0

Tactic:
simp [infDist]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem sub_dotProduct : (u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w

Proof state:
m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocRing α
u v w : m → α
⊢ (u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem equalizerSubobject_arrow_comp :
    (equalizerSubobject f g).arrow ≫ f = (equalizerSubobject f g).arrow ≫ g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
⊢ (equalizerSubobject f g).arrow ≫ f = (equalizerSubobject f g).arrow ≫ g

Tactic:
rw [← equalizerSubobject_arrow, Category.assoc, Category.assoc, equalizer.condition]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_pop {f : α → β} {l : Array α} : l.pop.map f = (l.map f).pop

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Array α
⊢ map f l.pop = (map f l).pop

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
toList✝ : List α
⊢ map f { toList := toList✝ }.pop = (map f { toList := toList✝ }).pop

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
toList✝ : List α
⊢ map f { toList := toList✝ }.pop = (map f { toList := toList✝ }).pop

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Hom.lean
theorem le_tsub_mul {R : Type*} [CommSemiring R] [Preorder R] [Sub R] [OrderedSub R]
    [MulLeftMono R] {a b c : R} : a * c - b * c ≤ (a - b) * c

Proof state:
R : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Preorder R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : MulLeftMono R
a b c : R
⊢ a * c - b * c ≤ (a - b) * c

Tactic:
simpa only [mul_comm _ c] using le_mul_tsub

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem leadingCoeff_normalize (p : R[X]) :
    leadingCoeff (normalize p) = normalize (leadingCoeff p)

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizationMonoid R
p : R[X]
⊢ (normalize p).leadingCoeff = normalize p.leadingCoeff

Tactic:
simp [normalize_apply]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma comp_assoc_of_third_deg_zero
    {a₁ a₂ a₁₂ : ℕ} (α : Ext X Y a₁) (β : Ext Y Z a₂) (γ : Ext Z T 0)
    (h₁₂ : a₁ + a₂ = a₁₂) :
    (α.comp β h₁₂).comp γ (add_zero _) = α.comp (β.comp γ (add_zero _)) h₁₂

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a₁ a₂ a₁₂ : ℕ
α : Ext X Y a₁
β : Ext Y Z a₂
γ : Ext Z T 0
h₁₂ : a₁ + a₂ = a₁₂
⊢ a₁ + a₂ + 0 = a₁₂

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a₁ a₂ a₁₂ : ℕ
α : Ext X Y a₁
β : Ext Y Z a₂
γ : Ext Z T 0
h₁₂ : a₁ + a₂ = a₁₂
⊢ (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ ⋯) h₁₂

Tactic:
apply comp_assoc

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
a₁ a₂ a₁₂ : ℕ
α : Ext X Y a₁
β : Ext Y Z a₂
γ : Ext Z T 0
h₁₂ : a₁ + a₂ = a₁₂
⊢ a₁ + a₂ + 0 = a₁₂
-- Mathlib/CategoryTheory/Sites/Sheafification.lean
theorem sheafifyMap_sheafifyLift {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R)
    (hR : Presheaf.IsSheaf J R) :
    sheafifyMap J η ≫ sheafifyLift J γ hR = sheafifyLift J (η ≫ γ) hR

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ sheafifyMap J η ≫ sheafifyLift J γ hR = sheafifyLift J (η ≫ γ) hR

Tactic:
apply sheafifyLift_unique

Result:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ toSheafify J P ≫ sheafifyMap J η ≫ sheafifyLift J γ hR = η ≫ γ

Proof state:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
inst✝ : HasWeakSheafify J D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ toSheafify J P ≫ sheafifyMap J η ≫ sheafifyLift J γ hR = η ≫ γ

Tactic:
rw [← Category.assoc, ← toSheafify_naturality, Category.assoc, toSheafify_sheafifyLift]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem t'_fst_fst_snd (i j k : 𝒰.J) :
    t' 𝒰 f g i j k ≫ pullback.fst _ _ ≫ pullback.fst _ _ ≫ pullback.snd _ _ =
      pullback.fst _ _ ≫ pullback.fst _ _ ≫ pullback.snd _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j k : 𝒰.J
⊢ t' 𝒰 f g i j k ≫
      pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫
        pullback.fst (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map k) ≫ pullback.snd (𝒰.map j ≫ f) g =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
      pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.snd (𝒰.map i ≫ f) g

Tactic:
simp only [t', Category.assoc, pullbackSymmetry_hom_comp_fst_assoc,
  pullbackRightPullbackFstIso_inv_snd_fst_assoc, pullback.lift_fst_assoc, t_fst_snd,
  pullbackRightPullbackFstIso_hom_fst_assoc]

Result:
no goals