harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem linearIndepOn_equiv (e : ι ≃ ι') {f : ι' → M} {s : Set ι} :
    LinearIndepOn R (f ∘ e) s ↔ LinearIndepOn R f (e '' s) :=
  linearIndependent_equiv' (e.image s) <| by simp [funext_iff]

Proof state:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι ≃ ι'
f : ι' → M
s : Set ι
⊢ (fun x => f ↑x) ∘ ⇑(e.image s) = fun x => (f ∘ ⇑e) ↑x

Tactic:
simp [funext_iff]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem map_nhds_induced_eq (a : α) : map f (@nhds α (induced f t) a) = 𝓝[range f] f a

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
a : α
⊢ map f (𝓝 a) = 𝓝[range f] f a

Tactic:
rw [nhds_induced, Filter.map_comap, nhdsWithin]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem get_replicate (a : α) (i : Fin n) : (Vector.replicate n a).get i = a

Proof state:
α : Type u_1
n : ℕ
a : α
i : Fin n
⊢ (replicate n a).get i = a

Tactic:
apply List.getElem_replicate

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem le_div_iff_of_neg (hc : c < 0) : a ≤ b / c ↔ b ≤ a * c

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : c < 0
⊢ a ≤ b / c ↔ b ≤ a * c

Tactic:
rw [← neg_neg c, mul_neg, div_neg, le_neg, div_le_iff₀ (neg_pos.2 hc), neg_mul]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma Exact.mono_g_iff (hS : S.Exact) : Mono S.g ↔ S.f = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ Mono S.g ↔ S.f = 0

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ Mono S.g → S.f = 0

case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ S.f = 0 → Mono S.g

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ S.f = 0 → Mono S.g

Tactic:
exact hS.mono_g

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
a✝ : Mono S.g
⊢ S.f = 0

Tactic:
rw [← cancel_mono S.g, zero, zero_comp]

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ Mono S.g → S.f = 0

Tactic:
intro

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
a✝ : Mono S.g
⊢ S.f = 0
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_neg_two : T R (-2) = 2 * X ^ 2 - 1

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ T R (-2) = 2 * X ^ 2 - 1

Tactic:
simp [T_two]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_eq (z : ℂ) : sin z = sin z.re * cosh z.im + cos z.re * sinh z.im * I

Proof state:
z : ℂ
⊢ sin z = sin ↑z.re * cosh ↑z.im + cos ↑z.re * sinh ↑z.im * I

Tactic:
convert sin_add_mul_I z.re z.im

Result:
case h.e'_2.h.e'_1
z : ℂ
⊢ z = ↑z.re + ↑z.im * I

Proof state:
case h.e'_2.h.e'_1
z : ℂ
⊢ z = ↑z.re + ↑z.im * I

Tactic:
exact (re_add_im z).symm

Result:
no goals
-- Mathlib/Topology/Algebra/ConstMulAction.lean
theorem Topology.IsInducing.continuousConstSMul {N β : Type*} [SMul N β] [TopologicalSpace β]
    {g : β → α} (hg : IsInducing g) (f : N → M) (hf : ∀ {c : N} {x : β}, g (c • x) = f c • g x) :
    ContinuousConstSMul N β where
  continuous_const_smul c

Proof state:
M : Type u_1
α : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : SMul M α
inst✝² : ContinuousConstSMul M α
N : Type u_4
β : Type u_5
inst✝¹ : SMul N β
inst✝ : TopologicalSpace β
g : β → α
hg : IsInducing g
f : N → M
hf : ∀ {c : N} {x : β}, g (c • x) = f c • g x
c : N
⊢ Continuous fun x => c • x

Tactic:
simpa only [Function.comp_def, hf, hg.continuous_iff] using hg.continuous.const_smul (f c)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Multiset.lean
@[simp] lemma prod_eq_zero_iff : s.prod = 0 ↔ (0 : α) ∈ s :=
  Quotient.inductionOn s fun l ↦ by rw [quot_mk_to_coe, prod_coe]; exact List.prod_eq_zero_iff

Proof state:
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
s : Multiset α
l : List α
⊢ l.prod = 0 ↔ 0 ∈ ↑l

