harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem exists_root_of_degree_eq_one (h : degree p = 1) : ∃ x, IsRoot p x :=
  ⟨-((p.coeff 1)⁻¹ * p.coeff 0), by
    rw [← mem_roots (by simp [← zero_le_degree_iff, h])]
    simp [roots_degree_eq_one h]⟩

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 1
⊢ -((p.coeff 1)⁻¹ * p.coeff 0) ∈ p.roots

Tactic:
simp [roots_degree_eq_one h]

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 1
⊢ p.IsRoot (-((p.coeff 1)⁻¹ * p.coeff 0))

Tactic:
rw [← mem_roots (by simp [← zero_le_degree_iff, h])]

Result:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 1
⊢ -((p.coeff 1)⁻¹ * p.coeff 0) ∈ p.roots

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 1
⊢ p ≠ 0

Tactic:
simp [← zero_le_degree_iff, h]

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
/-- See also `LieModule.isNilpotent_iff_exists_ucs_eq_top`. -/
lemma isNilpotent_iff :
    IsNilpotent L M ↔ ∃ k, lowerCentralSeries R L M k = ⊥

Proof state:
R : Type u
L : Type v
M : Type w
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
⊢ IsNilpotent L M ↔ ∃ k, lowerCentralSeries R L M k = ⊥

Tactic:
simp [isNilpotent_iff_int, SetLike.ext'_iff, coe_lowerCentralSeries_eq_int R L M]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/OpenPos.lean
theorem _root_.IsOpen.measure_eq_zero_iff (hU : IsOpen U) : μ U = 0 ↔ U = ∅

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
U : Set X
hU : IsOpen U
⊢ μ U = 0 ↔ U = ∅

Tactic:
simpa only [not_lt, nonpos_iff_eq_zero, not_nonempty_iff_eq_empty] using
  not_congr (hU.measure_pos_iff μ)

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma desc_comp_π (s : relations.Solution N) : (h.desc s).comp solution.π = s.π

Proof state:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : relations.Solution N
⊢ h.desc s ∘ₗ solution.π = s.π

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem coe_coe_sign (x : SignType) : ((x : ℝ) : EReal) = x

Proof state:
x : SignType
⊢ ↑↑x = ↑x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem neg_strictConcaveOn_iff : StrictConcaveOn 𝕜 s (-f) ↔ StrictConvexOn 𝕜 s f

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommGroup β
inst✝¹ : SMul 𝕜 E
inst✝ : Module 𝕜 β
s : Set E
f : E → β
⊢ StrictConcaveOn 𝕜 s (-f) ↔ StrictConvexOn 𝕜 s f

Tactic:
rw [← neg_strictConvexOn_iff, neg_neg f]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_le_encard_iff_encard_diff_le_encard_diff (h : (s ∩ t).Finite) :
    s.encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard

Proof state:
α : Type u_1
s t : Set α
h : (s ∩ t).Finite
⊢ s.encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard

Tactic:
rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
  WithTop.add_le_add_iff_right h.encard_lt_top.ne]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem map_eq_bot_iff_of_injective {f : G →* N} (hf : Function.Injective f) :
    H.map f = ⊥ ↔ H = ⊥

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ map f H = ⊥ ↔ H = ⊥

Tactic:
rw [map_eq_bot_iff, f.ker_eq_bot_iff.mpr hf, le_bot_iff]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma lift_whiskerRight {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Y ⟶ W) :
    lift f g ≫ (h ▷ Z) = lift (f ≫ h) g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
⊢ lift f g ≫ h ▷ Z = lift (f ≫ h) g

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Algebra/Field/Periodic.lean
theorem Antiperiodic.div_inv [DivisionSemiring α] [Neg β] (h : Antiperiodic f c) {a : α}
    (ha : a ≠ 0) : Antiperiodic (fun x => f (x / a)) (c * a)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : DivisionSemiring α
inst✝ : Neg β
h : Antiperiodic f c
a : α
ha : a ≠ 0
⊢ Antiperiodic (fun x => f (x / a)) (c * a)

Tactic:
simpa only [div_eq_mul_inv] using h.mul_const_inv ha

