harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Sum/Interval.lean
theorem sumLift₂_nonempty :
    (sumLift₂ f g a b).Nonempty ↔
      (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ (f a₁ b₁).Nonempty) ∨
        ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ (g a₂ b₂).Nonempty

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁ ⊕ α₂
b : β₁ ⊕ β₂
⊢ (sumLift₂ f g a b).Nonempty ↔
    (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ (f a₁ b₁).Nonempty) ∨ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ (g a₂ b₂).Nonempty

Tactic:
simp only [nonempty_iff_ne_empty, Ne, sumLift₂_eq_empty, not_and_or, not_forall, exists_prop]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma inter_pow_subset : (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

Tactic:
apply subset_inter <;> gcongr <;> simp

Result:
no goals
-- Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean
theorem not_mem_maximalIdeal {x : R} : x ∉ maximalIdeal R ↔ IsUnit x

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsLocalRing R
x : R
⊢ x ∉ maximalIdeal R ↔ IsUnit x

Tactic:
simp only [mem_maximalIdeal, mem_nonunits_iff, not_not]

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

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

Tactic:
exact Real.sin_pi_div_two_sub _

Result:
no goals

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

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ (↑(π / 2) - ↑x✝).sin = (↑x✝).cos
-- Mathlib/GroupTheory/GroupExtension/Basic.lean
theorem refl (s : S.Splitting) : S.IsConj s s :=
  ⟨1, by simp only [map_one, inv_one, one_mul, mul_one]⟩

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s : S.Splitting
⊢ ⇑s = fun g => S.inl 1 * s g * (S.inl 1)⁻¹

Tactic:
simp only [map_one, inv_one, one_mul, mul_one]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem cycleRange_symm_succ {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
    i.cycleRange.symm j.succ = i.succAbove j :=
  i.cycleRange.injective (by simp)

Proof state:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ i.cycleRange ((Equiv.symm i.cycleRange) j.succ) = i.cycleRange (i.succAbove j)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem mul_lt_iff_lt_one_right [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) :
    a * b < a ↔ b < 1 :=
  Iff.trans (by rw [mul_one]) (mul_lt_mul_left a0)

Proof state:
α : Type u_3
a b : α
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : PosMulStrictMono α
inst✝ : PosMulReflectLT α
a0 : 0 < a
⊢ a * b < a ↔ a * b < a * 1

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Linearity.lean
@[simp]
lemma LSeries_smul (f : ℕ → ℂ) (c s : ℂ) : LSeries (c • f) s = c * LSeries f s

Proof state:
f : ℕ → ℂ
c s : ℂ
⊢ LSeries (c • f) s = c * LSeries f s

Tactic:
simp [LSeries, term_smul_apply, tsum_mul_left]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_mul_distrib' (hf : (s ∩ mulSupport f).Finite) (hg : (s ∩ mulSupport g).Finite) :
    ∏ᶠ i ∈ s, f i * g i = (∏ᶠ i ∈ s, f i) * ∏ᶠ i ∈ s, g i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
s : Set α
hf : (s ∩ mulSupport f).Finite
hg : (s ∩ mulSupport g).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i

Tactic:
rw [← mulSupport_mulIndicator] at hf hg

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
s : Set α
hf : (mulSupport (s.mulIndicator f)).Finite
hg : (mulSupport (s.mulIndicator g)).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f g : α → M
s : Set α
hf : (mulSupport (s.mulIndicator f)).Finite
hg : (mulSupport (s.mulIndicator g)).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i

Tactic:
simp only [finprod_mem_def, mulIndicator_mul, finprod_mul_distrib hf hg]

Result:
no goals
-- Mathlib/Tactic/Positivity/Basic.lean
private lemma ite_nonneg [LE α] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ ite p a b

Proof state:
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ if p then a else b

Tactic:
by_cases p <;> simp [*]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem finiteIndex_iInf' {ι : Type*} {s : Finset ι}
    (f : ι → Subgroup G) (hs : ∀ i ∈ s, (f i).FiniteIndex) :
    (⨅ i ∈ s, f i).FiniteIndex

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_3
s : Finset ι
f : ι → Subgroup G
hs : ∀ i ∈ s, (f i).FiniteIndex
⊢ (⨅ x, f ↑x).FiniteIndex

Tactic:
exact finiteIndex_iInf fun ⟨i, hi⟩ => hs i hi

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_3
s : Finset ι
f : ι → Subgroup G
hs : ∀ i ∈ s, (f i).FiniteIndex
⊢ (⨅ i ∈ s, f i).FiniteIndex

Tactic:
rw [iInf_subtype']

Result:
G : Type u_1
inst✝ : Group G
ι : Type u_3
s : Finset ι
f : ι → Subgroup G
hs : ∀ i ∈ s, (f i).FiniteIndex
⊢ (⨅ x, f ↑x).FiniteIndex
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = (x / z) + 1

Proof state:
x z : Nat
H : 0 < z
⊢ (z + x) / z = x / z + 1

Tactic:
rw [Nat.add_comm, add_div_right x H]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem disjoint_of_subset_iff_left_eq_empty (h : s ⊆ t) :
    Disjoint s t ↔ s = ∅

Proof state:
α : Type u
s t : Set α
h : s ⊆ t
⊢ Disjoint s t ↔ s = ∅

Tactic:
simp only [disjoint_iff, inf_eq_left.mpr h, bot_eq_empty]

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.translate_left (hf : ConvexOn 𝕜 s f) (c : E) :
    ConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
c : E
⊢ ConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)

Tactic:
simpa only [add_comm c] using hf.translate_right c

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
/-- See also `Function.injective_iff_pairwise_ne` -/
lemma injOn_iff_pairwise_ne {s : Set ι} : InjOn f s ↔ s.Pairwise (f · ≠ f ·)

Proof state:
α : Type u_1
ι : Type u_4
f : ι → α
s : Set ι
⊢ InjOn f s ↔ s.Pairwise fun x1 x2 => f x1 ≠ f x2

Tactic:
simp only [InjOn, Set.Pairwise, not_imp_not]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem readyForRatAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
    ReadyForRatAdd f → ReadyForRatAdd (insert f c)

Proof state:
case left
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.ReadyForRatAdd
⊢ (f.insert c).ratUnits = #[]

Tactic:
simp only [insert, h.1] <;> split <;> rfl

Result:
no goals

Proof state:
case right
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.ReadyForRatAdd
⊢ (f.insert c).ReadyForRupAdd

Tactic:
exact readyForRupAdd_insert f c h.2

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ f.ReadyForRatAdd → (f.insert c).ReadyForRatAdd

Tactic:
intro h

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.ReadyForRatAdd
⊢ (f.insert c).ReadyForRatAdd

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.ReadyForRatAdd
⊢ (f.insert c).ReadyForRatAdd

Tactic:
constructor

Result:
case left
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.ReadyForRatAdd
⊢ (f.insert c).ratUnits = #[]

case right
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.ReadyForRatAdd
⊢ (f.insert c).ReadyForRupAdd
-- Mathlib/Algebra/Vertex/VertexOperator.lean
theorem coeff_eq_ncoeff (A : VertexOperator R V)
    (n : ℤ) : HVertexOperator.coeff A n = A [[-n - 1]]

Proof state:
R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
⊢ coeff A n = A[[-n - 1]]

Tactic:
rw [ncoeff, neg_sub, sub_neg_eq_add, add_sub_cancel_left]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem biUnion_and (p : ι → Prop) (q : ι → ι' → Prop) (s : ∀ x y, p x ∧ q x y → Set α) :
    ⋃ (x : ι) (y : ι') (h : p x ∧ q x y), s x y h =
      ⋃ (x : ι) (hx : p x) (y : ι') (hy : q x y), s x y ⟨hx, hy⟩

Proof state:
α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p x ∧ q x y → Set α
⊢ ⋃ x, ⋃ y, ⋃ (h : p x ∧ q x y), s x y h = ⋃ x, ⋃ (hx : p x), ⋃ y, ⋃ (hy : q x y), s x y ⋯

Tactic:
simp only [iUnion_and, @iUnion_comm _ ι']

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem coe_pi_add_coe_pi : (π : Real.Angle) + π = 0

Proof state:
⊢ ↑π + ↑π = 0

Tactic:
rw [← two_nsmul, two_nsmul_coe_pi]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
lemma MemLp.integrable_norm_pow' [IsFiniteMeasure μ] {f : α → β} {p : ℕ} (hf : MemLp f p μ) :
    Integrable (fun x : α => ‖f x‖ ^ p) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
p : ℕ
hf : MemLp f (↑p) μ
⊢ Integrable (fun x => ‖f x‖ ^ p) μ

Tactic:
simpa using hf.integrable_norm_rpow'

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma succ_injective (n : ℕ) : Injective (@Fin.succ n) := fun a b ↦ by simp [Fin.ext_iff]

Proof state:
n : ℕ
a b : Fin n
⊢ a.succ = b.succ → a = b

Tactic:
simp [Fin.ext_iff]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Bell.lean
theorem uniformBell_one_right (m : ℕ) : uniformBell m 1 = 1

Proof state:
m : ℕ
⊢ m.uniformBell 1 = 1

Tactic:
simp only [uniformBell_eq, mul_one, add_tsub_cancel_right, ge_iff_le, le_refl,
  tsub_eq_zero_of_le, choose_zero_right, Finset.prod_const_one]

Result:
no goals
-- Mathlib/Data/List/Sym.lean
theorem sym_one_eq : xs.sym 1 = xs.map (· ::ₛ .nil)

Proof state:
case cons
α : Type u_1
xs✝ : List α
x : α
xs : List α
ih : List.sym 1 xs = map (fun x => x ::ₛ Sym.nil) xs
⊢ List.sym 1 (x :: xs) = map (fun x => x ::ₛ Sym.nil) (x :: xs)

Tactic:
rw [map_cons, ← ih, List.sym, List.sym, map_singleton, singleton_append]

Result:
no goals

Proof state:
α : Type u_1
xs : List α
⊢ List.sym 1 xs = map (fun x => x ::ₛ Sym.nil) xs

Tactic:
induction xs with
| nil => simp only [List.sym, Nat.succ_eq_add_one, Nat.reduceAdd, map_nil]
| cons x xs ih =>
  rw [map_cons, ← ih, List.sym, List.sym, map_singleton, singleton_append]

Result:
no goals

Proof state:
case nil
α : Type u_1
xs : List α
⊢ List.sym 1 [] = map (fun x => x ::ₛ Sym.nil) []

Tactic:
simp only [List.sym, Nat.succ_eq_add_one, Nat.reduceAdd, map_nil]

Result:
no goals
-- Mathlib/Order/Chain.lean
theorem chainClosure_empty : ChainClosure r ∅

Proof state:
α : Type u_1
r : α → α → Prop
this : ChainClosure r (⋃₀ ∅)
⊢ ChainClosure r ∅

Tactic:
simpa using this

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
⊢ ChainClosure r ∅

Tactic:
have : ChainClosure r (⋃₀∅) := ChainClosure.union fun a h => (not_mem_empty _ h).elim

Result:
α : Type u_1
r : α → α → Prop
this : ChainClosure r (⋃₀ ∅)
⊢ ChainClosure r ∅
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
theorem quasispectrumRestricts_iff_spectrumRestricts_inr (S : Type*) {R A : Type*} [Semifield R]
    [Field S] [NonUnitalRing A] [Algebra R S] [Module R A] [Module S A] [IsScalarTower S A A]
    [SMulCommClass S A A] [IsScalarTower R S A] {a : A} {f : S → R} :
    QuasispectrumRestricts a f ↔ SpectrumRestricts (a : Unitization S A) f

Proof state:
S : Type u_3
R : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module R A
inst✝³ : Module S A
inst✝² : IsScalarTower S A A
inst✝¹ : SMulCommClass S A A
inst✝ : IsScalarTower R S A
a : A
f : S → R
⊢ QuasispectrumRestricts a f ↔ SpectrumRestricts (↑a) f

Tactic:
rw [quasispectrumRestricts_iff, spectrumRestricts_iff,
  ← Unitization.quasispectrum_eq_spectrum_inr']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_empty {a : α} {c} : get? (empty c : Raw α (fun _ => β)) a = none

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
a : α
c : Nat
⊢ get? (empty c) a = none

Tactic:
simp_to_raw using Raw₀.Const.get?_empty

Result:
no goals
-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem Cofix.dest_corec₁ {α : TypeVec n} {β : Type u}
    (g : ∀ {X}, (Cofix F α → X) → (β → X) → β → F (α.append1 X)) (x : β)
    (h : ∀ (X Y) (f : Cofix F α → X) (f' : β → X) (k : X → Y),
      g (k ∘ f) (k ∘ f') x = (id ::: k) <$$> g f f' x) :
    Cofix.dest (Cofix.corec₁ (@g) x) = g id (Cofix.corec₁ @g) x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x
⊢ (corec₁ g x).dest = g _root_.id (corec₁ g) x

Tactic:
rw [Cofix.corec₁, Cofix.dest_corec', ← h]

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x
⊢ g (Sum.elim _root_.id (corec' fun x => g Sum.inl Sum.inr x) ∘ Sum.inl)
      (Sum.elim _root_.id (corec' fun x => g Sum.inl Sum.inr x) ∘ Sum.inr) x =
    g _root_.id (corec₁ g) x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : {X : Type u} → (Cofix F α → X) → (β → X) → β → F (α ::: X)
x : β
h :
  ∀ (X Y : Type u) (f : Cofix F α → X) (f' : β → X) (k : X → Y), g (k ∘ f) (k ∘ f') x = (TypeVec.id ::: k) <$$> g f f' x
⊢ g (Sum.elim _root_.id (corec' fun x => g Sum.inl Sum.inr x) ∘ Sum.inl)
      (Sum.elim _root_.id (corec' fun x => g Sum.inl Sum.inr x) ∘ Sum.inr) x =
    g _root_.id (corec₁ g) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem _root_.Set.algebraMap_mem_center (r : R) : algebraMap R A r ∈ Set.center A

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ (algebraMap R A) r ∈ Set.center A

Tactic:
simp only [Semigroup.mem_center_iff, commutes, forall_const]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_mul (A : Matrix n n α) : adjugate A * A = A.det • (1 : Matrix n n α) :=
  calc
    adjugate A * A = (Aᵀ * adjugate Aᵀ)ᵀ

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ (Aᵀ * Aᵀ.adjugate)ᵀ = A.det • 1

Tactic:
rw [mul_adjugate Aᵀ, det_transpose, transpose_smul, transpose_one]

Result:
no goals

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ A.adjugate * A = (Aᵀ * Aᵀ.adjugate)ᵀ

Tactic:
rw [← adjugate_transpose, ← transpose_mul, transpose_transpose]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_div_le_one_div_of_neg_of_le (hb : b < 0) (h : a ≤ b) : 1 / b ≤ 1 / a

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
h : a ≤ b
⊢ 1 / b ≤ 1 / a

Tactic:
rwa [div_le_iff_of_neg' hb, ← div_eq_mul_one_div, div_le_one_of_neg (h.trans_lt hb)]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma le_iff_ne_zero_of_dvd (ha : a ≠ 0) (hab : a ∣ b) : a ≤ b ↔ b ≠ 0 where
  mp

Proof state:
a b : ℕ
ha : a ≠ 0
hab : a ∣ b
⊢ a ≤ b → b ≠ 0

Tactic:
rw [← Nat.pos_iff_ne_zero] at ha ⊢

Result:
a b : ℕ
ha : 0 < a
hab : a ∣ b
⊢ a ≤ b → 0 < b

Proof state:
a b : ℕ
ha : 0 < a
hab : a ∣ b
⊢ a ≤ b → 0 < b

Tactic:
exact Nat.lt_of_lt_of_le ha

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem comap_preimage (μ : Measure β) (s : Set β) :
    μ.comap f (f ⁻¹' s) = μ (s ∩ range f)

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure β
s : Set β
⊢ (Measure.comap f μ) (f ⁻¹' s) = μ (s ∩ range f)

Tactic:
rw [← hf.map_apply, hf.map_comap, restrict_apply' hf.measurableSet_range]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem comp_equiv_dotProduct_comp_equiv (e : m ≃ n) : x ∘ e ⬝ᵥ y ∘ e = x ⬝ᵥ y

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
x y : n → α
e : m ≃ n
⊢ x ∘ ⇑e ⬝ᵥ y ∘ ⇑e = x ⬝ᵥ y

Tactic:
rw [← dotProduct_comp_equiv_symm]

Result:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
x y : n → α
e : m ≃ n
⊢ x ⬝ᵥ (y ∘ ⇑e) ∘ ⇑e.symm = x ⬝ᵥ y

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
x y : n → α
e : m ≃ n
⊢ x ⬝ᵥ (y ∘ ⇑e) ∘ ⇑e.symm = x ⬝ᵥ y

Tactic:
simp only [Function.comp_def, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Prod.lean
lemma deterministic_prod_deterministic {f : α → β} {g : α → γ}
    (hf : Measurable f) (hg : Measurable g) :
    deterministic f hf ×ₖ deterministic g hg
      = deterministic (fun a ↦ (f a, g a)) (hf.prod_mk hg)

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
g : α → γ
hf : Measurable f
hg : Measurable g
a✝¹ : α
s✝ : Set (β × γ)
a✝ : MeasurableSet s✝
⊢ ((deterministic f hf ×ₖ deterministic g hg) a✝¹) s✝ = ((deterministic (fun a => (f a, g a)) ⋯) a✝¹) s✝

Tactic:
simp_rw [prod_apply, deterministic_apply, Measure.dirac_prod_dirac]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
g : α → γ
hf : Measurable f
hg : Measurable g
⊢ deterministic f hf ×ₖ deterministic g hg = deterministic (fun a => (f a, g a)) ⋯

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
g : α → γ
hf : Measurable f
hg : Measurable g
a✝¹ : α
s✝ : Set (β × γ)
a✝ : MeasurableSet s✝
⊢ ((deterministic f hf ×ₖ deterministic g hg) a✝¹) s✝ = ((deterministic (fun a => (f a, g a)) ⋯) a✝¹) s✝
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem hasMFDerivWithinAt_inter (h : t ∈ 𝓝 x) :
    HasMFDerivWithinAt I I' f (s ∩ t) x f' ↔ HasMFDerivWithinAt I I' f s x f'

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : t ∈ 𝓝 x
⊢ HasMFDerivWithinAt I I' f (s ∩ t) x f' ↔ HasMFDerivWithinAt I I' f s x f'

Tactic:
rw [HasMFDerivWithinAt, HasMFDerivWithinAt, extChartAt_preimage_inter_eq, hasFDerivWithinAt_inter,
  continuousWithinAt_inter h]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : t ∈ 𝓝 x
⊢ ↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝 (↑(extChartAt I x) x)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : t ∈ 𝓝 x
⊢ ↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝 (↑(extChartAt I x) x)

Tactic:
exact extChartAt_preimage_mem_nhds h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
lemma degree_map_lt (hp : f p.leadingCoeff = 0) (hp₀ : p ≠ 0) : (p.map f).degree < p.degree

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : p ≠ 0
⊢ (map f p).degree < p.degree

Tactic:
refine degree_map_le.lt_of_ne fun hpq ↦ hp₀ ?_

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0

Tactic:
rw [← degree_eq_bot, ← hpq, hp, degree_zero]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0

Tactic:
rw [leadingCoeff, ← coeff_map, ← natDegree_eq_natDegree hpq, ← leadingCoeff, leadingCoeff_eq_zero]
  at hp

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : map f p = 0
hp₀ : p ≠ 0
hpq : (map f p).degree = p.degree
⊢ p = 0
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.base_subset_complex [RelCWComplex C D] : D ⊆ C

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
⊢ D ⊆ skeleton C ⊤

Tactic:
exact base_subset_skeleton ⊤

Result:
no goals

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
⊢ D ⊆ C

Tactic:
simp_rw [← skeleton_top (C := C) (D := D)]

Result:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
⊢ D ⊆ skeleton C ⊤
-- Mathlib/Analysis/Convex/Intrinsic.lean
theorem intrinsicClosure_diff_intrinsicFrontier (s : Set P) :
    intrinsicClosure 𝕜 s \ intrinsicFrontier 𝕜 s = intrinsicInterior 𝕜 s :=
  (image_diff Subtype.coe_injective _ _).symm.trans <| by
    rw [closure_diff_frontier, intrinsicInterior]

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
s : Set P
⊢ (fun a => ↑a) '' (closure (Subtype.val ⁻¹' s) \ frontier (Subtype.val ⁻¹' s)) = intrinsicInterior 𝕜 s

Tactic:
rw [closure_diff_frontier, intrinsicInterior]

Result:
no goals
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem toΓSpecSheafedSpace_app_eq :
    X.toΓSpecSheafedSpace.c.app (op (basicOpen r)) = X.toΓSpecCApp r

Proof state:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ X.toΓSpecSheafedSpace.c.app (op (basicOpen r)) = X.toΓSpecCApp r

Tactic:
apply TopCat.Sheaf.extend_hom_app _ _ _

Result:
no goals