harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Density.lean
lemma dens_sdiff_comm (h : card s = card t) : dens (s \ t) = dens (t \ s) :=
  add_left_injective (dens t) <| by
    simp_rw [dens_sdiff_add_dens, union_comm s, ← dens_sdiff_add_dens, dens, h]

Proof state:
α : Type u_2
inst✝¹ : Fintype α
s t : Finset α
inst✝ : DecidableEq α
h : #s = #t
⊢ (fun x => x + t.dens) (s \ t).dens = (fun x => x + t.dens) (t \ s).dens

Tactic:
simp_rw [dens_sdiff_add_dens, union_comm s, ← dens_sdiff_add_dens, dens, h]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem of_natCast [AddGroupWithOne α] (n : ℕ) : ((n : ZNum) : α) = n

Proof state:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ℕ
⊢ ↑↑n = ↑n

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

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem add_absorp (h₁ : a < ω ^ b) (h₂ : ω ^ b ≤ c) : a + c = c

Proof state:
a b c : Ordinal.{u}
h₁ : a < ω ^ b
h₂ : ω ^ b ≤ c
⊢ a + c = c

Tactic:
rw [← Ordinal.add_sub_cancel_of_le h₂, ← add_assoc, add_omega0_opow h₁]

Result:
no goals
-- Mathlib/Algebra/Group/Idempotent.lean
@[simp] lemma iff_eq_one : IsIdempotentElem a ↔ a = 1

Proof state:
M : Type u_1
inst✝ : CancelMonoid M
a : M
⊢ IsIdempotentElem a ↔ a = 1