Tactic:
exact List.prod_eq_zero_iff

Result:
no goals

Proof state:
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
s : Multiset α
l : List α
⊢ prod ⟦l⟧ = 0 ↔ 0 ∈ ⟦l⟧

Tactic:
rw [quot_mk_to_coe, prod_coe]

Result:
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
s : Multiset α
l : List α
⊢ l.prod = 0 ↔ 0 ∈ ↑l
-- Mathlib/Analysis/RCLike/Basic.lean
lemma nnnorm_nnqsmul (q : ℚ≥0) (x : E) : ‖q • x‖₊ = q • ‖x‖₊

Proof state:
K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedField E
inst✝¹ : CharZero E
inst✝ : NormedSpace K E
q : ℚ≥0
x : E
⊢ ‖q • x‖₊ = q • ‖x‖₊

Tactic:
simpa [NNRat.cast_smul_eq_nnqsmul] using nnnorm_smul (q : K) x

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem get_cons_addChar (c : Char) (cs : List Char) (i : Pos) :
    get ⟨c :: cs⟩ (i + c) = get ⟨cs⟩ i

Proof state:
c : Char
cs : List Char
i : Pos
⊢ { data := c :: cs }.get (i + c) = { data := cs }.get i

Tactic:
simp [get, utf8GetAux, Pos.zero_ne_addChar, utf8GetAux_addChar_right_cancel]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Action.lean
theorem measure_eq_zero_iff_eq_empty_of_smulInvariant (hμ : μ ≠ 0) (hU : IsOpen U) :
    μ U = 0 ↔ U = ∅

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
μ : Measure α
inst✝⁴ : SMulInvariantMeasure G α μ
inst✝³ : TopologicalSpace α
inst✝² : ContinuousConstSMul G α
inst✝¹ : MulAction.IsMinimal G α
U : Set α
inst✝ : μ.Regular
hμ : μ ≠ 0
hU : IsOpen U
⊢ μ U = 0 ↔ U = ∅

Tactic:
rw [← not_iff_not, ← Ne, ← pos_iff_ne_zero,
  measure_pos_iff_nonempty_of_smulInvariant G hμ hU, nonempty_iff_ne_empty]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem support_derivativeFinsupp_subset_range {p : R[X]} {n : ℕ} (h : p.natDegree < n) :
    (derivativeFinsupp p).support ⊆ range n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ (Finsupp.onFinset (range (p.natDegree + 1)) (fun x => (⇑derivative)^[x] p) ⋯).support ⊆ range n

Tactic:
exact Finsupp.support_onFinset_subset.trans (Finset.range_subset.mpr h)

Result:
no goals

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

Tactic:
dsimp [derivativeFinsupp]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.natDegree < n
⊢ (Finsupp.onFinset (range (p.natDegree + 1)) (fun x => (⇑derivative)^[x] p) ⋯).support ⊆ range n
-- Mathlib/Data/Finset/Image.lean
theorem image_comm {β'} [DecidableEq β'] [DecidableEq γ] {f : β → γ} {g : α → β} {f' : α → β'}
    {g' : β' → γ} (h_comm : ∀ a, f (g a) = g' (f' a)) :
    (s.image g).image f = (s.image f').image g'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq β
s : Finset α
β' : Type u_4
inst✝¹ : DecidableEq β'
inst✝ : DecidableEq γ
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ image f (image g s) = image g' (image f' s)

Tactic:
simp_rw [image_image, comp_def, h_comm]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler_comp_rightAngleRotation (x y : E) : o.kahler (J x) (J y) = o.kahler x y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.kahler (o.rightAngleRotation x)) (o.rightAngleRotation y) = (o.kahler x) y

Tactic:
simp only [kahler_rightAngleRotation_left, kahler_rightAngleRotation_right]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Complex.I * (-Complex.I * (o.kahler x) y) = (o.kahler x) y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Complex.I * (-Complex.I * (o.kahler x) y) = (o.kahler x) y

Tactic:
linear_combination -o.kahler x y * Complex.I_sq

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem pow_card_pow (n : ℕ) (a : K) : a ^ q ^ n = a

Proof state:
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
n : ℕ
a : K
⊢ a ^ q ^ n = a

