harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_rename_of_injective {p : MvPolynomial σ R} {f : σ → τ} (h : Function.Injective f)
    (i : σ) : degreeOf (f i) (rename f p) = degreeOf i p

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
i : σ
⊢ degreeOf (f i) ((rename f) p) = degreeOf i p

Tactic:
simp only [degreeOf, degrees_rename_of_injective h, Multiset.count_map_eq_count' f p.degrees h]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
h : Injective f
i : σ
⊢ degreeOf (f i) ((rename f) p) = degreeOf i p

Tactic:
classical
simp only [degreeOf, degrees_rename_of_injective h, Multiset.count_map_eq_count' f p.degrees h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/RationalMap.lean
@[simp]
lemma fromSpecStalkOfMem_toPartialMap (f : X ⟶ Y) (x) :
    f.toPartialMap.fromSpecStalkOfMem (x := x) trivial = X.fromSpecStalk x ≫ f

Proof state:
X Y : Scheme
f : X ⟶ Y
x : ↑↑X.toPresheafedSpace
⊢ (Hom.toPartialMap f).fromSpecStalkOfMem trivial = X.fromSpecStalk x ≫ f

Tactic:
simp [fromSpecStalkOfMem]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[gcongr]
lemma div_le_div_of_nonneg_left (ha : 0 ≤ a) (hc : 0 < c) (h : c ≤ b) : a / b ≤ a / c

Proof state:
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : ZeroLEOneClass G₀
inst✝² : PosMulReflectLT G₀
a b c : G₀
inst✝¹ : MulPosMono G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a * b⁻¹ ≤ a * c⁻¹

Tactic:
exact mul_le_mul_of_nonneg_left ((inv_le_inv₀ (hc.trans_le h) hc).mpr h) ha

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : ZeroLEOneClass G₀
inst✝² : PosMulReflectLT G₀
a b c : G₀
inst✝¹ : MulPosMono G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a / b ≤ a / c

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]

Result:
G₀ : Type u_2
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : PartialOrder G₀
inst✝³ : ZeroLEOneClass G₀
inst✝² : PosMulReflectLT G₀
a b c : G₀
inst✝¹ : MulPosMono G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a * b⁻¹ ≤ a * c⁻¹
-- Mathlib/Data/Matroid/Circuit.lean
@[simp] lemma dual_isCocircuit_iff : M✶.IsCocircuit C ↔ M.IsCircuit C

Proof state:
α : Type u_1
M : Matroid α
C : Set α
⊢ M✶.IsCocircuit C ↔ M.IsCircuit C

Tactic:
rw [isCocircuit_def, dual_dual]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem cpow_ne_zero_iff_of_exponent_ne_zero {x y : ℂ} (hy : y ≠ 0) :
    x ^ y ≠ 0 ↔ x ≠ 0

Proof state:
x y : ℂ
hy : y ≠ 0
⊢ x ^ y ≠ 0 ↔ x ≠ 0

Tactic:
simp [hy]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
/-- If `s ⊆ s₁ ⊆ ℝ` and `t ⊆ t₁ ⊆ ℝ`, then `s × t ⊆ s₁ × t₁` in `ℂ`. -/
lemma reProdIm_subset_iff' {s s₁ t t₁ : Set ℝ} :
    s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Proof state:
case h.e'_1.a
s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

Tactic:
exact reProdIm_subset_iff

Result:
no goals

Proof state:
s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

Tactic:
convert prod_subset_prod_iff

Result:
case h.e'_1.a
s s₁ t t₁ : Set ℝ
⊢ s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁
-- Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean
/-- Given a diagram
```
a'        a --φ--> b
|         |        |
v         v        v
R' --g--> R --f--> S
```
such that `φ` is strongly cartesian, and morphisms `ψ ψ' : a' ⟶ a` such that
`g ≫ ψ = φ' = g ≫ ψ'`. Then we have that `ψ = ψ'`. -/
protected lemma ext (φ : a ⟶ b) [IsStronglyCartesian p f φ] {R' : 𝒮} {a' : 𝒳} (g : R' ⟶ R)
    {ψ ψ' : a' ⟶ a} [IsHomLift p g ψ] [IsHomLift p g ψ'] (h : ψ ≫ φ = ψ' ≫ φ) : ψ = ψ'

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCartesian f φ
R' : 𝒮
a' : 𝒳
g : R' ⟶ R
ψ ψ' : a' ⟶ a
inst✝¹ : p.IsHomLift g ψ
inst✝ : p.IsHomLift g ψ'
h : ψ ≫ φ = ψ' ≫ φ
⊢ ψ = ψ'

Tactic:
rw [map_uniq p f φ (g := g) rfl (ψ ≫ φ) ψ rfl, map_uniq p f φ (g := g) rfl (ψ ≫ φ) ψ' h.symm]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
lemma condExp_nonpos (hf : f ≤ᵐ[μ] 0) : μ[f|m] ≤ᵐ[μ] 0

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : f ≤ᶠ[ae μ] 0
hfint : Integrable f μ
⊢ μ[f|m] ≤ᶠ[ae μ] μ[0|m]

Tactic:
exact condExp_mono hfint (integrable_zero _ _ _) hf

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : f ≤ᶠ[ae μ] 0
hfint : ¬Integrable f μ
⊢ μ[f|m] ≤ᶠ[ae μ] 0

Tactic:
rw [condExp_of_not_integrable hfint]

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : f ≤ᶠ[ae μ] 0
hfint : Integrable f μ
⊢ μ[f|m] ≤ᶠ[ae μ] 0

Tactic:
rw [(condExp_zero.symm : (0 : α → E) = μ[0|m])]

Result:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : f ≤ᶠ[ae μ] 0
hfint : Integrable f μ
⊢ μ[f|m] ≤ᶠ[ae μ] μ[0|m]

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : f ≤ᶠ[ae μ] 0
⊢ μ[f|m] ≤ᶠ[ae μ] 0

Tactic:
by_cases hfint : Integrable f μ

Result:
case pos
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : f ≤ᶠ[ae μ] 0
hfint : Integrable f μ
⊢ μ[f|m] ≤ᶠ[ae μ] 0

case neg
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst✝³ : NormedLatticeAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OrderedSMul ℝ E
hf : f ≤ᶠ[ae μ] 0
hfint : ¬Integrable f μ
⊢ μ[f|m] ≤ᶠ[ae μ] 0
-- Mathlib/Data/TypeVec.lean
theorem repeatEq_iff_eq {α : TypeVec n} {i x y} :
    ofRepeat (repeatEq α i (prod.mk _ x y)) ↔ x = y

Proof state:
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
x y : α i
⊢ ofRepeat (α.repeatEq i (prod.mk i x y)) ↔ x = y

Tactic:
induction i with
| fz => rfl
| fs _ i_ih => erw [repeatEq, i_ih]

Result:
no goals

Proof state:
case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
x y : α Fin2.fz
⊢ ofRepeat (α.repeatEq Fin2.fz (prod.mk Fin2.fz x y)) ↔ x = y

Tactic:
rfl

Result:
no goals

Proof state:
case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝} {x y : α a✝}, ofRepeat (α.repeatEq a✝ (prod.mk a✝ x y)) ↔ x = y
α : TypeVec.{u_1} (n✝ + 1)
x y : α a✝.fs
⊢ ofRepeat (α.repeatEq a✝.fs (prod.mk a✝.fs x y)) ↔ x = y

Tactic:
erw [repeatEq, i_ih]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma add_equiv {P P' Q Q' : Fin 3 → R} (hP : P ≈ P') (hQ : Q ≈ Q') :
    W'.add P Q ≈ W'.add P' Q'

Proof state:
case intro.intro
R : Type r
inst✝ : CommRing R
W' : Projective R
P' Q' : Fin 3 → R
u v : Rˣ
⊢ W'.add ((fun m => m • P') u) ((fun m => m • Q') v) ≈ W'.add P' Q'

Tactic:
exact add_smul_equiv P' Q' u.isUnit v.isUnit

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P P' Q Q' : Fin 3 → R
hP : P ≈ P'
hQ : Q ≈ Q'
⊢ W'.add P Q ≈ W'.add P' Q'

Tactic:
rcases hP, hQ with ⟨⟨u, rfl⟩, ⟨v, rfl⟩⟩

Result:
case intro.intro
R : Type r
inst✝ : CommRing R
W' : Projective R
P' Q' : Fin 3 → R
u v : Rˣ
⊢ W'.add ((fun m => m • P') u) ((fun m => m • Q') v) ≈ W'.add P' Q'
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nadd_one (a : Ordinal) : a ♯ 1 = succ a

Proof state:
case mk
a i : Ordinal.{u_1}
hi : i ∈ Iio a
⊢ succ (↑⟨i, hi⟩ ♯ 1) ≤ succ a

Tactic:
rwa [nadd_one, succ_le_succ_iff, succ_le_iff]

Result:
no goals

Proof state:
a : Ordinal.{u_1}
⊢ ∀ (i : ↑(Iio a)), succ (↑i ♯ 1) ≤ succ a

Tactic:
rintro ⟨i, hi⟩

Result:
case mk
a i : Ordinal.{u_1}
hi : i ∈ Iio a
⊢ succ (↑⟨i, hi⟩ ♯ 1) ≤ succ a

Proof state:
a : Ordinal.{u_1}
⊢ a ♯ 1 = succ a

Tactic:
rw [nadd, ciSup_unique (s := fun _ : Iio 1 ↦ _), Iio_one_default_eq, nadd_zero,
  max_eq_right_iff, Ordinal.iSup_le_iff]

Result:
a : Ordinal.{u_1}
⊢ ∀ (i : ↑(Iio a)), succ (↑i ♯ 1) ≤ succ a
-- Mathlib/GroupTheory/Perm/Support.lean
theorem card_support_conj : #(σ * τ * σ⁻¹).support = #τ.support

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ #(σ * τ * σ⁻¹).support = #τ.support

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem IsPrefix.ne_nil {x y : List α} (h : x <+: y) (hx : x ≠ []) : y ≠ []

Proof state:
α : Type u_1
x : List α
hx : x ≠ []
h : x <+: []
⊢ False

Tactic:
exact hx <| List.prefix_nil.mp h

Result:
no goals

Proof state:
α : Type u_1
x y : List α
h : x <+: y
hx : x ≠ []
⊢ y ≠ []

Tactic:
rintro rfl

Result:
α : Type u_1
x : List α
hx : x ≠ []
h : x <+: []
⊢ False
-- Mathlib/Algebra/Order/Star/Basic.lean
@[simp]
lemma star_lt_star_iff {x y : R} : star x < star y ↔ x < y

Proof state:
case neg
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
h : ¬x = y
⊢ star x < star y ↔ x < y

Tactic:
simpa [le_iff_lt_or_eq, h] using star_le_star_iff (x := x) (y := y)

Result:
no goals

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
⊢ star x < star y ↔ x < y

Tactic:
by_cases h : x = y

Result:
case pos
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
h : x = y
⊢ star x < star y ↔ x < y

case neg
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
h : ¬x = y
⊢ star x < star y ↔ x < y

Proof state:
case pos
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x y : R
h : x = y
⊢ star x < star y ↔ x < y

Tactic:
simp [h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
theorem Trident.equalizer_ext [Nonempty J] (s : Trident f) {W : C} {k l : W ⟶ s.pt}
    (h : k ≫ s.ι = l ≫ s.ι) : ∀ j : WalkingParallelFamily J, k ≫ s.π.app j = l ≫ s.π.app j
  | zero => h
  | one => by rw [← s.app_zero (Classical.arbitrary J), reassoc_of% h]

Proof state:
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s : Trident f
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ k ≫ s.π.app one = l ≫ s.π.app one

Tactic:
rw [← s.app_zero (Classical.arbitrary J), reassoc_of% h]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup'_cons {b : β} {hb : b ∉ s} :
    (cons b s hb).sup' (cons_nonempty hb) f = f b ⊔ s.sup' H f

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
b : β
hb : b ∉ s
⊢ ↑((cons b s hb).sup' ⋯ f) = ↑(f b ⊔ s.sup' H f)

Tactic:
simp [WithBot.coe_sup]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
b : β
hb : b ∉ s
⊢ (cons b s hb).sup' ⋯ f = f b ⊔ s.sup' H f

Tactic:
rw [← WithBot.coe_eq_coe]

Result:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
f : β → α
b : β
hb : b ∉ s
⊢ ↑((cons b s hb).sup' ⋯ f) = ↑(f b ⊔ s.sup' H f)
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem map_map_of_aemeasurable {g : β → γ} {f : α → β} (hg : AEMeasurable g (Measure.map f μ))
    (hf : AEMeasurable f μ) : (μ.map f).map g = μ.map (g ∘ f)

Proof state:
case h
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
s : Set γ
hs : MeasurableSet s
⊢ (Measure.map g (Measure.map f μ)) s = (Measure.map (g ∘ f) μ) s

Tactic:
rw [map_apply_of_aemeasurable hg hs, map_apply₀ hf (hg.nullMeasurable hs),
  map_apply_of_aemeasurable (hg.comp_aemeasurable hf) hs, preimage_comp]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ Measure.map g (Measure.map f μ) = Measure.map (g ∘ f) μ

Tactic:
ext1 s hs

Result:
case h
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ : Measure α
g : β → γ
f : α → β
hg : AEMeasurable g (Measure.map f μ)
hf : AEMeasurable f μ
s : Set γ
hs : MeasurableSet s
⊢ (Measure.map g (Measure.map f μ)) s = (Measure.map (g ∘ f) μ) s
-- Mathlib/Data/Multiset/Fintype.lean
theorem prod_toEnumFinset {β : Type*} [CommMonoid β] (m : Multiset α) (f : α → ℕ → β) :
    ∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x : m, f x x.2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
β : Type u_3
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x : m.ToType, f x.fst ↑x.snd

Tactic:
rw [Fintype.prod_equiv m.coeEquiv (fun x ↦ f x x.2) fun x ↦ f x.1.1 x.1.2]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
β : Type u_3
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x : { x // x ∈ m.toEnumFinset }, f (↑x).1 (↑x).2

α : Type u_1
inst✝¹ : DecidableEq α
β : Type u_3
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∀ (x : m.ToType), f x.fst ↑x.snd = f (↑(m.coeEquiv x)).1 (↑(m.coeEquiv x)).2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
β : Type u_3
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
x : m.ToType
⊢ f x.fst ↑x.snd = f (↑(m.coeEquiv x)).1 (↑(m.coeEquiv x)).2

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
β : Type u_3
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∀ (x : m.ToType), f x.fst ↑x.snd = f (↑(m.coeEquiv x)).1 (↑(m.coeEquiv x)).2

Tactic:
intro x

Result:
α : Type u_1
inst✝¹ : DecidableEq α
β : Type u_3
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
x : m.ToType
⊢ f x.fst ↑x.snd = f (↑(m.coeEquiv x)).1 (↑(m.coeEquiv x)).2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
β : Type u_3
inst✝ : CommMonoid β
m : Multiset α
f : α → ℕ → β
⊢ ∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x : { x // x ∈ m.toEnumFinset }, f (↑x).1 (↑x).2

Tactic:
rw [← m.toEnumFinset.prod_coe_sort fun x ↦ f x.1 x.2]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean
theorem factors_prod {a : α} (ane0 : a ≠ 0) : Associated (factors a).prod a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Classical.choose ⋯).prod ~ᵤ a

Tactic:
exact (Classical.choose_spec (exists_prime_factors a ane0)).2

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (factors a).prod ~ᵤ a

Tactic:
rw [factors, dif_neg ane0]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ane0 : a ≠ 0
⊢ (Classical.choose ⋯).prod ~ᵤ a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem two_mul {x : BitVec w} : 2#w * x = x + x

Proof state:
w : Nat
x : BitVec w
⊢ 2#w * x = x + x

Tactic:
rw [BitVec.mul_comm, mul_two]

Result:
no goals
-- Mathlib/Data/List/Nodup.lean
theorem Nodup.diff_eq_filter [BEq α] [LawfulBEq α] :
    ∀ {l₁ l₂ : List α} (_ : l₁.Nodup), l₁.diff l₂ = l₁.filter (· ∉ l₂)
  | l₁, [], _ => by simp
  | l₁, a :: l₂, hl₁ => by
    rw [diff_cons, (hl₁.erase _).diff_eq_filter, hl₁.erase_eq_filter, filter_filter]
    simp only [decide_not, bne, Bool.and_comm, mem_cons, not_or, decide_mem_cons, Bool.not_or]

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : l₁.Nodup
⊢ List.filter (fun a_1 => decide (a_1 ∉ l₂) && a_1 != a) l₁ = List.filter (fun x => decide (x ∉ a :: l₂)) l₁

Tactic:
simp only [decide_not, bne, Bool.and_comm, mem_cons, not_or, decide_mem_cons, Bool.not_or]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
x✝ : l₁.Nodup
⊢ l₁.diff [] = List.filter (fun x => decide (x ∉ [])) l₁

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : l₁.Nodup
⊢ l₁.diff (a :: l₂) = List.filter (fun x => decide (x ∉ a :: l₂)) l₁

Tactic:
rw [diff_cons, (hl₁.erase _).diff_eq_filter, hl₁.erase_eq_filter, filter_filter]

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : l₁.Nodup
⊢ List.filter (fun a_1 => decide (a_1 ∉ l₂) && a_1 != a) l₁ = List.filter (fun x => decide (x ∉ a :: l₂)) l₁
-- Mathlib/Topology/Separation/Basic.lean
theorem isClosed_setOf_specializes : IsClosed { p : X × X | p.1 ⤳ p.2 }

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ IsClosed {p | p.1 ⤳ p.2}

Tactic:
simp only [← isOpen_compl_iff, compl_setOf, ← disjoint_nhds_nhds_iff_not_specializes,
  isOpen_setOf_disjoint_nhds_nhds]

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
@[simp] lemma strongConvexOn_zero : StrongConvexOn s 0 f ↔ ConvexOn ℝ s f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
f : E → ℝ
⊢ StrongConvexOn s 0 f ↔ ConvexOn ℝ s f

Tactic:
simp [StrongConvexOn, ← Pi.zero_def]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
theorem prod_le_borel_prod : Prod.instMeasurableSpace ≤ borel (α × β)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : TopologicalSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ MeasurableSpace.comap Prod.snd (borel β) ≤ borel (α × β)

Tactic:
exact comap_le_iff_le_map.mpr continuous_snd.borel_measurable

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : TopologicalSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ MeasurableSpace.comap Prod.fst (borel α) ≤ borel (α × β)

Tactic:
exact comap_le_iff_le_map.mpr continuous_fst.borel_measurable

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : TopologicalSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ Prod.instMeasurableSpace ≤ borel (α × β)

Tactic:
refine sup_le ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : TopologicalSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ MeasurableSpace.comap Prod.fst (borel α) ≤ borel (α × β)

case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : TopologicalSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ MeasurableSpace.comap Prod.snd (borel β) ≤ borel (α × β)
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem toQuadraticForm' [DecidableEq n] {M : Matrix n n ℝ} (hM : M.PosDef) :
    M.toQuadraticMap'.PosDef

Proof state:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosDef
x : n → ℝ
hx : x ≠ 0
⊢ 0 < x ⬝ᵥ M *ᵥ x

Tactic:
apply hM.2 x hx

Result:
no goals

Proof state:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosDef
x : n → ℝ
hx : x ≠ 0
⊢ 0 < M.toQuadraticMap' x

Tactic:
simp only [Matrix.toQuadraticMap', LinearMap.BilinMap.toQuadraticMap_apply,
  toLinearMap₂'_apply']

Result:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosDef
x : n → ℝ
hx : x ≠ 0
⊢ 0 < x ⬝ᵥ M *ᵥ x

Proof state:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosDef
⊢ M.toQuadraticMap'.PosDef

Tactic:
intro x hx

Result:
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n ℝ
hM : M.PosDef
x : n → ℝ
hx : x ≠ 0
⊢ 0 < M.toQuadraticMap' x
-- Mathlib/Data/Num/Lemmas.lean
theorem castNum_or : ∀ m n : Num, ↑(m ||| n) = (↑m ||| ↑n : ℕ)

Proof state:
⊢ ∀ (m n : Num), ↑(m ||| n) = ↑m ||| ↑n

Tactic:
apply castNum_eq_bitwise fun x y => pos (PosNum.lor x y) <;>
 intros <;> (try cases_type* Bool) <;> rfl

Result:
no goals

Proof state:
case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ pos ((PosNum.bit a✝ m✝).lor (PosNum.bit b✝ n✝)) = bit (a✝ || b✝) (pos (m✝.lor n✝))

Tactic:
cases_type* Bool

Result:
case pbb.false.false
m✝ n✝ : PosNum
⊢ pos ((PosNum.bit false m✝).lor (PosNum.bit false n✝)) = bit (false || false) (pos (m✝.lor n✝))

case pbb.false.true
m✝ n✝ : PosNum
⊢ pos ((PosNum.bit false m✝).lor (PosNum.bit true n✝)) = bit (false || true) (pos (m✝.lor n✝))

case pbb.true.false
m✝ n✝ : PosNum
⊢ pos ((PosNum.bit true m✝).lor (PosNum.bit false n✝)) = bit (true || false) (pos (m✝.lor n✝))

case pbb.true.true
m✝ n✝ : PosNum
⊢ pos ((PosNum.bit true m✝).lor (PosNum.bit true n✝)) = bit (true || true) (pos (m✝.lor n✝))

Proof state:
case pbb
a✝ b✝ : Bool
m✝ n✝ : PosNum
⊢ pos ((PosNum.bit a✝ m✝).lor (PosNum.bit b✝ n✝)) = bit (a✝ || b✝) (pos (m✝.lor n✝))

Tactic:
try cases_type* Bool

Result:
case pbb.false.false
m✝ n✝ : PosNum
⊢ pos ((PosNum.bit false m✝).lor (PosNum.bit false n✝)) = bit (false || false) (pos (m✝.lor n✝))

case pbb.false.true
m✝ n✝ : PosNum
⊢ pos ((PosNum.bit false m✝).lor (PosNum.bit true n✝)) = bit (false || true) (pos (m✝.lor n✝))

case pbb.true.false
m✝ n✝ : PosNum
⊢ pos ((PosNum.bit true m✝).lor (PosNum.bit false n✝)) = bit (true || false) (pos (m✝.lor n✝))

case pbb.true.true
m✝ n✝ : PosNum
⊢ pos ((PosNum.bit true m✝).lor (PosNum.bit true n✝)) = bit (true || true) (pos (m✝.lor n✝))
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem inv_sub_inv {A B : Matrix n n α} (h : IsUnit A ↔ IsUnit B) :
    A⁻¹ - B⁻¹ = A⁻¹ * (B - A) * B⁻¹

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

Tactic:
simpa only [nonsing_inv_eq_ring_inverse] using Ring.inverse_sub_inverse h

Result:
no goals
-- Mathlib/Data/Int/Cast/Lemmas.lean
@[simp] lemma _root_.zsmul_eq_mul (a : α) : ∀ n : ℤ, n • a = n * a
  | (n : ℕ) => by rw [natCast_zsmul, nsmul_eq_mul, Int.cast_natCast]
  | -[n+1] => by simp [Nat.cast_succ, neg_add_rev, Int.cast_negSucc, add_mul]

Proof state:
α : Type u_3
inst✝ : NonAssocRing α
a : α
n : ℕ
⊢ ↑n • a = ↑↑n * a

Tactic:
rw [natCast_zsmul, nsmul_eq_mul, Int.cast_natCast]

Result:
no goals

Proof state:
α : Type u_3
inst✝ : NonAssocRing α
a : α
n : ℕ
⊢ -[n+1] • a = ↑-[n+1] * a

Tactic:
simp [Nat.cast_succ, neg_add_rev, Int.cast_negSucc, add_mul]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem eq_natCast_sub_of_add_eq_natCast {x y : PartENat} {n : ℕ} (h : x + y = n) :
    x = ↑(n - y.get (dom_of_le_natCast ((le_add_left le_rfl).trans_eq h)))

Proof state:
case intro
y : PartENat
n x : ℕ
h : ↑x + y = ↑n
⊢ ↑x = ↑(n - y.get ⋯)

Tactic:
lift y to ℕ using dom_of_le_natCast ((le_add_left le_rfl).trans_eq h)

Result:
case intro.intro
n x y : ℕ
h : ↑x + ↑y = ↑n
⊢ ↑x = ↑(n - (↑y).get ⋯)

Proof state:
x y : PartENat
n : ℕ
h : x + y = ↑n
⊢ x = ↑(n - y.get ⋯)

Tactic:
lift x to ℕ using dom_of_le_natCast ((le_add_right le_rfl).trans_eq h)

Result:
case intro
y : PartENat
n x : ℕ
h : ↑x + y = ↑n
⊢ ↑x = ↑(n - y.get ⋯)

Proof state:
case intro.intro
n x y : ℕ
h : ↑x + ↑y = ↑n
⊢ ↑x = ↑(n - (↑y).get ⋯)

Tactic:
rw [← Nat.cast_add, natCast_inj] at h

Result:
case intro.intro
n x y : ℕ
h✝ : ↑x + ↑y = ↑n
h : x + y = n
⊢ ↑x = ↑(n - (↑y).get ⋯)

Proof state:
case intro.intro
n x y : ℕ
h✝ : ↑x + ↑y = ↑n
h : x + y = n
⊢ ↑x = ↑(n - (↑y).get ⋯)

Tactic:
rw [get_natCast, natCast_inj, eq_tsub_of_add_eq h]

Result:
no goals
-- Mathlib/Data/Int/Order/Units.lean
theorem units_pow_eq_pow_mod_two (u : ℤˣ) (n : ℕ) : u ^ n = u ^ (n % 2)

Proof state:
u : ℤˣ
n : ℕ
⊢ u ^ n = u ^ (n % 2)

Tactic:
conv =>
  lhs
  rw [← Nat.mod_add_div n 2]
  rw [pow_add, pow_mul, units_sq, one_pow, mul_one]

Result:
no goals