harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matroid/Sum.lean
lemma IsBase.eq_union_image_of_disjointSum {h B} (hB : (disjointSum M N h).IsBase B) :
    ∃ BM BN, M.IsBase BM ∧ N.IsBase BN ∧ Disjoint BM BN ∧ B = BM ∪ BN

Proof state:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
⊢ ∃ BM BN, M.IsBase BM ∧ N.IsBase BN ∧ Disjoint BM BN ∧ B = BM ∪ BN

Tactic:
refine ⟨_, _, hB.1, hB.2.1, h.mono inter_subset_right inter_subset_right, ?_⟩

Result:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
⊢ B = B ∩ M.E ∪ B ∩ N.E

Proof state:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
⊢ B = B ∩ M.E ∪ B ∩ N.E

Tactic:
rw [← inter_union_distrib_left, inter_eq_self_of_subset_left hB.2.2]

Result:
no goals

Proof state:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : (M.disjointSum N h).IsBase B
⊢ ∃ BM BN, M.IsBase BM ∧ N.IsBase BN ∧ Disjoint BM BN ∧ B = BM ∪ BN

Tactic:
rw [disjointSum_isBase_iff] at hB

Result:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
B : Set α
hB : M.IsBase (B ∩ M.E) ∧ N.IsBase (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
⊢ ∃ BM BN, M.IsBase BM ∧ N.IsBase BN ∧ Disjoint BM BN ∧ B = BM ∪ BN
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zipWith_comm (f : α → β → γ) (la : Vector α n) (lb : Vector β n) :
    zipWith f la lb = zipWith (fun b a => f a b) lb la

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
f : α → β → γ
la : Vector α n
lb : Vector β n
⊢ zipWith f la lb = zipWith (fun b a => f a b) lb la

Tactic:
rcases la with ⟨la, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : Array α
lb : Vector β la.size
⊢ zipWith f { toArray := la, size_toArray := ⋯ } lb = zipWith (fun b a => f a b) lb { toArray := la, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : Array α
lb : Vector β la.size
⊢ zipWith f { toArray := la, size_toArray := ⋯ } lb = zipWith (fun b a => f a b) lb { toArray := la, size_toArray := ⋯ }

Tactic:
rcases lb with ⟨lb, h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : Array α
lb : Array β
h : lb.size = la.size
⊢ zipWith f { toArray := la, size_toArray := ⋯ } { toArray := lb, size_toArray := h } =
    zipWith (fun b a => f a b) { toArray := lb, size_toArray := h } { toArray := la, size_toArray := ⋯ }

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
la : Array α
lb : Array β
h : lb.size = la.size
⊢ zipWith f { toArray := la, size_toArray := ⋯ } { toArray := lb, size_toArray := h } =
    zipWith (fun b a => f a b) { toArray := lb, size_toArray := h } { toArray := la, size_toArray := ⋯ }

Tactic:
simpa using Array.zipWith_comm _ _ _

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem of_int_multiplicity {z : ℤ} (hp : p ≠ 1) (hz : z ≠ 0) :
    padicValRat p (z : ℚ) = multiplicity (p : ℤ) z

Proof state:
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ padicValRat p ↑z = ↑(multiplicity (↑p) z)

Tactic:
rw [of_int, padicValInt.of_ne_one_ne_zero hp hz]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
private lemma LFunction_isBigO_horizontal_of_eq_zero {y : ℝ} (hy : y ≠ 0 ∨ χ ≠ 1)
    (h : LFunction χ (1 + I * y) = 0) :
    (fun x : ℝ ↦ LFunction χ (1 + x + I * y)) =O[𝓝[>] 0] fun x : ℝ ↦ (x : ℂ)

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * ↑y) = 0
⊢ (fun x => LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝[>] 0] fun x => ↑x

Tactic:
have := (χ.differentiableAt_LFunction _ <| one_add_I_mul_ne_one_or χ hy).hasDerivAt

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * ↑y) = 0
this : HasDerivAt (LFunction χ) (deriv (LFunction χ) (1 + I * ↑y)) (1 + I * ↑y)
⊢ (fun x => LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝[>] 0] fun x => ↑x

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * ↑y) = 0
this : HasDerivAt (LFunction χ) (deriv (LFunction χ) (1 + I * ↑y)) (1 + I * ↑y)
⊢ (fun x => LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝[>] 0] fun x => ↑x

Tactic:
rw [← zero_add (1 + _)] at this

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * ↑y) = 0
this : HasDerivAt (LFunction χ) (deriv (LFunction χ) (0 + (1 + I * ↑y))) (0 + (1 + I * ↑y))
⊢ (fun x => LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝[>] 0] fun x => ↑x

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * ↑y) = 0
⊢ (fun x => LFunction χ (1 + ↑x + I * ↑y)) =O[𝓝[>] 0] fun x => ↑x