Tactic:
induction n with
| zero => simp
| succ n ih => simp [pow_succ, pow_mul, ih, pow_card]

Result:
no goals

Proof state:
case zero
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
⊢ a ^ q ^ 0 = a

Tactic:
simp

Result:
no goals

Proof state:
case succ
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
n : ℕ
ih : a ^ q ^ n = a
⊢ a ^ q ^ (n + 1) = a

Tactic:
simp [pow_succ, pow_mul, ih, pow_card]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem self_mul_star : a * star a = normSq a

Proof state:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a * star a = ↑(normSq a)

Tactic:
rw [mul_star_eq_coe, normSq_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.elem_toArray [BEq α] {l : List α} {a : α} :
    Array.elem a l.toArray = List.elem a l

Proof state:
α : Type u_1
inst✝ : BEq α
l : List α
a : α
⊢ elem a l.toArray = List.elem a l

Tactic:
simp [Array.elem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem not_lt {a b : Int} : ¬a < b ↔ b ≤ a :=
  by rw [← Int.not_le, Decidable.not_not]

Proof state:
a b : Int
⊢ ¬a < b ↔ b ≤ a

Tactic:
rw [← Int.not_le, Decidable.not_not]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_Ico' [DivisionRing α] {x : α} (hx : x ≠ 1) {m n : ℕ} (hmn : m ≤ n) :
    ∑ i ∈ Finset.Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x)

Proof state:
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ (x ^ n - x ^ m) / (x - 1) = (x ^ m - x ^ n) / (1 - x)

Tactic:
convert neg_div_neg_eq (x ^ m - x ^ n) (1 - x) using 2 <;> abel

Result:
no goals

Proof state:
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ ∑ i ∈ Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x)

Tactic:
simp only [geom_sum_Ico hx hmn]

Result:
α : Type u
inst✝ : DivisionRing α
x : α
hx : x ≠ 1
m n : ℕ
hmn : m ≤ n
⊢ (x ^ n - x ^ m) / (x - 1) = (x ^ m - x ^ n) / (1 - x)
-- Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
theorem integralNormalization_coeff_degree {i : ℕ} (hi : p.degree = i) :
    (integralNormalization p).coeff i = 1

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : p.degree = ↑i
⊢ p.integralNormalization.coeff i = 1

Tactic:
rw [integralNormalization_coeff, if_pos hi]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem cyclicPermutations_ne_nil : ∀ l : List α, cyclicPermutations l ≠ []
  | a::l, h => by simpa using congr_arg length h

Proof state:
α : Type u
a : α
l : List α
h : (a :: l).cyclicPermutations = []
⊢ False

Tactic:
simpa using congr_arg length h

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Lemmas.lean
theorem recDiag_zero_succ {motive : Nat → Nat → Sort _} (zero_zero : motive 0 0)
    (zero_succ : ∀ n, motive 0 n → motive 0 (n+1)) (succ_zero : ∀ m, motive m 0 → motive (m+1) 0)
    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) (n) :
    Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 (n+1)
      = zero_succ n (Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 n)

Proof state:
motive : Nat → Nat → Sort u_1
zero_zero : motive 0 0
zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)
succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0
succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)
n : Nat
⊢ Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 (n + 1) =
    zero_succ n (Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 n)

Tactic:
simp [Nat.recDiag]

Result:
motive : Nat → Nat → Sort u_1
zero_zero : motive 0 0
zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)
succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0
succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)
n : Nat
⊢ recDiag.left zero_zero zero_succ (n + 1) = zero_succ n (recDiag.left zero_zero zero_succ n)

Proof state:
motive : Nat → Nat → Sort u_1
zero_zero : motive 0 0
zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)
succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0
succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)
n : Nat
⊢ recDiag.left zero_zero zero_succ (n + 1) = zero_succ n (recDiag.left zero_zero zero_succ n)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma lieBracket_swap : lieBracket 𝕜 V W x = - lieBracket 𝕜 W V x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
⊢ lieBracket 𝕜 V W x = -lieBracket 𝕜 W V x