Result:
no goals
-- Mathlib/FieldTheory/LinearDisjoint.lean
theorem of_finrank_coprime (H : (finrank F A).Coprime (finrank F L)) : A.LinearDisjoint L :=
  letI : Field (AlgHom.range (IsScalarTower.toAlgHom F L E)) :=
    inferInstanceAs <| Field (AlgHom.fieldRange (IsScalarTower.toAlgHom F L E))
  letI : Field A.toSubalgebra := inferInstanceAs <| Field A
  Subalgebra.LinearDisjoint.of_finrank_coprime_of_free <| by
    rwa [(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.finrank_eq] at H

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : (finrank F ↥A).Coprime (finrank F L)
this✝ : Field ↥(IsScalarTower.toAlgHom F L E).range :=
  inferInstanceAs (Field ↥(IsScalarTower.toAlgHom F L E).fieldRange)
this : Field ↥A.toSubalgebra := inferInstanceAs (Field ↥A)
⊢ (finrank F ↥A.toSubalgebra).Coprime (finrank F ↥(IsScalarTower.toAlgHom F L E).range)

Tactic:
rwa [(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.finrank_eq] at H

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem associated_iff_normalizedFactors_eq_normalizedFactors {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
    x ~ᵤ y ↔ normalizedFactors x = normalizedFactors y :=
  ⟨Associated.normalizedFactors_eq, fun h =>
    (prod_normalizedFactors hx).symm.trans (_root_.trans (by rw [h]) (prod_normalizedFactors hy))⟩

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalizedFactors x = normalizedFactors y
⊢ (normalizedFactors x).prod ~ᵤ (normalizedFactors y).prod

Tactic:
rw [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem find?_toList (p : α → Bool) (v : Vector α n) :
    v.toList.find? p = v.find? p

Proof state:
α : Type
n : Nat
p : α → Bool
v : Vector α n
⊢ List.find? p v.toList = find? p v

Tactic:
cases v

Result:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.find? p { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    find? p { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ List.find? p { toArray := toArray✝, size_toArray := size_toArray✝ }.toList =
    find? p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticChar_sq_one' {a : F} (ha : a ≠ 0) : quadraticChar F (a ^ 2) = 1

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
a : F
ha : a ≠ 0
⊢ (quadraticChar F) (a ^ 2) = 1

Tactic:
simp only [quadraticChar_apply, quadraticCharFun, sq_eq_zero_iff, ha, IsSquare.sq, if_true,
  if_false]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem option_orElse : Primrec₂ ((· <|> ·) : Option α → Option α → Option α) :=
  (option_casesOn fst snd (fst.comp fst).to₂).of_eq fun ⟨o₁, o₂⟩ => by cases o₁ <;> cases o₂ <;> rfl

Proof state:
α : Type u_1
inst✝ : Primcodable α
x✝ : Option α × Option α
o₁ o₂ : Option α
⊢ (Option.casesOn (o₁, o₂).1 (o₁, o₂).2 fun b => ((o₁, o₂), b).1.1) = (fun x1 x2 => x1 <|> x2) (o₁, o₂).1 (o₁, o₂).2

Tactic:
cases o₁ <;> cases o₂ <;> rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_to_list (s : Finset α) (f : α → β) : (s.toList.map f).prod = s.prod f

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset α
f : α → β
⊢ (List.map f s.toList).prod = s.prod f

Tactic:
rw [Finset.prod, ← Multiset.prod_coe, ← Multiset.map_coe, Finset.coe_toList]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
@[simp] lemma odd_add_one_self' : Odd (a + (1 + a))

Proof state:
α : Type u_2
inst✝ : Semiring α
a : α
⊢ Odd (a + (1 + a))

Tactic:
simp [add_comm 1 a]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
theorem hermite_succ (n : ℕ) : hermite (n + 1) = X * hermite n - derivative (hermite n)

Proof state:
n : ℕ
⊢ hermite (n + 1) = X * hermite n - derivative (hermite n)

Tactic:
rw [hermite]

Result:
no goals
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem neLocus_self_add_left : neLocus (f + g) f = g.support

Proof state:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ (f + g).neLocus f = g.support

Tactic:
rw [neLocus_comm, neLocus_self_add_right]

Result:
no goals
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem neLocus_neg : neLocus (-f) g = f.neLocus (-g)

Proof state:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ (-f).neLocus g = f.neLocus (-g)

Tactic:
rw [← neLocus_neg_neg, neg_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem head?_modifyHead {l : List α} {f : α → α} :
    (l.modifyHead f).head? = l.head?.map f

Proof state:
α : Type u_1
l : List α
f : α → α
⊢ (modifyHead f l).head? = Option.map f l.head?

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_emod_mul_of_pos
    {a : Int} (b c : Int) (H : 0 < a) : (a * b) % (a * c) = a * (b % c)

Proof state:
a b c : Int
H : 0 < a
⊢ a * b % (a * c) = a * (b % c)

Tactic:
rw [emod_def, emod_def, mul_ediv_mul_of_pos _ _ H, Int.mul_sub, Int.mul_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_symm (a b) : ∫ x in b..a, f x ∂μ = -∫ x in a..b, f x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
⊢ ∫ (x : ℝ) in b..a, f x ∂μ = -∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
simp only [intervalIntegral, neg_sub]

Result:
no goals
-- Mathlib/Algebra/Ring/Identities.lean
theorem sq_add_mul_sq_mul_sq_add_mul_sq :
    (x₁ ^ 2 + n * x₂ ^ 2) * (y₁ ^ 2 + n * y₂ ^ 2) =
    (x₁ * y₁ - n * x₂ * y₂) ^ 2 + n * (x₁ * y₂ + x₂ * y₁) ^ 2

Proof state:
R : Type u_1
inst✝ : CommRing R
x₁ x₂ y₁ y₂ n : R
⊢ (x₁ ^ 2 + n * x₂ ^ 2) * (y₁ ^ 2 + n * y₂ ^ 2) = (x₁ * y₁ - n * x₂ * y₂) ^ 2 + n * (x₁ * y₂ + x₂ * y₁) ^ 2

Tactic:
ring

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem tendsto_prod_iff' {g' : Filter γ} {s : α → β × γ} :
    Tendsto s f (g ×ˢ g') ↔ Tendsto (fun n => (s n).1) f g ∧ Tendsto (fun n => (s n).2) f g'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
g' : Filter γ
s : α → β × γ
⊢ Tendsto s f (g ×ˢ g') ↔ Tendsto (fun n => (s n).1) f g ∧ Tendsto (fun n => (s n).2) f g'

Tactic:
simp only [prod_eq_inf, tendsto_inf, tendsto_comap_iff, Function.comp_def]

Result:
no goals
-- Mathlib/Logic/Function/Iterate.lean
theorem foldr_const (f : β → β) (b : β) : ∀ l : List α, l.foldr (fun _ ↦ f) b = f^[l.length] b
  | [] => rfl
  | a :: l => by rw [length_cons, foldr, foldr_const f b l, iterate_succ_apply']

Proof state:
α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
⊢ foldr (fun x => f) b (a :: l) = f^[(a :: l).length] b

Tactic:
rw [length_cons, foldr, foldr_const f b l, iterate_succ_apply']

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean
@[reassoc]
lemma map_shift_unop {X Y : Cᵒᵖ} (f : X ⟶ Y) (n : ℤ) :
    F.map ((f⟦n⟧').unop) = ((F.op.commShiftIso n).inv.app Y).unop ≫
      ((F.map f.unop).op⟦n⟧').unop ≫ ((F.op.commShiftIso n).hom.app X).unop

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X Y : Cᵒᵖ
f : X ⟶ Y
n : ℤ
⊢ F.map ((shiftFunctor Cᵒᵖ n).map f).unop =
    ((F.op.commShiftIso n).inv.app Y).unop ≫
      ((shiftFunctor Dᵒᵖ n).map (F.map f.unop).op).unop ≫ ((F.op.commShiftIso n).hom.app X).unop

Tactic:
simp [shift_map_op]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_concat_zero : (concat x b)[0] = b

Proof state:
w✝ : Nat
x : BitVec w✝
b : Bool
⊢ (x.concat b)[0] = b

Tactic:
simp [getElem_concat]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem isUnit_iff_norm_isUnit {d : ℤ} (z : ℤ√d) : IsUnit z ↔ IsUnit z.norm

Proof state:
d : ℤ
z : ℤ√d
⊢ IsUnit z ↔ IsUnit z.norm

Tactic:
rw [Int.isUnit_iff_natAbs_eq, norm_eq_one_iff]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem AddValuation.map_zero : addValuationDef (0 : ℚ_[p]) = ⊤

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ addValuationDef 0 = ⊤

Tactic:
rw [addValuationDef, if_pos rfl]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem iInf_toSubsemiring {ι : Sort*} (S : ι → Subalgebra R A) :
    (iInf S).toSubsemiring = ⨅ i, (S i).toSubsemiring

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
⊢ (iInf S).toSubsemiring = ⨅ i, (S i).toSubsemiring

Tactic:
simp only [iInf, sInf_toSubsemiring, ← Set.range_comp, Function.comp_def]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
@[simp]
lemma Hom.sub_tmul (f g : Hom P P') (r x) :
    f.sub g (r ⊗ₜ .D _ _ x) = r • Cotangent.mk (f.subToKer g x)

Proof state:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Extension R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
r : S
x : P.Ring
⊢ (f.sub g) (r ⊗ₜ[P.Ring] (D R P.Ring) x) = r • Cotangent.mk ((f.subToKer g) x)

Tactic:
simp only [sub, LinearMap.liftBaseChange_tmul, Derivation.liftKaehlerDifferential_comp_D,
  Derivation.mk_coe, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem self_eq_append_left {x y : Array α} : y = x ++ y ↔ x = #[]

Proof state:
α : Type u_1
x y : Array α
⊢ y = x ++ y ↔ x = #[]

Tactic:
rw [eq_comm, append_left_eq_self]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem hasBasis_cobounded_compl_closedBall (c : α) :
    (cobounded α).HasBasis (fun _ ↦ True) (fun r ↦ (closedBall c r)ᶜ) :=
  ⟨compl_surjective.forall.2 fun _ ↦ (isBounded_iff_subset_closedBall c).trans <| by simp⟩

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
c : α
x✝ : Set α
⊢ (∃ r, x✝ ⊆ closedBall c r) ↔ ∃ i, True ∧ (closedBall c i)ᶜ ⊆ x✝ᶜ

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem comp_sup'_eq_sup'_comp [SemilatticeSup γ] {s : Finset β} (H : s.Nonempty) {f : β → α}
    (g : α → γ) (g_sup : ∀ x y, g (x ⊔ y) = g x ⊔ g y) : g (s.sup' H f) = s.sup' H (g ∘ f)

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
⊢ g (s.sup' H f) = s.sup' H (g ∘ f)

Tactic:
refine H.cons_induction ?_ ?_ <;> intros <;> simp [*]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem edist_of_re_eq {z w : ℂ} (h : z.re = w.re) : edist z w = edist z.im w.im

Proof state:
z w : ℂ
h : z.re = w.re
⊢ edist z w = edist z.im w.im

Tactic:
rw [edist_nndist, edist_nndist, nndist_of_re_eq h]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
lemma map_inits {β : Type*} (g : α → β) : (l.map g).inits = l.inits.map (map g)

Proof state:
α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g l).inits = map (map g) l.inits

Tactic:
induction' l using reverseRecOn <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem getElem_range' {n m step} (i) (H : i < (range' n m step).length) :
    (range' n m step)[i] = n + step * i :=
  (getElem?_eq_some_iff.1 <| getElem?_range' n step (by simpa using H)).2

Proof state:
n m step i : Nat
H : i < (range' n m step).length
⊢ i < m

Tactic:
simpa using H

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@[to_additive (attr := simp)]
lemma natCard_inv (s : Set G) : Nat.card ↥(s⁻¹) = Nat.card s

Proof state:
G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ Nat.card ↑s⁻¹ = Nat.card ↑s

Tactic:
rw [← image_inv_eq_inv, Nat.card_image_of_injective inv_injective]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem mem_range {m n : Nat} : m ∈ range n ↔ m < n

Proof state:
m n : Nat
⊢ m ∈ range n ↔ m < n

Tactic:
simp only [range_eq_range', mem_range'_1, Nat.zero_le, true_and, Nat.zero_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)} {k fallback : α}
    (h' : (l.map Prod.fst).contains k = false) :
    (insertMany m l).1.getKeyD k fallback = m.getKeyD k fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
k fallback : α
h' : (List.map Prod.fst l).contains k = false
⊢ (insertMany m l).val.getKeyD k fallback = m.getKeyD k fallback

Tactic:
simp_to_model [Const.insertMany] using List.getKeyD_insertListConst_of_contains_eq_false

Result:
no goals
-- Mathlib/Data/Finset/Grade.lean
@[simp] lemma erase_wcovBy (s : Finset α) (a : α) : s.erase a ⩿ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s.erase a ⩿ s

Tactic:
simp [← coe_wcovBy_coe]

Result:
no goals
-- Mathlib/Tactic/NormNum/Inv.lean
theorem isRat_inv_one {α} [DivisionRing α] : {a : α} →
    IsNat a (nat_lit 1) → IsNat a⁻¹ (nat_lit 1)
  | _, ⟨rfl⟩ => ⟨by simp⟩

Proof state:
α : Type u_1
inst✝ : DivisionRing α
⊢ (↑1)⁻¹ = ↑1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
theorem cast_natCast (n : ℕ) : ((n : ℚ) : α) = n

Proof state:
α : Type u_3
inst✝ : DivisionRing α
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
rw [← Int.cast_natCast, cast_intCast, Int.cast_natCast]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem mem_zpowers_of_prime_card {p : ℕ} [hp : Fact p.Prime]
    (h : Nat.card G = p) {g g' : G} (hg : g ≠ 1) : g' ∈ zpowers g

Proof state:
G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
⊢ g' ∈ zpowers g

Tactic:
simp_rw [zpowers_eq_top_of_prime_card h hg, Subgroup.mem_top]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem sSup_eq_iSup' (s : Set α) : sSup s = ⨆ a : s, (a : α)

Proof state:
α : Type u_1
inst✝ : SupSet α
s : Set α
⊢ sSup s = ⨆ a, ↑a

Tactic:
rw [iSup, Subtype.range_coe]

Result:
no goals
-- Mathlib/Data/Vector3.lean
theorem exists_vector_succ (f : Vector3 α (succ n) → Prop) : Exists f ↔ ∃ x v, f (x :: v) :=
  ⟨fun ⟨v, fv⟩ => ⟨_, _, by rw [cons_head_tail v]; exact fv⟩, fun ⟨_, _, fxv⟩ => ⟨_, fxv⟩⟩

Proof state:
α : Type u_1
n : ℕ
f : Vector3 α n.succ → Prop
x✝ : Exists f
v : Vector3 α n.succ
fv : f v
⊢ f (?m.22125 x✝ v fv :: ?m.22126 x✝ v fv)

Tactic:
rw [cons_head_tail v]

Result:
α : Type u_1
n : ℕ
f : Vector3 α n.succ → Prop
x✝ : Exists f
v : Vector3 α n.succ
fv : f v
⊢ f v

Proof state:
α : Type u_1
n : ℕ
f : Vector3 α n.succ → Prop
x✝ : Exists f
v : Vector3 α n.succ
fv : f v
⊢ f v

Tactic:
exact fv

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem det_one_sub_mul_comm (A : Matrix m n α) (B : Matrix n m α) :
    det (1 - A * B) = det (1 - B * A)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (1 - A * B).det = (1 - B * A).det

Tactic:
rw [sub_eq_add_neg, ← Matrix.neg_mul, det_one_add_mul_comm, Matrix.mul_neg, ← sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem le_of_lt : ∀ {x y : Bool}, x < y → x ≤ y

Proof state:
⊢ ∀ {x y : Bool}, x < y → x ≤ y

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem tendsto_self_mul_const_pow_of_abs_lt_one {r : ℝ} (hr : |r| < 1) :
    Tendsto (fun n ↦ n * r ^ n : ℕ → ℝ) atTop (𝓝 0)

Proof state:
r : ℝ
hr : |r| < 1
⊢ Tendsto (fun n => ↑n * r ^ n) atTop (𝓝 0)

Tactic:
simpa only [pow_one] using tendsto_pow_const_mul_const_pow_of_abs_lt_one 1 hr

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
lemma ball_mem_nhds [TopologicalSpace E] {p : Seminorm 𝕝 E} (hp : Continuous p) {r : ℝ}
    (hr : 0 < r) : p.ball 0 r ∈ (𝓝 0 : Filter E) :=
  have this : Tendsto p (𝓝 0) (𝓝 0) := map_zero p ▸ hp.tendsto 0
  by simpa only [p.ball_zero_eq] using this (Iio_mem_nhds hr)

Proof state:
𝕝 : Type u_6
E : Type u_7
inst✝³ : SeminormedRing 𝕝
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕝 E
inst✝ : TopologicalSpace E
p : Seminorm 𝕝 E
hp : Continuous ⇑p
r : ℝ
hr : 0 < r
this : Tendsto (⇑p) (𝓝 0) (𝓝 0)
⊢ p.ball 0 r ∈ 𝓝 0

Tactic:
simpa only [p.ball_zero_eq] using this (Iio_mem_nhds hr)

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem coe_ideal_span_singleton_mul_inv {x : R₁} (hx : x ≠ 0) :
    (Ideal.span ({x} : Set R₁) : FractionalIdeal R₁⁰ K) *
    (Ideal.span ({x} : Set R₁) : FractionalIdeal R₁⁰ K)⁻¹ = 1

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : R₁
hx : x ≠ 0
⊢ ↑(Ideal.span {x}) * (↑(Ideal.span {x}))⁻¹ = 1

Tactic:
rw [coeIdeal_span_singleton,
  spanSingleton_mul_inv K <|
    (map_ne_zero_iff _ <| FaithfulSMul.algebraMap_injective R₁ K).mpr hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem range_eq_nil {n : Nat} : range n = [] ↔ n = 0

Proof state:
n : Nat
⊢ range n = [] ↔ n = 0

Tactic:
rw [← length_eq_zero, length_range]

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp]
lemma WithTop.ofDual_lt_ofDual_iff {x y : WithTop αᵒᵈ} :
    WithTop.ofDual x < WithTop.ofDual y ↔ y < x

Proof state:
α : Type u_1
inst✝ : LT α
x y : WithTop αᵒᵈ
⊢ WithTop.ofDual x < WithTop.ofDual y ↔ y < x

Tactic:
cases x <;> cases y <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem prev_zero (s : Substring) : s.prev 0 = 0

Proof state:
s : Substring
⊢ s.prev 0 = 0

Tactic:
simp [prev, Pos.add_eq, Pos.byteIdx_zero]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem image_univ : r.image Set.univ = r.codom

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ r.image Set.univ = r.codom

Tactic:
ext y

Result:
case h
α : Type u_1
β : Type u_2
r : Rel α β
y : β
⊢ y ∈ r.image Set.univ ↔ y ∈ r.codom

Proof state:
case h
α : Type u_1
β : Type u_2
r : Rel α β
y : β
⊢ y ∈ r.image Set.univ ↔ y ∈ r.codom

Tactic:
simp [mem_image, codom]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
@[simp]
lemma id_map {a : M} (f : ShiftedHom X Y a) : f.map (𝟭 C) = f

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y : C
a : M
f : ShiftedHom X Y a
⊢ f.map (𝟭 C) = f

Tactic:
simp [map, Functor.commShiftIso, Functor.CommShift.iso]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
lemma inf_iSup₂_eq {f : ∀ i, κ i → α} (a : α) : (a ⊓ ⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, a ⊓ f i j

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
a : α
⊢ a ⊓ ⨆ i, ⨆ j, f i j = ⨆ i, ⨆ j, a ⊓ f i j

Tactic:
simp only [inf_iSup_eq]

Result:
no goals