Tactic:
simp [IsIdempotentElem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem forIn'_map [Monad m] [LawfulMonad m]
    (l : Vector α n) (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :
    forIn' (l.map g) init f = forIn' l init fun a h y => f (g a) (mem_map_of_mem g h) y

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
f : (b : β) → b ∈ map g { toArray := toArray✝, size_toArray := size_toArray✝ } → γ → m (ForInStep γ)
⊢ forIn' (map g { toArray := toArray✝, size_toArray := size_toArray✝ }) init f =
    forIn' { toArray := toArray✝, size_toArray := size_toArray✝ } init fun a h y => f (g a) ⋯ y

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Vector α n
g : α → β
f : (b : β) → b ∈ map g l → γ → m (ForInStep γ)
⊢ forIn' (map g l) init f = forIn' l init fun a h y => f (g a) ⋯ y

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_4
γ : Type u_1
init : γ
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : α → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
f : (b : β) → b ∈ map g { toArray := toArray✝, size_toArray := size_toArray✝ } → γ → m (ForInStep γ)
⊢ forIn' (map g { toArray := toArray✝, size_toArray := size_toArray✝ }) init f =
    forIn' { toArray := toArray✝, size_toArray := size_toArray✝ } init fun a h y => f (g a) ⋯ y
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem preimage_emetric_closedBall (h : α ≃ᵢ β) (x : β) (r : ℝ≥0∞) :
    h ⁻¹' EMetric.closedBall x r = EMetric.closedBall (h.symm x) r

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' EMetric.closedBall x r = EMetric.closedBall (h.symm x) r

Tactic:
rw [← h.isometry.preimage_emetric_closedBall (h.symm x) r, h.apply_symm_apply]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem toMultiset_eq_nil {s : Cycle α} : s.toMultiset = 0 ↔ s = Cycle.nil :=
  Quotient.inductionOn' s (by simp)

Proof state:
α : Type u_1
s : Cycle α
⊢ ∀ (a : List α), toMultiset (Quotient.mk'' a) = 0 ↔ Quotient.mk'' a = nil

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_ite_eq (i : ι) (f : ι → M) :
    𝔼 j, (if i = j then f j else 0) = f i /ℚ card ι

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
i : ι
f : ι → M
⊢ (𝔼 j : ι, if i = j then f j else 0) = (↑(card ι))⁻¹ • f i

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem partNum_none_iff_s_none : g.partNums.get? n = none ↔ g.s.get? n = none

Proof state:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.partNums.get? n = none ↔ g.s.get? n = none

Tactic:
cases s_nth_eq : g.s.get? n <;> simp [partNums, s_nth_eq]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Seminorm.lean
theorem map_sub_le_max : f (x - y) ≤ max (f x) (f y)

Proof state:
E : Type u_3
F : Type u_4
inst✝² : AddGroup E
inst✝¹ : FunLike F E ℝ
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ f (x + -y) ≤ f x ⊔ f (-y)

Tactic:
exact map_add_le_max _ _ _

Result:
no goals

Proof state:
E : Type u_3
F : Type u_4
inst✝² : AddGroup E
inst✝¹ : FunLike F E ℝ
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ f (x - y) ≤ f x ⊔ f y

Tactic:
rw [sub_eq_add_neg, ← NonarchAddGroupSeminormClass.map_neg_eq_map' f y]

Result:
E : Type u_3
F : Type u_4
inst✝² : AddGroup E
inst✝¹ : FunLike F E ℝ
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ f (x + -y) ≤ f x ⊔ f (-y)
-- Mathlib/Data/Finset/Prod.lean
theorem disjoint_product : Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ Disjoint s s' ∨ Disjoint t t'

Proof state:
α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
⊢ Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ Disjoint s s' ∨ Disjoint t t'

Tactic:
simp_rw [← disjoint_coe, coe_product, Set.disjoint_prod]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Comp.lean
theorem lintegral_comp (η : Kernel β γ) (κ : Kernel α β) (a : α) {g : γ → ℝ≥0∞}
    (hg : Measurable g) : ∫⁻ c, g c ∂(η ∘ₖ κ) a = ∫⁻ b, ∫⁻ c, g c ∂η b ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
κ : Kernel α β
a : α
g : γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : γ), g c ∂(η ∘ₖ κ) a = ∫⁻ (b : β), ∫⁻ (c : γ), g c ∂η b ∂κ a

Tactic:
rw [comp_apply, Measure.lintegral_bind (Kernel.measurable _) hg]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem neg_coeff (x : 𝕎 R) (n : ℕ) : (-x).coeff n = peval (wittNeg p n) ![x.coeff]

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ (-x).coeff n = peval (wittNeg p n) ![x.coeff]

Tactic:
simp [Neg.neg, eval, Matrix.cons_fin_one, coeff_mk]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
theorem map_smul_inv {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) :
    c • f x = f (σ' c • x)

Proof state:
R : Type u_1
S : Type u_5
M : Type u_8
M₃ : Type u_11
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₃
σ : R →+* S
f : M →ₛₗ[σ] M₃
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
c : S
x : M
⊢ c • f x = f (σ' c • x)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem mem_closedBall_iff_norm''' : b ∈ closedBall a r ↔ ‖a / b‖ ≤ r

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖a / b‖ ≤ r

Tactic:
rw [mem_closedBall', dist_eq_norm_div]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem zero_mul {f : ℕ → M} (h : HasProd (fun n ↦ f (n + 1)) m) :
    HasProd f (f 0 * m)

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℕ → M
h : HasProd (fun n => f (n + 1)) m
⊢ HasProd f (f 0 * m)

Tactic:
simpa only [prod_range_one] using h.prod_range_mul

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem aleph1_lt_lift {c : Cardinal.{u}} : ℵ₁ < lift.{v} c ↔ ℵ₁ < c

Proof state:
c : Cardinal.{u}
⊢ ℵ_ 1 < lift.{v, u} c ↔ ℵ_ 1 < c

Tactic:
simpa using lift_lt (a := ℵ₁)

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem index_map_subtype {H : Subgroup G} (K : Subgroup H) :
    (K.map H.subtype).index = K.index * H.index

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
K : Subgroup ↥H
⊢ (map H.subtype K).index = K.index * H.index

Tactic:
rw [K.index_map_of_injective H.subtype_injective, H.range_subtype]

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
/-- Negating a matrix partitioned by rows is equivalent to negating each of the rows. -/
@[simp]
lemma fromRows_neg (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
    -fromRows A₁ A₂ = fromRows (-A₁) (-A₂)

Proof state:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
⊢ -A₁.fromRows A₂ = (-A₁).fromRows (-A₂)

Tactic:
ext (i | i) j <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
lemma essSup_eq_iSup (hμ : ∀ a, μ {a} ≠ 0) (f : α → β) : essSup f μ = ⨆ i, f i

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteLattice β
hμ : ∀ (a : α), μ {a} ≠ 0
f : α → β
⊢ essSup f μ = ⨆ i, f i

Tactic:
rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_iSup]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
lemma erase_eq_iff_eq_insert (hs : a ∈ s) (ht : a ∉ t) : erase s a = t ↔ s = insert a t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : a ∈ s
ht : a ∉ t
⊢ s.erase a = t ↔ s = insert a t

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_X [Nontrivial R] : (X n : MvPolynomial σ R).vars = {n}

Proof state:
R : Type u
σ : Type u_1
n : σ
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
⊢ (X n).vars = {n}

Tactic:
rw [X, vars_monomial (one_ne_zero' R), Finsupp.support_single_ne_zero _ (one_ne_zero' ℕ)]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_map_equiv [MeasurableSpace β] (e : α ≃ᵐ β) {f : β → E} {μ : Measure α}
    {s : Set β} : IntegrableOn f s (μ.map e) ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) μ

Proof state:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
f : β → E
μ : Measure α
s : Set β
⊢ IntegrableOn f s (Measure.map (⇑e) μ) ↔ IntegrableOn (f ∘ ⇑e) (⇑e ⁻¹' s) μ

Tactic:
simp only [IntegrableOn, e.restrict_map, integrable_map_equiv e]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem nhdsSet_insert (x : X) (s : Set X) : 𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ 𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s

Tactic:
rw [insert_eq, nhdsSet_union, nhdsSet_singleton]

Result:
no goals
-- Mathlib/Data/Multiset/UnionInter.lean
theorem map_set_pairwise {f : α → β} {r : β → β → Prop} {m : Multiset α}
    (h : { a | a ∈ m }.Pairwise fun a₁ a₂ => r (f a₁) (f a₂)) : { b | b ∈ m.map f }.Pairwise r :=
  fun b₁ h₁ b₂ h₂ hn => by
    obtain ⟨⟨a₁, H₁, rfl⟩, a₂, H₂, rfl⟩ := Multiset.mem_map.1 h₁, Multiset.mem_map.1 h₂
    exact h H₁ H₂ (mt (congr_arg f) hn)

Proof state:
α : Type u_1
β : Type v
f : α → β
r : β → β → Prop
m : Multiset α
h : {a | a ∈ m}.Pairwise fun a₁ a₂ => r (f a₁) (f a₂)
b₁ : β
h₁ : b₁ ∈ {b | b ∈ map f m}
b₂ : β
h₂ : b₂ ∈ {b | b ∈ map f m}
hn : b₁ ≠ b₂
⊢ r b₁ b₂

Tactic:
obtain ⟨⟨a₁, H₁, rfl⟩, a₂, H₂, rfl⟩ := Multiset.mem_map.1 h₁, Multiset.mem_map.1 h₂

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type v
f : α → β
r : β → β → Prop
m : Multiset α
h : {a | a ∈ m}.Pairwise fun a₁ a₂ => r (f a₁) (f a₂)
a₁ : α
H₁ : a₁ ∈ m
h₁ : f a₁ ∈ {b | b ∈ map f m}
a₂ : α
H₂ : a₂ ∈ m
h₂ : f a₂ ∈ {b | b ∈ map f m}
hn : f a₁ ≠ f a₂
⊢ r (f a₁) (f a₂)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type v
f : α → β
r : β → β → Prop
m : Multiset α
h : {a | a ∈ m}.Pairwise fun a₁ a₂ => r (f a₁) (f a₂)
a₁ : α
H₁ : a₁ ∈ m
h₁ : f a₁ ∈ {b | b ∈ map f m}
a₂ : α
H₂ : a₂ ∈ m
h₂ : f a₂ ∈ {b | b ∈ map f m}
hn : f a₁ ≠ f a₂
⊢ r (f a₁) (f a₂)

Tactic:
exact h H₁ H₂ (mt (congr_arg f) hn)

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem sbtw_const_vsub_iff {x y z : P} (p : P) :
    Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z

Tactic:
rw [Sbtw, Sbtw, wbtw_const_vsub_iff, (vsub_right_injective p).ne_iff,
  (vsub_right_injective p).ne_iff]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_of_div_eq_one (h : a / b = 1) : a = b :=
  inv_injective <| inv_eq_of_mul_eq_one_right <| by rwa [← div_eq_mul_inv]

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a / b = 1
⊢ a * b⁻¹ = 1

Tactic:
rwa [← div_eq_mul_inv]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem mul_inv_le_inv_mul_iff : a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b

Proof state:
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
a b c d : α
inst✝ : MulRightMono α
⊢ a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b

Tactic:
rw [← mul_le_mul_iff_left d, ← mul_le_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
  inv_mul_cancel_right]

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Orthogonality.lean
theorem sum_char_inv_mul_char_eq {a : ZMod n} (ha : IsUnit a) (b : ZMod n) :
    ∑ χ : DirichletCharacter R n, χ a⁻¹ * χ b = if a = b then (n.totient : R) else 0

Proof state:
R : Type u_1
inst✝³ : CommRing R
n : ℕ
inst✝² : NeZero n
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsDomain R
a : ZMod n
ha : IsUnit a
b : ZMod n
⊢ ∑ χ : DirichletCharacter R n, χ a⁻¹ * χ b = if a = b then ↑n.totient else 0

Tactic:
simp only [← map_mul, sum_characters_eq, ZMod.inv_mul_eq_one_of_isUnit ha]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem natCast_mul {a₁ a₃ : ℕ} (a₂) (_ : ((a₁ : ℕ) : R) = b₁)
    (_ : ((a₃ : ℕ) : R) = b₃) : ((a₁ ^ a₂ * a₃ : ℕ) : R) = b₁ ^ a₂ * b₃

Proof state:
R : Type u_1
inst✝ : CommSemiring R
b₁ b₃ : R
a₁ a₃ a₂ : ℕ
x✝¹ : ↑a₁ = b₁
x✝ : ↑a₃ = b₃
⊢ ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₃ a₂ : ℕ
⊢ ↑(a₁ ^ a₂ * a₃) = ↑a₁ ^ a₂ * ↑a₃

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a₁ a₃ a₂ : ℕ
⊢ ↑(a₁ ^ a₂ * a₃) = ↑a₁ ^ a₂ * ↑a₃

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem map_update_sub [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x y : M₁ i) :
    f (update m i (x - y)) = f (update m i x) - f (update m i y)

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ f (update m i (x - y)) = f (update m i x) - f (update m i y)

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, MultilinearMap.map_update_add, map_update_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem find?_range'_eq_none {s n : Nat} {p : Nat → Bool} :
    (range' s n).find? p = none ↔ ∀ i, s ≤ i → i < s + n → !p i

Proof state:
s n : Nat
p : Nat → Bool
⊢ find? p (range' s n) = none ↔ ∀ (i : Nat), s ≤ i → i < s + n → (!p i) = true

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem comap_map_le : I ≤ comap f (map f I)

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ I ≤ comap f (map f I)

Tactic:
rw [← map_le_iff_le_comap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_eq_foldrM (f : α → β → β) (b) (l : Array α) :
    l.foldr f b start stop = l.foldrM (m := Id) f b start stop

Proof state:
α : Type u_1
β : Type u_2
start stop : Nat
f : α → β → β
b : β
l : Array α
⊢ foldr f b l start stop = foldrM f b l start stop

Tactic:
simp [foldr, Id.run]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem OrderIso.map_sInf_eq_sInf_symm_preimage [CompleteLattice β] (f : α ≃o β) (s : Set α) :
    f (sInf s) = sInf (f.symm ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α ≃o β
s : Set α
⊢ f (sInf s) = sInf (⇑f.symm ⁻¹' s)

Tactic:
rw [map_sInf, ← sInf_image, f.image_eq_preimage]

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
@[simp]
lemma ideal_top : ideal (X := X) ⊤ = ⊤ :=
  top_le_iff.mp (ideal_mono (le_top (a := ⟨⊤, by simp [Ideal.map_top]⟩)))

Proof state:
X : Scheme
⊢ ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (⊤ U) = ⊤ (X.affineBasicOpen f)

Tactic:
simp [Ideal.map_top]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Defs.lean
theorem mul_inv_cancel_left₀ (h : a ≠ 0) (b : G₀) : a * (a⁻¹ * b) = b :=
  calc
    a * (a⁻¹ * b) = a * a⁻¹ * b := (mul_assoc _ _ _).symm
    _ = b

Proof state:
G₀ : Type u
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
b : G₀
⊢ a * a⁻¹ * b = b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Finsupp/Fin.lean
theorem tail_cons : tail (cons y s) = s :=
  ext fun k => by simp only [tail_apply, cons_succ]

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
s : Fin n →₀ M
k : Fin n
⊢ (cons y s).tail k = s k

Tactic:
simp only [tail_apply, cons_succ]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
theorem add_algebraMap {x y : S} (r : K) (h : IsConjRoot K x y) :
    IsConjRoot K (x + algebraMap K S r) (y + algebraMap K S r)

Proof state:
K : Type u_2
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Field K
inst✝ : Algebra K S
x y : S
r : K
h : IsConjRoot K x y
⊢ IsConjRoot K (x + (algebraMap K S) r) (y + (algebraMap K S) r)

Tactic:
rw [isConjRoot_def, minpoly.add_algebraMap x r, minpoly.add_algebraMap y r, h]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Inverse.lean
theorem X_eq_normalizeX : (X : k⟦X⟧) = normalize X

Proof state:
k : Type u_2
inst✝ : Field k
⊢ X = normalize X

Tactic:
simp only [normalize_apply, normUnit_X, Units.val_one, mul_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem nondegenerate_iff_det_ne_zero {B : BilinForm A M₂} (b : Basis ι A M₂) :
    B.Nondegenerate ↔ (BilinForm.toMatrix b B).det ≠ 0

Proof state:
M₂ : Type u_4
inst✝⁵ : AddCommGroup M₂
A : Type u_5
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Module A M₂
ι : Type u_6
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
B : BilinForm A M₂
b : Basis ι A M₂
⊢ B.Nondegenerate ↔ ((BilinForm.toMatrix b) B).det ≠ 0

Tactic:
rw [← Matrix.nondegenerate_iff_det_ne_zero, nondegenerate_toMatrix_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zipWith_foldl_eq_zip_foldl {f : α → β → γ} (i : δ):
    (zipWith f l₁ l₂).foldl g i = (zip l₁ l₂).foldl (fun r p => g r (f p.1 p.2)) i

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
l₁ : List α
l₂ : List β
g : δ → γ → δ
f : α → β → γ
i : δ
⊢ foldl g i (zipWith f l₁ l₂) = foldl (fun r p => g r (f p.fst p.snd)) i (l₁.zip l₂)

Tactic:
induction l₁ generalizing i l₂ <;> cases l₂ <;> simp_all

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
lemma iSup_sUnion (S : Set (Set α)) (f : α → β) :
    (⨆ x ∈ ⋃₀ S, f x) = ⨆ (s ∈ S) (x ∈ s), f x

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨆ x ∈ ⋃₀ S, f x = ⨆ s ∈ S, ⨆ x ∈ s, f x

Tactic:
rw [sUnion_eq_iUnion, iSup_iUnion, ← iSup_subtype'']

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Basic.lean
theorem coe_decompose_mul_of_left_mem_of_le (a_mem : a ∈ 𝒜 i) (h : i ≤ n) :
    (decompose 𝒜 (a * b) n : A) = a * decompose 𝒜 b (n - i)

Proof state:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹⁰ : Semiring A
inst✝⁹ : DecidableEq ι
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : PartialOrder ι
inst✝⁶ : CanonicallyOrderedAdd ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
h : i ≤ n
a : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (↑a * b)) n) = ↑a * ↑(((decompose 𝒜) b) (n - i))

Tactic:
rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_le]

Result:
no goals

Proof state:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹⁰ : Semiring A
inst✝⁹ : DecidableEq ι
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : PartialOrder ι
inst✝⁶ : CanonicallyOrderedAdd ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
a b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
a_mem : a ∈ 𝒜 i
h : i ≤ n
⊢ ↑(((decompose 𝒜) (a * b)) n) = a * ↑(((decompose 𝒜) b) (n - i))

Tactic:
lift a to 𝒜 i using a_mem

Result:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹⁰ : Semiring A
inst✝⁹ : DecidableEq ι
inst✝⁸ : AddCommMonoid ι
inst✝⁷ : PartialOrder ι
inst✝⁶ : CanonicallyOrderedAdd ι
inst✝⁵ : SetLike σ A
inst✝⁴ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝³ : GradedRing 𝒜
b : A
n i : ι
inst✝² : Sub ι
inst✝¹ : OrderedSub ι
inst✝ : AddLeftReflectLE ι
h : i ≤ n
a : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (↑a * b)) n) = ↑a * ↑(((decompose 𝒜) b) (n - i))
-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_inv (σ : Perm α) : support σ⁻¹ = σ.support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ σ⁻¹.support = σ.support

Tactic:
simp_rw [Finset.ext_iff, mem_support, not_iff_not, inv_eq_iff_eq.trans eq_comm, imp_true_iff]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_add_eq_sqrt_iff_real_inner_eq_zero {x y : F} :
    ‖x + y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x + y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0

Tactic:
rw [← norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, eq_comm, sqrt_eq_iff_mul_self_eq,
  eq_comm] <;> positivity

Result:
no goals
-- Mathlib/Analysis/Convex/Continuous.lean
lemma ConcaveOn.isBoundedUnder_abs (hf : ConcaveOn ℝ C f) {x₀ : E} (hC : C ∈ 𝓝 x₀) :
    (𝓝 x₀).IsBoundedUnder (· ≤ ·) |f| ↔ (𝓝 x₀).IsBoundedUnder (· ≥ ·) f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConcaveOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
⊢ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) |f| ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (𝓝 x₀) f

Tactic:
simpa [Pi.neg_def, Pi.abs_def] using hf.neg.isBoundedUnder_abs hC

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem denseRange_iff {f : β → α} : DenseRange f ↔ ∀ x, ∀ r > 0, ∃ y, dist x (f y) < r :=
  forall_congr' fun x => by simp only [mem_closure_iff, exists_range_iff]

Proof state:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
x : α
⊢ x ∈ closure (range f) ↔ ∀ r > 0, ∃ y, dist x (f y) < r

Tactic:
simp only [mem_closure_iff, exists_range_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_congr [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a b : α} {fallback : β}
    (hab : a == b) : getD m a fallback = getD m b fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a b : α
fallback : β
hab : (a == b) = true
⊢ getD m a fallback = getD m b fallback

Tactic:
simp_to_model using List.getValueD_congr

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
lemma real_iff [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] {a : A} :
    QuasispectrumRestricts a Complex.reCLM ↔ ∀ x ∈ σₙ ℂ a, x = x.re

Proof state:
A : Type u_3
inst✝³ : NonUnitalRing A
inst✝² : Module ℂ A
inst✝¹ : IsScalarTower ℂ A A
inst✝ : SMulCommClass ℂ A A
a : A
⊢ QuasispectrumRestricts a ⇑Complex.reCLM ↔ ∀ x ∈ σₙ ℂ a, x = ↑x.re

Tactic:
rw [quasispectrumRestricts_iff_spectrumRestricts_inr,
  Unitization.quasispectrum_eq_spectrum_inr' _ ℂ, SpectrumRestricts.real_iff]

Result:
no goals
-- Mathlib/Data/List/Forall2.lean
theorem sublistForall₂_map_left_iff {f : γ → α} {l₁ : List γ} {l₂ : List β} :
    SublistForall₂ R (map f l₁) l₂ ↔ SublistForall₂ (fun c b => R (f c) b) l₁ l₂

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → α
l₁ : List γ
l₂ : List β
⊢ SublistForall₂ R (map f l₁) l₂ ↔ SublistForall₂ (fun c b => R (f c) b) l₁ l₂

Tactic:
simp [sublistForall₂_iff]

Result:
no goals