Tactic:
simp [lieBracket]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_δ_self' {n} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : j = Fin.castSucc i) :
    X.δ i ≫ X.δ j = X.δ i ≫ X.δ i.succ

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i ≫ X.δ i.castSucc = X.δ i ≫ X.δ i.succ

Tactic:
rw [δ_comp_δ_self]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = i.castSucc
⊢ X.δ i ≫ X.δ j = X.δ i ≫ X.δ i.succ

Tactic:
subst H

Result:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i ≫ X.δ i.castSucc = X.δ i ≫ X.δ i.succ
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem rel_sup_mul [CompleteLattice α] (m : α → M) (m0 : m ⊥ = 1) (R : M → M → Prop)
    (m_iSup : ∀ s : ℕ → α, R (m (⨆ i, s i)) (∏' i, m (s i))) (s₁ s₂ : α) :
    R (m (s₁ ⊔ s₂)) (m s₁ * m s₂)

Proof state:
case h.e'_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ m s₁ * m s₂ = ∏' (b : Bool), m (bif b then s₁ else s₂)

Tactic:
rw [tprod_fintype, Fintype.prod_bool, cond, cond]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ R (m (s₁ ⊔ s₂)) (m s₁ * m s₂)

Tactic:
convert rel_iSup_tprod m m0 R m_iSup fun b ↦ cond b s₁ s₂

Result:
case h.e'_1.h.e'_1
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ s₁ ⊔ s₂ = ⨆ b, bif b then s₁ else s₂

case h.e'_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ m s₁ * m s₂ = ∏' (b : Bool), m (bif b then s₁ else s₂)

Proof state:
case h.e'_1.h.e'_1
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ s₁ ⊔ s₂ = ⨆ b, bif b then s₁ else s₂

Tactic:
simp only [iSup_bool_eq, cond]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_mul_of_one_le [CommSemiring α] [PartialOrder α] [AddLeftReflectLE α]
    [AddLeftMono α] [ExistsAddOfLE α] [Sub α] [OrderedSub α] {x : α} (hx : 1 ≤ x) (n : ℕ) :
    (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

Proof state:
α : Type u
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : AddLeftReflectLE α
inst✝³ : AddLeftMono α
inst✝² : ExistsAddOfLE α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x : α
hx : 1 ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

Tactic:
simpa using geom_sum₂_mul_of_ge hx n

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem disjoint_prod : Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

Proof state:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

Tactic:
simp_rw [disjoint_left, mem_prod, not_and_or, Prod.forall, and_imp, ← @forall_or_right α, ←
  @forall_or_left β, ← @forall_or_right (_ ∈ s₁), ← @forall_or_left (_ ∈ t₁)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem findSomeRev?_toArray (f : α → Option β) (v : Vector α n) :
    v.toArray.findSomeRev? f = v.findSomeRev? f

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.findSomeRev? f { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    findSomeRev? f { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
v : Vector α n
⊢ Array.findSomeRev? f v.toArray = findSomeRev? f v

Tactic:
cases v

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
f : α → Option β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.findSomeRev? f { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    findSomeRev? f { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBasis.insert_isBasis_insert (hI : M.IsBasis I X) (h : M.Indep (insert e I)) :
    M.IsBasis (insert e I) (insert e X)

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis I X
h : M.Indep (insert e I)
⊢ M.IsBasis (insert e I) (insert e X)

Tactic:
simp_rw [← union_singleton] at *

Result:
α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis I X
h : M.Indep (I ∪ {e})
⊢ M.IsBasis (I ∪ {e}) (X ∪ {e})

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
e : α
hI : M.IsBasis I X
h : M.Indep (I ∪ {e})
⊢ M.IsBasis (I ∪ {e}) (X ∪ {e})

Tactic:
exact hI.union_isBasis_union (h.subset subset_union_right).isBasis_self h

Result:
no goals
-- Mathlib/Algebra/Lie/Engel.lean
theorem LieModule.isNilpotent_iff_forall' [IsNoetherian R M] :
    LieModule.IsNilpotent L M ↔ ∀ x, _root_.IsNilpotent <| toEnd R L M x

Proof state:
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNoetherian R M
⊢ IsNilpotent L M ↔ ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)

Tactic:
rw [← isNilpotent_range_toEnd_iff (R := R), LieModule.isNilpotent_iff_forall (R := R)]

Result:
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNoetherian R M
⊢ (∀ (x : ↥(toEnd R L M).range), _root_.IsNilpotent ((toEnd R (↥(toEnd R L M).range) M) x)) ↔
    ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)

Proof state:
R : Type u₁
L : Type u₂
M : Type u₄
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : IsNoetherian R M
⊢ (∀ (x : ↥(toEnd R L M).range), _root_.IsNilpotent ((toEnd R (↥(toEnd R L M).range) M) x)) ↔
    ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem support_rename_of_injective {p : MvPolynomial σ R} {f : σ → τ} [DecidableEq τ]
    (h : Function.Injective f) :
    (rename f p).support = Finset.image (Finsupp.mapDomain f) p.support

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
inst✝ : DecidableEq τ
h : Injective f
⊢ ((rename f) p).support = Finset.image (Finsupp.mapDomain f) p.support

Tactic:
rw [rename_eq]

Result:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
inst✝ : DecidableEq τ
h : Injective f
⊢ support (Finsupp.mapDomain (Finsupp.mapDomain f) p) = Finset.image (Finsupp.mapDomain f) p.support

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
inst✝ : DecidableEq τ
h : Injective f
⊢ support (Finsupp.mapDomain (Finsupp.mapDomain f) p) = Finset.image (Finsupp.mapDomain f) p.support

Tactic:
exact Finsupp.mapDomain_support_of_injective (mapDomain_injective h) _

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem factors_prod (a : Associates α) : a.factors.prod = a

Proof state:
case intro.inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : a ≠ 0
⊢ (Associates.mk a).factors.prod = Associates.mk a

Tactic:
simp [ha, prod_mk, mk_eq_mk_iff_associated, UniqueFactorizationMonoid.factors_prod,
  -Quotient.eq]

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ (Associates.mk a).factors.prod = Associates.mk a

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Result:
case intro.inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ (Associates.mk 0).factors.prod = Associates.mk 0

case intro.inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : a ≠ 0
⊢ (Associates.mk a).factors.prod = Associates.mk a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ a.factors.prod = a

Tactic:
rcases Associates.mk_surjective a with ⟨a, rfl⟩

Result:
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ (Associates.mk a).factors.prod = Associates.mk a

Proof state:
case intro.inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ (Associates.mk 0).factors.prod = Associates.mk 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_C_mul_X (ha : a ≠ 0) : degree (C a * X) = 1

Proof state:
R : Type u
a : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X).degree = 1

Tactic:
simpa only [pow_one] using degree_C_mul_X_pow 1 ha

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem smul_ball_preimage (p : Seminorm 𝕜 E) (y : E) (r : ℝ) (a : 𝕜) (ha : a ≠ 0) :
    (a • ·) ⁻¹' p.ball y r = p.ball (a⁻¹ • y) (r / ‖a‖) :=
  Set.ext fun _ => by
    rw [mem_preimage, mem_ball, mem_ball, lt_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
      map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
a : 𝕜
ha : a ≠ 0
x✝ : E
⊢ x✝ ∈ (fun x => a • x) ⁻¹' p.ball y r ↔ x✝ ∈ p.ball (a⁻¹ • y) (r / ‖a‖)

Tactic:
rw [mem_preimage, mem_ball, mem_ball, lt_div_iff₀ (norm_pos_iff.mpr ha), mul_comm, ←
  map_smul_eq_mul p, smul_sub, smul_inv_smul₀ ha]

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
@[to_additive]
lemma smul_one_smul {M} (N) [Monoid N] [SMul M N] [MulAction N α] [SMul M α]
    [IsScalarTower M N α] (x : M) (y : α) : (x • (1 : N)) • y = x • y

Proof state:
α : Type u_5
M : Type u_9
N : Type u_10
inst✝⁴ : Monoid N
inst✝³ : SMul M N
inst✝² : MulAction N α
inst✝¹ : SMul M α
inst✝ : IsScalarTower M N α
x : M
y : α
⊢ (x • 1) • y = x • y

Tactic:
rw [smul_assoc, one_smul]

Result:
no goals