Tactic:
simp_rw [add_comm (1 : ℂ), add_assoc]

Result:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * ↑y) = 0
⊢ (fun x => LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝[>] 0] fun x => ↑x

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
h : LFunction χ (1 + I * ↑y) = 0
this : HasDerivAt (LFunction χ) (deriv (LFunction χ) (0 + (1 + I * ↑y))) (0 + (1 + I * ↑y))
⊢ (fun x => LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝[>] 0] fun x => ↑x

Tactic:
simpa only [zero_add, h, sub_zero]
  using (Complex.isBigO_comp_ofReal_nhds
    (this.comp_add_const 0 _).differentiableAt.isBigO_sub) |>.mono nhdsWithin_le_nhds

Result:
no goals
-- Mathlib/Algebra/CharP/MixedCharZero.lean
theorem pnatCast_eq_natCast [Fact (∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I))] (n : ℕ+) :
    ((n : Rˣ) : R) = ↑n

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ ↑⋯.unit = ↑↑n

Tactic:
simp only [IsUnit.unit_spec]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ ↑↑n = ↑↑n

Tactic:
change ((PNat.isUnit_natCast (R := R) n).unit : R) = ↑n

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))
n : ℕ+
⊢ ↑⋯.unit = ↑↑n
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
lemma Subalgebra.toNonUnitalSubalgebra_toSubalgebra (S : Subalgebra R A) :
    S.toNonUnitalSubalgebra.toSubalgebra S.one_mem = S

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ S.toNonUnitalSubalgebra.toSubalgebra ⋯ = S

Tactic:
cases S

Result:
case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
⊢ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }.toNonUnitalSubalgebra.toSubalgebra ⋯ =
    { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }

Proof state:
case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
⊢ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }.toNonUnitalSubalgebra.toSubalgebra ⋯ =
    { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem out_embedding {c c' : Cardinal} : c ≤ c' ↔ Nonempty (c.out ↪ c'.out)

Proof state:
c c' : Cardinal.{u_1}
⊢ c ≤ c' ↔ Nonempty (Quotient.out c ↪ Quotient.out c')

Tactic:
conv_lhs => rw [← Cardinal.mk_out c, ← Cardinal.mk_out c', le_def]

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem roots_expand_map_frobenius : (expand R p f).roots.map (frobenius R p) = p • f.roots

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : ExpChar R p
f : R[X]
inst✝ : PerfectRing R p
⊢ Multiset.map (⇑(frobenius R p)) ((expand R p) f).roots = p • f.roots

Tactic:
simp [roots_expand, Multiset.map_nsmul]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
lemma Nat.Coprime.orderOf_pow (h : (orderOf y).Coprime m) : orderOf (y ^ m) = orderOf y

Proof state:
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
⊢ orderOf (y ^ m) = orderOf y

Tactic:
by_cases hg : IsOfFinOrder y

Result:
case pos
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : IsOfFinOrder y
⊢ orderOf (y ^ m) = orderOf y

case neg
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : ¬IsOfFinOrder y
⊢ orderOf (y ^ m) = orderOf y

Proof state:
case pos
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : IsOfFinOrder y
⊢ orderOf (y ^ m) = orderOf y

Tactic:
rw [hg.orderOf_pow y m , h.gcd_eq_one, Nat.div_one]

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Monoid G
y : G
m : ℕ
h : (orderOf y).Coprime m
hg : ¬IsOfFinOrder y
⊢ orderOf (y ^ m) = orderOf y

Tactic:
rw [m.coprime_zero_left.1 (orderOf_eq_zero hg ▸ h), pow_one]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem minFac_eq_one_iff {n : ℕ} : minFac n = 1 ↔ n = 1

Proof state:
case mp
n : ℕ
h : n.minFac = 1
hn : ¬n = 1
this : Prime n.minFac
⊢ False

Tactic:
rw [h] at this

Result:
case mp
n : ℕ
h : n.minFac = 1
hn : ¬n = 1
this : Prime 1
⊢ False

Proof state:
case mpr
n : ℕ
⊢ n = 1 → n.minFac = 1

Tactic:
rintro rfl

Result:
case mpr

⊢ minFac 1 = 1

Proof state:
n : ℕ
⊢ n.minFac = 1 ↔ n = 1

Tactic:
constructor

Result:
case mp
n : ℕ
⊢ n.minFac = 1 → n = 1

case mpr
n : ℕ
⊢ n = 1 → n.minFac = 1

Proof state:
case mp
n : ℕ
h : n.minFac = 1
hn : ¬n = 1
this : Prime 1
⊢ False

Tactic:
exact not_prime_one this

Result:
no goals

Proof state:
case mp
n : ℕ
⊢ n.minFac = 1 → n = 1

Tactic:
intro h

Result:
case mp
n : ℕ
h : n.minFac = 1
⊢ n = 1

Proof state:
case mpr

⊢ minFac 1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
case mp
n : ℕ
h : n.minFac = 1
hn : ¬n = 1
⊢ False

Tactic:
have := minFac_prime hn

Result:
case mp
n : ℕ
h : n.minFac = 1
hn : ¬n = 1
this : Prime n.minFac
⊢ False

Proof state:
case mp
n : ℕ
h : n.minFac = 1
⊢ n = 1

Tactic:
by_contra hn

Result:
case mp
n : ℕ
h : n.minFac = 1
hn : ¬n = 1
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem ofNat_pos {a : Nat} : 0 < (a : Int) ↔ 0 < a

Proof state:
a : Nat
⊢ 0 < ↑a ↔ 0 < a

Tactic:
rw [← Int.ofNat_zero, Int.ofNat_lt]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem edge_other_incident_set {v : V} {e : Sym2 V} (h : e ∈ G.incidenceSet v) :
    e ∈ G.incidenceSet (G.otherVertexOfIncident h)

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
⊢ e ∈ G.incidenceSet (G.otherVertexOfIncident h)

Tactic:
use h.1

Result:
case right
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
⊢ G.otherVertexOfIncident h ∈ e

Proof state:
case right
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
v : V
e : Sym2 V
h : e ∈ G.incidenceSet v
⊢ G.otherVertexOfIncident h ∈ e

Tactic:
simp [otherVertexOfIncident, Sym2.other_mem']

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Int.lean
theorem exist_integer_multiples_of_finite {ι : Type*} [Finite ι] (g : ι → M') :
    ∃ b : S, ∀ i, IsInteger f ((b : R) • g i)

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
ι : Type u_4
inst✝ : Finite ι
g : ι → M'
⊢ ∃ b, ∀ (i : ι), IsInteger f (↑b • g i)

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
ι : Type u_4
inst✝ : Finite ι
g : ι → M'
val✝ : Fintype ι
⊢ ∃ b, ∀ (i : ι), IsInteger f (↑b • g i)

Proof state:
case intro.intro
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
ι : Type u_4
inst✝ : Finite ι
g : ι → M'
val✝ : Fintype ι
b : ↥S
hb : ∀ i ∈ Finset.univ, IsInteger f (↑b • g i)
⊢ ∃ b, ∀ (i : ι), IsInteger f (↑b • g i)

Tactic:
exact ⟨b, fun i => hb i (Finset.mem_univ _)⟩

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
ι : Type u_4
inst✝ : Finite ι
g : ι → M'
val✝ : Fintype ι
⊢ ∃ b, ∀ (i : ι), IsInteger f (↑b • g i)

Tactic:
obtain ⟨b, hb⟩ := exist_integer_multiples S f Finset.univ g

Result:
case intro.intro
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
ι : Type u_4
inst✝ : Finite ι
g : ι → M'
val✝ : Fintype ι
b : ↥S
hb : ∀ i ∈ Finset.univ, IsInteger f (↑b • g i)
⊢ ∃ b, ∀ (i : ι), IsInteger f (↑b • g i)
-- Mathlib/Data/Set/Lattice.lean
theorem inter_empty_of_inter_sUnion_empty {s t : Set α} {S : Set (Set α)} (hs : t ∈ S)
    (h : s ∩ ⋃₀ S = ∅) : s ∩ t = ∅ :=
  eq_empty_of_subset_empty <| by
    rw [← h]; exact inter_subset_inter_right _ (subset_sUnion_of_mem hs)

Proof state:
α : Type u_1
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ s ∩ ⋃₀ S

Tactic:
exact inter_subset_inter_right _ (subset_sUnion_of_mem hs)

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ ∅

Tactic:
rw [← h]

Result:
α : Type u_1
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ s ∩ ⋃₀ S
-- Mathlib/Data/Option/Basic.lean
theorem pbind_eq_bind (f : α → Option β) (x : Option α) : (x.pbind fun a _ ↦ f a) = x.bind f

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
x : Option α
⊢ (x.pbind fun a x => f a) = x.bind f

Tactic:
cases x <;> simp only [pbind, none_bind', some_bind']

Result:
no goals
-- Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
/-- If `A` has doubling strictly less than `2`, then `A * A⁻¹ = A⁻¹ * A`. -/
lemma mul_inv_eq_inv_mul_of_doubling_lt_two (h : #(A * A) < 2 * #A) : A * A⁻¹ = A⁻¹ * A

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
⊢ A * A⁻¹ ⊆ A⁻¹ * A

Tactic:
simpa using
  mul_inv_eq_inv_mul_of_doubling_lt_two_aux (A := A⁻¹) (by simpa [← mul_inv_rev] using h)

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
⊢ #(A⁻¹ * A⁻¹) < 2 * #A⁻¹

Tactic:
simpa [← mul_inv_rev] using h

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
⊢ A * A⁻¹ = A⁻¹ * A

Tactic:
refine Subset.antisymm ?_ (mul_inv_eq_inv_mul_of_doubling_lt_two_aux h)

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : #(A * A) < 2 * #A
⊢ A * A⁻¹ ⊆ A⁻¹ * A
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_smul (r : R) : (r • p).smeval x = r • p.smeval x

Proof state:
case h_monomial
R : Type u_1
inst✝³ : Semiring R
p : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
r : R
n : ℕ
a : R
⊢ (r • (monomial n) a).smeval x = r • ((monomial n) a).smeval x

Tactic:
rw [smul_monomial, smeval_monomial, smeval_monomial, smul_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Semiring R
p : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
r : R
⊢ (r • p).smeval x = r • p.smeval x

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q ph qh =>
  rw [smul_add, smeval_add, ph, qh, ← smul_add, smeval_add]
| h_monomial n a =>
  rw [smul_monomial, smeval_monomial, smeval_monomial, smul_assoc]

Result:
no goals

Proof state:
case h_add
R : Type u_1
inst✝³ : Semiring R
p✝ : R[X]
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : Module R S
x : S
r : R
p q : R[X]
ph : (r • p).smeval x = r • p.smeval x
qh : (r • q).smeval x = r • q.smeval x
⊢ (r • (p + q)).smeval x = r • (p + q).smeval x

Tactic:
rw [smul_add, smeval_add, ph, qh, ← smul_add, smeval_add]

Result:
no goals
-- Mathlib/LinearAlgebra/Goursat.lean
lemma goursatSnd_toAddSubgroup :
    (goursatSnd L).toAddSubgroup = L.toAddSubgroup.goursatSnd

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
⊢ L.goursatSnd.toAddSubgroup = L.toAddSubgroup.goursatSnd

Tactic:
ext x

Result:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
x : N
⊢ x ∈ L.goursatSnd.toAddSubgroup ↔ x ∈ L.toAddSubgroup.goursatSnd

Proof state:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
x : N
⊢ x ∈ L.goursatSnd.toAddSubgroup ↔ x ∈ L.toAddSubgroup.goursatSnd

Tactic:
simp [mem_toAddSubgroup, goursatSnd, AddSubgroup.mem_goursatSnd]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_lt_one_of_one_lt_of_neg {x z : ℝ} (hx : 1 < x) (hz : z < 0) : x ^ z < 1

Proof state:
x z : ℝ
hx : 1 < x
hz : z < 0
⊢ x ^ z < 1

Tactic:
convert rpow_lt_rpow_of_exponent_lt hx hz

Result:
case h.e'_4
x z : ℝ
hx : 1 < x
hz : z < 0
⊢ 1 = x ^ 0

Proof state:
case h.e'_4
x z : ℝ
hx : 1 < x
hz : z < 0
⊢ 1 = x ^ 0

Tactic:
exact (rpow_zero x).symm

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem tmul_sum (m : M) {α : Type*} (s : Finset α) (n : α → N) :
    (m ⊗ₜ[R] ∑ a ∈ s, n a) = ∑ a ∈ s, m ⊗ₜ[R] n a

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
m : M
α : Type u_11
s : Finset α
n : α → N
⊢ m ⊗ₜ[R] ∑ a ∈ s, n a = ∑ a ∈ s, m ⊗ₜ[R] n a

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert has ih => simp [Finset.sum_insert has, tmul_add, ih]

Result:
no goals

Proof state:
case insert
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
m : M
α : Type u_11
n : α → N
a✝ : α
s✝ : Finset α
has : a✝ ∉ s✝
ih : m ⊗ₜ[R] ∑ a ∈ s✝, n a = ∑ a ∈ s✝, m ⊗ₜ[R] n a
⊢ m ⊗ₜ[R] ∑ a ∈ insert a✝ s✝, n a = ∑ a ∈ insert a✝ s✝, m ⊗ₜ[R] n a

Tactic:
simp [Finset.sum_insert has, tmul_add, ih]

Result:
no goals

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
m : M
α : Type u_11
s : Finset α
n : α → N
⊢ m ⊗ₜ[R] ∑ a ∈ s, n a = ∑ a ∈ s, m ⊗ₜ[R] n a

Tactic:
induction s using Finset.induction with
| empty => simp
| insert has ih => simp [Finset.sum_insert has, tmul_add, ih]

Result:
no goals

Proof state:
case empty
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
m : M
α : Type u_11
n : α → N
⊢ m ⊗ₜ[R] ∑ a ∈ ∅, n a = ∑ a ∈ ∅, m ⊗ₜ[R] n a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem attach_map_val {s : Finset α} : s.attach.map (Embedding.subtype _) = s :=
  eq_of_veq <| by rw [map_val, attach_val]; exact Multiset.attach_map_val _

Proof state:
α : Type u_1
s : Finset α
⊢ (map (Embedding.subtype fun x => x ∈ s) s.attach).val = s.val

Tactic:
rw [map_val, attach_val]

Result:
α : Type u_1
s : Finset α
⊢ Multiset.map (⇑(Embedding.subtype fun x => x ∈ s)) s.val.attach = s.val

Proof state:
α : Type u_1
s : Finset α
⊢ Multiset.map (⇑(Embedding.subtype fun x => x ∈ s)) s.val.attach = s.val

Tactic:
exact Multiset.attach_map_val _

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem diagonal_updateRow_single [DecidableEq n] [Zero α] (v : n → α) (i : n) (x : α) :
    (diagonal v).updateRow i (Pi.single i x) = diagonal (Function.update v i x)

Proof state:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
⊢ (diagonal v).updateRow i (Pi.single i x) = diagonal (Function.update v i x)

Tactic:
rw [← diagonal_transpose, updateRow_transpose, diagonal_updateCol_single, diagonal_transpose]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Assoc.lean
theorem pullbackAssoc_inv_fst_snd [HasPullback ((pullback.snd _ _ : Z₁ ⟶ X₂) ≫ f₃) f₄]
    [HasPullback f₁ ((pullback.fst _ _ : Z₂ ⟶ X₂) ≫ f₂)] :
    (pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.fst _ _ ≫ pullback.snd _ _ =
    pullback.snd _ _ ≫ pullback.fst _ _

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂ =
    pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄

Tactic:
rw [Iso.inv_comp_eq, pullbackAssoc_hom_snd_fst]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem coeff_C_mul (m) (a : R) (p : MvPolynomial σ R) : coeff m (C a * p) = a * coeff m p

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ (sum p fun n b => (monomial (0 + n)) (0 * b)) = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ coeff m (C a * p) = a * coeff m p

Tactic:
rw [mul_def, sum_C]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ coeff m (sum p fun n b => (monomial (0 + n)) (a * b)) = a * coeff m p

R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ (sum p fun n b => (monomial (0 + n)) (0 * b)) = 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
a : R
p : MvPolynomial σ R
⊢ coeff m (sum p fun n b => (monomial (0 + n)) (a * b)) = a * coeff m p

Tactic:
simp +contextual [sum_def, coeff_sum]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sub_eq_iff_eq_add {x y z : BitVec w} : x - y = z ↔ x = z + y

Proof state:
case mp
w : Nat
x y z : BitVec w
h : x - y = z
⊢ x = z + y

Tactic:
simp [← h, sub_add_cancel]

Result:
no goals

Proof state:
case mpr
w : Nat
x y z : BitVec w
h : x = z + y
⊢ x - y = z

Tactic:
simp [h, add_sub_cancel]

Result:
no goals

Proof state:
w : Nat
x y z : BitVec w
⊢ x - y = z ↔ x = z + y

Tactic:
apply Iff.intro <;> intro h

Result:
case mp
w : Nat
x y z : BitVec w
h : x - y = z
⊢ x = z + y

case mpr
w : Nat
x y z : BitVec w
h : x = z + y
⊢ x - y = z
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp] lemma inv_neg'' : a⁻¹ < 0 ↔ a < 0

Proof state:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulMono G₀
this : PosMulReflectLT G₀
⊢ a⁻¹ < 0 ↔ a < 0

Tactic:
simp only [← not_le, inv_nonneg]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulMono G₀
⊢ a⁻¹ < 0 ↔ a < 0

Tactic:
have := PosMulMono.toPosMulReflectLT (α := G₀)

Result:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulMono G₀
this : PosMulReflectLT G₀
⊢ a⁻¹ < 0 ↔ a < 0