harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_prod {s : Set α} {t : Set β} :
    MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

Proof state:
case inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
h : (s ×ˢ t).Nonempty
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

Tactic:
simp [← not_nonempty_iff_eq_empty, prod_nonempty_iff.mp h, measurableSet_prod_of_nonempty h]

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
h : s ×ˢ t = ∅
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

Tactic:
simp [h, prod_eq_empty_iff.mp h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

Tactic:
rcases (s ×ˢ t).eq_empty_or_nonempty with h | h

Result:
case inl
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
h : s ×ˢ t = ∅
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

case inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
h : (s ×ˢ t).Nonempty
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem forall_mem_flatMap {p : β → Prop} {l : List α} {f : α → List β} :
    (∀ (x) (_ : x ∈ l.flatMap f), p x) ↔ ∀ (a) (_ : a ∈ l) (b) (_ : b ∈ f a), p b

Proof state:
case mpr
β : Type u_1
α : Type u_2
p : β → Prop
l : List α
f : α → List β
⊢ (∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b) → ∀ (x : β) (x_1 : α), x_1 ∈ l → x ∈ f x_1 → p x

Tactic:
intros

Result:
case mpr
β : Type u_1
α : Type u_2
p : β → Prop
l : List α
f : α → List β
a✝² : ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b
x✝¹ : β
x✝ : α
a✝¹ : x✝ ∈ l
a✝ : x✝¹ ∈ f x✝
⊢ p x✝¹

Proof state:
β : Type u_1
α : Type u_2
p : β → Prop
l : List α
f : α → List β
⊢ (∀ (x : β) (x_1 : α), x_1 ∈ l → x ∈ f x_1 → p x) ↔ ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b

Tactic:
constructor <;> (intros; solve_by_elim)

Result:
no goals

Proof state:
case mpr
β : Type u_1
α : Type u_2
p : β → Prop
l : List α
f : α → List β
a✝² : ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b
x✝¹ : β
x✝ : α
a✝¹ : x✝ ∈ l
a✝ : x✝¹ ∈ f x✝
⊢ p x✝¹

Tactic:
solve_by_elim

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
p : β → Prop
l : List α
f : α → List β
⊢ (∀ (x : β), x ∈ flatMap f l → p x) ↔ ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b

Tactic:
simp only [mem_flatMap, forall_exists_index, and_imp]

Result:
β : Type u_1
α : Type u_2
p : β → Prop
l : List α
f : α → List β
⊢ (∀ (x : β) (x_1 : α), x_1 ∈ l → x ∈ f x_1 → p x) ↔ ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b
-- Mathlib/Data/Bool/Basic.lean
theorem eq_false_eq_not_eq_true (b : Bool) : (¬b = true) = (b = false)

Proof state:
b : Bool
⊢ (¬b = true) = (b = false)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Sheaves/Presheaf.lean
theorem pushforwardToOfIso_app {X Y : TopCat} (H₁ : X ≅ Y) {ℱ : Y.Presheaf C} {𝒢 : X.Presheaf C}
    (H₂ : ℱ ⟶ H₁.hom _* 𝒢) (U : (Opens X)ᵒᵖ) :
    (pushforwardToOfIso H₁ H₂).app U =
      H₂.app (op ((Opens.map H₁.inv).obj (unop U))) ≫
        𝒢.map (eqToHom (by simp [Opens.map, Set.preimage_preimage]))

Proof state:
C✝ : Type u
inst✝³ : Category.{v, u} C✝
X✝ : TopCat
C : Type u_1
inst✝² : Category.{?u.69489, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C Y
𝒢 : Presheaf C X
H₂ : ℱ ⟶ (pushforward C H₁.hom).obj 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ (Opens.map H₁.hom).op.obj (op ((Opens.map H₁.inv).obj (unop U))) = U

Tactic:
simp [Opens.map, Set.preimage_preimage]

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_5, u_1} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C Y
𝒢 : Presheaf C X
H₂ : ℱ ⟶ (pushforward C H₁.hom).obj 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ (pushforwardToOfIso H₁ H₂).app U = H₂.app (op ((Opens.map H₁.inv).obj (unop U))) ≫ 𝒢.map (eqToHom ⋯)

Tactic:
simp [pushforwardToOfIso, Equivalence.toAdjunction, Adjunction.homEquiv_counit]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem dotProduct_single (x : α) (i : m) : v ⬝ᵥ Pi.single i x = v i * x

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → v j * Pi.single i x j = 0
⊢ v ⬝ᵥ Pi.single i x = v i * x

Tactic:
convert Finset.sum_eq_single i (fun j _ => this j) _ using 1 <;> simp

Result:
no goals

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i j : m
hij : j ≠ i
⊢ v j * Pi.single i x j = 0

Tactic:
simp [Pi.single_eq_of_ne hij]

Result:
no goals

Proof state:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
⊢ v ⬝ᵥ Pi.single i x = v i * x

Tactic:
have : ∀ j ≠ i, v j * Pi.single (f := fun _ => α) i x j = 0 := fun j hij => by
  simp [Pi.single_eq_of_ne hij]

Result:
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i : m
this : ∀ (j : m), j ≠ i → v j * Pi.single i x j = 0
⊢ v ⬝ᵥ Pi.single i x = v i * x
-- Mathlib/FieldTheory/Separable.lean
theorem separable_prod_X_sub_C_iff {ι : Sort _} [Fintype ι] {f : ι → F} :
    (∏ i, (X - C (f i))).Separable ↔ Function.Injective f :=
  separable_prod_X_sub_C_iff'.trans <| by simp_rw [mem_univ, true_imp_iff, Function.Injective]

Proof state:
F : Type u
inst✝¹ : Field F
ι : Type u_1
inst✝ : Fintype ι
f : ι → F
⊢ (∀ x ∈ univ, ∀ y ∈ univ, f x = f y → x = y) ↔ Function.Injective f

Tactic:
simp_rw [mem_univ, true_imp_iff, Function.Injective]

Result:
no goals
-- Mathlib/Algebra/Module/FinitePresentation.lean
lemma Module.FinitePresentation.exists_lift_of_isLocalizedModule
    [h : Module.FinitePresentation R M] (g : M →ₗ[R] N') :
    ∃ (h : M →ₗ[R] N) (s : S), f ∘ₗ h = s • g

Proof state:
case mk.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset ({ x // x ∈ σ } →₀ R)
hτ : Submodule.span R ↑τ = LinearMap.ker (linearCombination R Subtype.val)
π : ({ x // x ∈ σ } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : { x // x ∈ σ } → N := fun x => (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
⊢ ∃ h s, f ∘ₗ h = s • g

Tactic:
have hi : f ∘ₗ Finsupp.linearCombination R i = (s₀ • g) ∘ₗ π := by
  ext j
  simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply,
    linearCombination_single, one_smul, LinearMap.map_smul_of_tower, ← hs, LinearMap.smul_apply,
    i, s₀, π]
  rw [← mul_smul, Finset.prod_erase_mul]
  exact j.prop

Result:
case mk.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset ({ x // x ∈ σ } →₀ R)
hτ : Submodule.span R ↑τ = LinearMap.ker (linearCombination R Subtype.val)
π : ({ x // x ∈ σ } →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
s : N' → N × ↥S
hs : ∀ (y : N'), (s y).2 • y = f (s y).1
i : { x // x ∈ σ } → N := fun x => (∏ j ∈ σ.erase ↑x, (s (g j)).2) • (s (g ↑x)).1
s₀ : ↥S := ∏ j ∈ σ, (s (g j)).2
hi : f ∘ₗ linearCombination R i = (s₀ • g) ∘ₗ π
⊢ ∃ h s, f ∘ₗ h = s • g
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem admissible_flatOrder (P : FlatOrder b → Prop) (hnot : P b) : admissible P

Proof state:
case pos
α : Sort u
b : α
P : FlatOrder b → Prop
hnot : P b
c : FlatOrder b → Prop
hchain : chain c
h : ∀ (x : FlatOrder b), c x → P x
h' : ∃ x, c x ∧ x ≠ b
⊢ ∀ (a : FlatOrder b), c a ∧ ¬a = b → P a

Tactic:
intro x ⟨hcx, hneb⟩

Result:
case pos
α : Sort u
b : α
P : FlatOrder b → Prop
hnot : P b
c : FlatOrder b → Prop
hchain : chain c
h : ∀ (x : FlatOrder b), c x → P x
h' : ∃ x, c x ∧ x ≠ b
x : FlatOrder b
hcx : c x
hneb : ¬x = b
⊢ P x

Proof state:
case pos
α : Sort u
b : α
P : FlatOrder b → Prop
hnot : P b
c : FlatOrder b → Prop
hchain : chain c
h : ∀ (x : FlatOrder b), c x → P x
h' : ∃ x, c x ∧ x ≠ b
⊢ P (CCPO.csup c)

Tactic:
simp [CCPO.csup, flat_csup, h']

Result:
case pos
α : Sort u
b : α
P : FlatOrder b → Prop
hnot : P b
c : FlatOrder b → Prop
hchain : chain c
h : ∀ (x : FlatOrder b), c x → P x
h' : ∃ x, c x ∧ x ≠ b
⊢ P (Classical.choose ⋯)

Proof state:
case pos
α : Sort u
b : α
P : FlatOrder b → Prop
hnot : P b
c : FlatOrder b → Prop
hchain : chain c
h : ∀ (x : FlatOrder b), c x → P x
h' : ∃ x, c x ∧ x ≠ b
x : FlatOrder b
hcx : c x
hneb : ¬x = b
⊢ P x

Tactic:
apply h x hcx

Result:
no goals

Proof state:
case neg
α : Sort u
b : α
P : FlatOrder b → Prop
hnot : P b
c : FlatOrder b → Prop
hchain : chain c
h : ∀ (x : FlatOrder b), c x → P x
h' : ¬∃ x, c x ∧ x ≠ b
⊢ P (CCPO.csup c)

Tactic:
simp [CCPO.csup, flat_csup, h', hnot]

Result:
no goals

Proof state:
α : Sort u
b : α
P : FlatOrder b → Prop
hnot : P b
⊢ admissible P

Tactic:
intro c hchain h

Result:
α : Sort u
b : α
P : FlatOrder b → Prop
hnot : P b
c : FlatOrder b → Prop
hchain : chain c
h : ∀ (x : FlatOrder b), c x → P x
⊢ P (CCPO.csup c)

Proof state:
α : Sort u
b : α
P : FlatOrder b → Prop
hnot : P b
c : FlatOrder b → Prop
hchain : chain c
h : ∀ (x : FlatOrder b), c x → P x
⊢ P (CCPO.csup c)

Tactic:
by_cases h' : ∃ (x : FlatOrder b), c x ∧ x ≠ b

Result:
case pos
α : Sort u
b : α
P : FlatOrder b → Prop
hnot : P b
c : FlatOrder b → Prop
hchain : chain c
h : ∀ (x : FlatOrder b), c x → P x
h' : ∃ x, c x ∧ x ≠ b
⊢ P (CCPO.csup c)

case neg
α : Sort u
b : α
P : FlatOrder b → Prop
hnot : P b
c : FlatOrder b → Prop
hchain : chain c
h : ∀ (x : FlatOrder b), c x → P x
h' : ¬∃ x, c x ∧ x ≠ b
⊢ P (CCPO.csup c)
-- Mathlib/Data/Finsupp/Single.lean
theorem card_support_le_one' [Nonempty α] {f : α →₀ M} :
    #f.support ≤ 1 ↔ ∃ a b, f = single a b

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : Nonempty α
f : α →₀ M
⊢ #f.support ≤ 1 ↔ ∃ a b, f = single a b

Tactic:
simp only [card_le_one_iff_subset_singleton, support_subset_singleton']

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
theorem finite_of_toPiLocalization_surjective
    (surj : Function.Surjective (toPiLocalization R)) :
    Finite (MaximalSpectrum R)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
surj✝ : Function.Surjective ⇑(toPiLocalization R)
surj : Function.Surjective (⇑(toPiLocalization (PiLocalization R)) ∘ ⇑(toPiLocalization R))
⊢ Finite (MaximalSpectrum R)

Tactic:
exact finite_of_toPiLocalization_pi_surjective surj.of_comp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
surj : Function.Surjective ⇑(toPiLocalization R)
⊢ Finite (MaximalSpectrum R)

Tactic:
replace surj := mapPiLocalization_bijective _ ⟨toPiLocalization_injective R, surj⟩
  |>.2.comp surj

Result:
R : Type u_1
inst✝ : CommSemiring R
surj✝ : Function.Surjective ⇑(toPiLocalization R)
surj : Function.Surjective (⇑(mapPiLocalization (toPiLocalization R) ⋯) ∘ ⇑(toPiLocalization R))
⊢ Finite (MaximalSpectrum R)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
surj✝ : Function.Surjective ⇑(toPiLocalization R)
surj : Function.Surjective (⇑(mapPiLocalization (toPiLocalization R) ⋯) ∘ ⇑(toPiLocalization R))
⊢ Finite (MaximalSpectrum R)

Tactic:
rw [← RingHom.coe_comp, mapPiLocalization_naturality, RingHom.coe_comp] at surj

Result:
R : Type u_1
inst✝ : CommSemiring R
surj✝ : Function.Surjective ⇑(toPiLocalization R)
surj : Function.Surjective (⇑(toPiLocalization (PiLocalization R)) ∘ ⇑(toPiLocalization R))
⊢ Finite (MaximalSpectrum R)
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem iso_symm_apply_aux (m : M') :
    (iso S f).symm m =
      LocalizedModule.mk (IsLocalizedModule.surj S f m).choose.1
        (IsLocalizedModule.surj S f m).choose.2

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M'
⊢ m = (iso S f) (LocalizedModule.mk ⋯.choose.1 ⋯.choose.2)

Tactic:
simp [iso, fromLocalizedModule, Module.End_algebraMap_isUnit_inv_apply_eq_iff',
  ← Submonoid.smul_def, (surj' _).choose_spec]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M'
⊢ (iso S f).symm m = LocalizedModule.mk ⋯.choose.1 ⋯.choose.2

Tactic:
apply_fun iso S f using LinearEquiv.injective (iso S f)

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M'
⊢ (iso S f) ((iso S f).symm m) = (iso S f) (LocalizedModule.mk ⋯.choose.1 ⋯.choose.2)

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M'
⊢ (iso S f) ((iso S f).symm m) = (iso S f) (LocalizedModule.mk ⋯.choose.1 ⋯.choose.2)

Tactic:
rw [LinearEquiv.apply_symm_apply]

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M'
⊢ m = (iso S f) (LocalizedModule.mk ⋯.choose.1 ⋯.choose.2)
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get?_inj
    (h₀ : i < xs.length) (h₁ : Nodup xs) (h₂ : xs.get? i = xs.get? j) : i = j

Proof state:
i : Nat
α✝ : Type u_1
xs : List α✝
j : Nat
h₀ : i < xs.length
h₁ : xs.Nodup
h₂ : xs.get? i = xs.get? j
⊢ i = j

Tactic:
apply getElem?_inj h₀ h₁

Result:
i : Nat
α✝ : Type u_1
xs : List α✝
j : Nat
h₀ : i < xs.length
h₁ : xs.Nodup
h₂ : xs.get? i = xs.get? j
⊢ xs[i]? = xs[j]?

Proof state:
i : Nat
α✝ : Type u_1
xs : List α✝
j : Nat
h₀ : i < xs.length
h₁ : xs.Nodup
h₂ : xs.get? i = xs.get? j
⊢ xs[i]? = xs[j]?

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem all_eq_false {p : α → Bool} {as : Array α} :
    as.all p = false ↔ ∃ (i : Nat) (_ : i < as.size), ¬p as[i]

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ (¬∀ (i : Nat) (x : i < as.size), p as[i] = true) ↔ ∃ i x, ¬p as[i] = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
as : Array α
⊢ as.all p = false ↔ ∃ i x, ¬p as[i] = true

Tactic:
rw [Bool.eq_false_iff, Ne, all_eq_true]

Result:
α : Type u_1
p : α → Bool
as : Array α
⊢ (¬∀ (i : Nat) (x : i < as.size), p as[i] = true) ↔ ∃ i x, ¬p as[i] = true
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem rTensor_refl_apply : (refl R N).rTensor M y = y

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
y : N ⊗[R] M
⊢ (rTensor M (refl R N)) y = y

Tactic:
rw [rTensor_refl, refl_apply]

Result:
no goals
-- Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
theorem sumIDeriv_apply_of_lt {p : R[X]} {n : ℕ} (hn : p.natDegree < n) :
    sumIDeriv p = ∑ i ∈ range n, derivative^[i] p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ (derivativeFinsupp p).support ⊆ range n

Tactic:
simp [hn]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ sumIDeriv p = ∑ i ∈ range n, (⇑derivative)^[i] p

Tactic:
dsimp [sumIDeriv]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ ((derivativeFinsupp p).sum fun i => id) = ∑ i ∈ range n, (⇑derivative)^[i] p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ ((derivativeFinsupp p).sum fun i => id) = ∑ i ∈ range n, (⇑derivative)^[i] p

Tactic:
exact Finsupp.sum_of_support_subset _ (by simp [hn]) _ (by simp)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
⊢ ∀ i ∈ range n, id 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem mem_direction_iff_eq_vsub {s : AffineSubspace k P} (h : (s : Set P).Nonempty) (v : V) :
    v ∈ s.direction ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂

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
h : (↑s).Nonempty
v : V
⊢ (∃ x ∈ ↑s, ∃ y ∈ ↑s, x -ᵥ y = v) ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂

Tactic:
simp only [SetLike.mem_coe, eq_comm]

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
h : (↑s).Nonempty
v : V
⊢ v ∈ s.direction ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂

Tactic:
rw [← SetLike.mem_coe, coe_direction_eq_vsub_set h, Set.mem_vsub]

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
h : (↑s).Nonempty
v : V
⊢ (∃ x ∈ ↑s, ∃ y ∈ ↑s, x -ᵥ y = v) ↔ ∃ p₁ ∈ s, ∃ p₂ ∈ s, v = p₁ -ᵥ p₂
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem strictMono_iff_map_pos :
    StrictMono (f : α → β) ↔ ∀ a, 0 < a → 0 < f a

Proof state:
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
inst✝ : AddLeftStrictMono β
h : ∀ (a : α), 0 < a → 0 < f a
a b : α
hl : a < b
⊢ f a < f (b - a) + f a

Tactic:
exact lt_add_of_pos_left _ (h _ <| sub_pos.2 hl)

Result:
no goals

Proof state:
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
inst✝ : AddLeftStrictMono β
h : StrictMono ⇑f
a : α
⊢ 0 < a → f 0 < f a

Tactic:
apply h

Result:
no goals

Proof state:
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
inst✝ : AddLeftStrictMono β
h : StrictMono ⇑f
a : α
⊢ 0 < a → 0 < f a

Tactic:
rw [← map_zero f]

Result:
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
inst✝ : AddLeftStrictMono β
h : StrictMono ⇑f
a : α
⊢ 0 < a → f 0 < f a

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
inst✝ : AddLeftStrictMono β
⊢ StrictMono ⇑f ↔ ∀ (a : α), 0 < a → 0 < f a

Tactic:
refine ⟨fun h a => ?_, fun h a b hl => ?_⟩

Result:
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
inst✝ : AddLeftStrictMono β
h : StrictMono ⇑f
a : α
⊢ 0 < a → 0 < f a

case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
inst✝ : AddLeftStrictMono β
h : ∀ (a : α), 0 < a → 0 < f a
a b : α
hl : a < b
⊢ f a < f b

Proof state:
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
inst✝ : AddLeftStrictMono β
h : ∀ (a : α), 0 < a → 0 < f a
a b : α
hl : a < b
⊢ f a < f b

Tactic:
rw [← sub_add_cancel b a, map_add f]

Result:
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
inst✝ : AddLeftStrictMono β
h : ∀ (a : α), 0 < a → 0 < f a
a b : α
hl : a < b
⊢ f a < f (b - a) + f a
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_le_iff_dvd {d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) :
    d.factorization ≤ n.factorization ↔ d ∣ n

Proof state:
case mp
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : d.factorization ≤ n.factorization
⊢ d ∣ n

Tactic:
set K := n.factorization - d.factorization with hK

Result:
case mp
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : d.factorization ≤ n.factorization
K : ℕ →₀ ℕ := n.factorization - d.factorization
hK : K = n.factorization - d.factorization
⊢ d ∣ n

Proof state:
case h
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : d.factorization ≤ n.factorization
K : ℕ →₀ ℕ := n.factorization - d.factorization
hK : K = n.factorization - d.factorization
⊢ n = d * K.prod fun x1 x2 => x1 ^ x2

Tactic:
rw [← factorization_prod_pow_eq_self hn, ← factorization_prod_pow_eq_self hd,
    ← Finsupp.prod_add_index' pow_zero pow_add, hK, add_tsub_cancel_of_le hdn]

Result:
no goals

Proof state:
case mpr.intro
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
⊢ d.factorization ≤ d.factorization + c.factorization

Tactic:
simp

Result:
no goals

Proof state:
case mp
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d.factorization ≤ n.factorization → d ∣ n

Tactic:
intro hdn

Result:
case mp
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
hdn : d.factorization ≤ n.factorization
⊢ d ∣ n

Proof state:
case mpr
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d ∣ n → d.factorization ≤ n.factorization

Tactic:
rintro ⟨c, rfl⟩

Result:
case mpr.intro
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
⊢ d.factorization ≤ (d * c).factorization

Proof state:
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d.factorization ≤ n.factorization ↔ d ∣ n

Tactic:
constructor

Result:
case mp
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d.factorization ≤ n.factorization → d ∣ n

case mpr
d n : ℕ
hd : d ≠ 0
hn : n ≠ 0
⊢ d ∣ n → d.factorization ≤ n.factorization

Proof state:
case mpr.intro
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
⊢ d.factorization ≤ (d * c).factorization

Tactic:
rw [factorization_mul hd (right_ne_zero_of_mul hn)]

Result:
case mpr.intro
d : ℕ
hd : d ≠ 0
c : ℕ
hn : d * c ≠ 0
⊢ d.factorization ≤ d.factorization + c.factorization
-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuous_iSup {f : ι → α → δ} (h : ∀ i, LowerSemicontinuous (f i)) :
    LowerSemicontinuous fun x' => ⨆ i, f i x' :=
  lowerSemicontinuous_ciSup (by simp) h

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Sort u_3
δ : Type u_4
inst✝ : CompleteLinearOrder δ
f : ι → α → δ
h : ∀ (i : ι), LowerSemicontinuous (f i)
⊢ ∀ (x : α), BddAbove (range fun i => f i x)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Card.lean
/-- We can shrink a set to any smaller size. -/
lemma exists_subset_card_eq {n : ℕ} (hns : n ≤ s.ncard) : ∃ t ⊆ s, t.ncard = n

Proof state:
α : Type u_1
s : Set α
n : ℕ
hns : n ≤ s.ncard
⊢ ∃ t ⊆ s, t.ncard = n

Tactic:
simpa using exists_subsuperset_card_eq s.empty_subset (by simp) hns

Result:
no goals

Proof state:
α : Type u_1
s : Set α
n : ℕ
hns : n ≤ s.ncard
⊢ ∅.ncard ≤ n

Tactic:
simp

Result:
no goals