harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
@[simp]
lemma leadingCoeff_ΨSq [NoZeroDivisors R] {n : ℤ} (h : (n : R) ≠ 0) :
    (W.ΨSq n).leadingCoeff = n ^ 2

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : NoZeroDivisors R
n : ℤ
h : ↑n ≠ 0
⊢ (W.ΨSq n).leadingCoeff = ↑n ^ 2

Tactic:
rw [leadingCoeff, W.natDegree_ΨSq h, coeff_ΨSq]

Result:
no goals
-- Mathlib/Combinatorics/Additive/Corner/Defs.lean
@[simp] lemma not_isCorner_empty : ¬ IsCorner ∅ x₁ y₁ x₂ y₂

Proof state:
G : Type u_1
inst✝ : AddCommMonoid G
x₁ y₁ x₂ y₂ : G
⊢ ¬IsCorner ∅ x₁ y₁ x₂ y₂

Tactic:
simp [isCorner_iff]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem algebraMap_eq_zero_iff {x : K[X]} : algebraMap K[X] (RatFunc K) x = 0 ↔ x = 0

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : K[X]
⊢ (algebraMap K[X] (RatFunc K)) x = 0 ↔ x = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
    m.size ≤ (m.insertIfNew k v).size

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β k
⊢ m.size ≤ (m.insertIfNew k v).size

Tactic:
simp_to_raw using Raw₀.size_le_size_insertIfNew ⟨m, _⟩

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
theorem mulMap'_surjective : Function.Surjective (mulMap' M N)

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ Function.Surjective ⇑(M.mulMap' N)

Tactic:
simp_rw [mulMap', LinearMap.coe_comp, LinearEquiv.coe_coe, EquivLike.comp_surjective,
  LinearMap.surjective_rangeRestrict]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
theorem map_comp_isoH0_hom :
    map f φ 0 ≫ (isoH0 B).hom = (isoH0 A).hom ≫ H0Map f φ

Proof state:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ map f φ 0 ≫ (isoH0 B).hom = (isoH0 A).hom ≫ H0Map f φ

Tactic:
simp [← cancel_epi (groupCohomologyπ _ _)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem sshiftRightRec_succ_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
    sshiftRightRec x y (n + 1) = (sshiftRightRec x y n).sshiftRight' (y &&& twoPow w₂ (n + 1))

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
n : Nat
⊢ x.sshiftRightRec y (n + 1) = (x.sshiftRightRec y n).sshiftRight' (y &&& twoPow w₂ (n + 1))

Tactic:
simp [sshiftRightRec]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image_image₂_antidistrib_left {g : γ → δ} {f' : β' → α → δ} {g' : β → β'}
    (h_antidistrib : ∀ a b, g (f a b) = f' (g' b) a) :
    (image₂ f s t).image g = image₂ f' (t.image g') s :=
  coe_injective <| by
    push_cast
    exact image_image2_antidistrib_left h_antidistrib

Proof state:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ ↑(image g (image₂ f s t)) = ↑(image₂ f' (image g' t) s)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ g '' image2 f ↑s ↑t = image2 f' (g' '' ↑t) ↑s

Proof state:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq β'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ g '' image2 f ↑s ↑t = image2 f' (g' '' ↑t) ↑s

Tactic:
exact image_image2_antidistrib_left h_antidistrib

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Rank.lean
theorem finrank_sup_eq_finrank_left_mul_finrank_of_free :
    finrank R ↥(A ⊔ B) = finrank R A * finrank A (Algebra.adjoin A (B : Set S))

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
inst✝¹ : Free R ↥A
inst✝ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
⊢ finrank R ↥(A ⊔ B) = finrank R ↥A * finrank ↥A ↥(Algebra.adjoin ↥A ↑B)

Tactic:
simpa only [map_mul] using congr(Cardinal.toNat $(rank_sup_eq_rank_left_mul_rank_of_free A B))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem mapIdx_eq_cons_iff {l : List α} {b : β} :
    mapIdx f l = b :: l₂ ↔
      ∃ (a : α) (l₁ : List α), l = a :: l₁ ∧ f 0 a = b ∧ mapIdx (fun i => f (i + 1)) l₁ = l₂

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
l₂ : List β
l : List α
b : β
⊢ mapIdx f l = b :: l₂ ↔ ∃ a l₁, l = a :: l₁ ∧ f 0 a = b ∧ mapIdx (fun i => f (i + 1)) l₁ = l₂

Tactic:
cases l <;> simp [and_assoc]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_le_floor_add_one (a : α) : ⌈a⌉₊ ≤ ⌊a⌋₊ + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
⊢ ⌈a⌉₊ ≤ ⌊a⌋₊ + 1

Tactic:
rw [ceil_le, Nat.cast_add, Nat.cast_one]

Result:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
⊢ a ≤ ↑⌊a⌋₊ + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
⊢ a ≤ ↑⌊a⌋₊ + 1

Tactic:
exact (lt_floor_add_one a).le

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem diam_preimage (s : Set β) : Metric.diam (h ⁻¹' s) = Metric.diam s

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
s : Set β
⊢ Metric.diam (⇑h ⁻¹' s) = Metric.diam s

Tactic:
rw [← image_symm, diam_image]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_setOf [Fintype α] (p : α → Prop) [DecidablePred p] [Fintype { x | p x }] :
    Set.toFinset {x | p x} = Finset.univ.filter p

Proof state:
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype ↑{x | p x}
⊢ {x | p x}.toFinset = filter p Finset.univ

Tactic:
ext

Result:
case h
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype ↑{x | p x}
a✝ : α
⊢ a✝ ∈ {x | p x}.toFinset ↔ a✝ ∈ filter p Finset.univ

Proof state:
case h
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype ↑{x | p x}
a✝ : α
⊢ a✝ ∈ {x | p x}.toFinset ↔ a✝ ∈ filter p Finset.univ

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
@[simp]
lemma pairingIn_same [FaithfulSMul S R] [P.IsValuedIn S] (i : ι) :
    P.pairingIn S i i = 2 :=
  FaithfulSMul.algebraMap_injective S R <| by simp [map_ofNat]

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra S R
inst✝¹ : FaithfulSMul S R
inst✝ : P.IsValuedIn S
i : ι
⊢ (algebraMap S R) (P.pairingIn S i i) = (algebraMap S R) 2

Tactic:
simp [map_ofNat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_shiftLeftConst : eval (shiftLeftConst n) = ((· <<< n) : BitVec w → BitVec w)

Proof state:
n w : Nat
⊢ (shiftLeftConst n).eval = fun x => x <<< n

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem bsup_lt_ord {o : Ordinal} {f : ∀ a < o, Ordinal} {c : Ordinal} (ho : o.card < c.cof) :
    (∀ i hi, f i hi < c) → bsup.{u, u} o f < c :=
  bsup_lt_ord_lift (by rwa [o.card.lift_id])

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
⊢ Cardinal.lift.{u, u} o.card < c.cof

Tactic:
rwa [o.card.lift_id]

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem natDegree_of_b_ne_zero (ha : P.a = 0) (hb : P.b ≠ 0) : P.toPoly.natDegree = 2

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b ≠ 0
⊢ P.toPoly.natDegree = 2

Tactic:
rw [of_a_eq_zero ha, natDegree_quadratic hb]

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
theorem biUnion_singleton {f : α → β} : (s.biUnion fun a => {f a}) = s.image f :=
  ext fun x => by simp only [mem_biUnion, mem_image, mem_singleton, eq_comm]

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
inst✝ : DecidableEq β
f : α → β
x : β
⊢ (x ∈ s.biUnion fun a => {f a}) ↔ x ∈ image f s

Tactic:
simp only [mem_biUnion, mem_image, mem_singleton, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_pos {b : Bool} {a a' : α} (h : b = true) : (bif b then a else a') = a

Proof state:
α : Type u_1
b : Bool
a a' : α
h : b = true
⊢ (bif b then a else a') = a

Tactic:
rw [h, cond_true]

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

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

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem T_neg_one : T R (-1) = X := show 2 * X * 1 - X = X by ring

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

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem inv_pow_le_inv_pow_of_le (a1 : 1 ≤ a) {m n : ℕ} (mn : m ≤ n) : (a ^ n)⁻¹ ≤ (a ^ m)⁻¹

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ n)⁻¹ ≤ (a ^ m)⁻¹

Tactic:
convert one_div_pow_le_one_div_pow_of_le a1 mn using 1 <;> simp

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem rat_sub_iff : LiouvilleWith p (r - x) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
r : ℚ
⊢ LiouvilleWith p (↑r - x) ↔ LiouvilleWith p x

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Tendsto.atBot_mul_const_of_neg' (hr : r < 0) (hf : Tendsto f l atBot) :
    Tendsto (fun x => f x * r) l atTop

Proof state:
α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedRing R
inst✝ : Archimedean R
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto (fun x => f x * r) l atTop

Tactic:
simpa only [mul_neg, tendsto_neg_atBot_iff] using hf.atBot_mul_const' (neg_pos.2 hr)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem max_const (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => max (f x) a

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
Kf : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith Kf fun x => f x ⊔ a

Tactic:
simpa only [max_eq_left (zero_le Kf)] using hf.max (LipschitzWith.const a)

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem existsUnique_equiv_nat (a : ℤ) {b : ℤ} (hb : 0 < b) : ∃ z : ℕ, ↑z < b ∧ ↑z ≡ a [ZMOD b] :=
  let ⟨z, hz1, hz2, hz3⟩ := existsUnique_equiv a hb
  ⟨z.natAbs, by
    constructor <;> rw [natAbs_of_nonneg hz1] <;> assumption⟩

Proof state:
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑z.natAbs < b ∧ ↑z.natAbs ≡ a [ZMOD b]

Tactic:
constructor <;> rw [natAbs_of_nonneg hz1] <;> assumption

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
/-- The derivative of `log ∘ f` is the logarithmic derivative provided `f` is differentiable and
`f x  ≠ 0`. -/
lemma Real.deriv_log_comp_eq_logDeriv {f : ℝ → ℝ} {x : ℝ} (h₁ : DifferentiableAt ℝ f x)
    (h₂ : f x ≠ 0) : deriv (log ∘ f) x = logDeriv f x

Proof state:
f : ℝ → ℝ
x : ℝ
h₁ : DifferentiableAt ℝ f x
h₂ : f x ≠ 0
⊢ deriv (log ∘ f) x = logDeriv f x

Tactic:
simp only [ne_eq, logDeriv, Pi.div_apply, ← deriv.log h₁ h₂, Function.comp_def]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem CompositionAsSet.toComposition_length (c : CompositionAsSet n) :
    c.toComposition.length = c.length

Proof state:
n : ℕ
c : CompositionAsSet n
⊢ c.toComposition.length = c.length

Tactic:
simp [CompositionAsSet.toComposition, Composition.length, Composition.blocks]

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Pi.lean
theorem left_inv : Function.LeftInverse (invFun p) (toFun p) := fun x =>
  Submodule.Quotient.induction_on _ x fun x' => by
    dsimp only [toFun, invFun]
    rw [quotientPiLift_mk p, funext fun i => (mkQ_apply (p i) (x' i)), piQuotientLift_mk p,
      lsum_single, id_apply]

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ invFun p (toFun p (Quotient.mk x')) = Quotient.mk x'

Tactic:
dsimp only [toFun, invFun]

Result:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ (piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) ((quotientPiLift p (fun i => (p i).mkQ) ⋯) (Quotient.mk x')) =
    Quotient.mk x'

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁴ : CommRing R
Ms : ι → Type u_3
inst✝³ : (i : ι) → AddCommGroup (Ms i)
inst✝² : (i : ι) → Module R (Ms i)
p : (i : ι) → Submodule R (Ms i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ (piQuotientLift p (pi Set.univ p) (single R Ms) ⋯) ((quotientPiLift p (fun i => (p i).mkQ) ⋯) (Quotient.mk x')) =
    Quotient.mk x'

Tactic:
rw [quotientPiLift_mk p, funext fun i => (mkQ_apply (p i) (x' i)), piQuotientLift_mk p,
  lsum_single, id_apply]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem Bool.inf_eq_band : (· ⊓ ·) = and

Proof state:
⊢ (fun x1 x2 => x1 ⊓ x2) = and

Tactic:
dsimp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
@[simp]
protected lemma map_one : map f (1 : GL n R) = 1

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
⊢ (map f) 1 = 1

Tactic:
ext

Result:
case a.a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
i✝ j✝ : n
⊢ ↑((map f) 1) i✝ j✝ = ↑1 i✝ j✝

Proof state:
case a.a
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
i✝ j✝ : n
⊢ ↑((map f) 1) i✝ j✝ = ↑1 i✝ j✝

Tactic:
simp only [_root_.map_one, Units.val_one]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
@[to_additive] lemma smul_div_smul_comm (a : α) (s : Set α) (b : α) (t : Set α) :
    a • s / b • t = (a / b) • (s / t)

Proof state:
α : Type u_2
inst✝ : CommGroup α
a : α
s : Set α
b : α
t : Set α
⊢ a • s / b • t = (a / b) • (s / t)

Tactic:
simp_rw [← image_smul, smul_eq_mul, ← singleton_mul, mul_div_mul_comm _ s,
  singleton_div_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem lookup_isSome_iff {l : List (α × β)} {k : α} :
    (l.lookup k).isSome ↔ ∃ p ∈ l, k == p.1

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l : List (α × β)
k : α
⊢ (lookup k l).isSome = true ↔ ∃ p, p ∈ l ∧ (k == p.fst) = true

Tactic:
simp [lookup_eq_findSome?]

Result:
no goals
-- Mathlib/Algebra/Order/UpperLower.lean
theorem upperClosure_mul_distrib : upperClosure (s * t) = upperClosure s * upperClosure t :=
  SetLike.coe_injective <| by
    rw [UpperSet.coe_mul, mul_upperClosure, upperClosure_mul, UpperSet.upperClosure]

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
⊢ ↑(upperClosure (s * t)) = ↑(upperClosure s * upperClosure t)

Tactic:
rw [UpperSet.coe_mul, mul_upperClosure, upperClosure_mul, UpperSet.upperClosure]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval_map (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) :
    eval g (map f p) = eval₂ f g p

Proof state:
case h_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (eval g) ((map f) p) = eval₂ f g p → (eval g) ((map f) (p * X n)) = eval₂ f g (p * X n)

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_and {x y : BitVec w} : (x &&& y).msb = (x.msb && y.msb)

Proof state:
w : Nat
x y : BitVec w
⊢ (x &&& y).msb = (x.msb && y.msb)

Tactic:
simp [BitVec.msb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem getLeft?_eq_some_iff : x.getLeft? = some a ↔ x = inl a

Proof state:
α✝ : Type u_1
a : α✝
β✝ : Type u_2
x : α✝ ⊕ β✝
⊢ x.getLeft? = some a ↔ x = inl a

Tactic:
cases x <;> simp only [getLeft?, Option.some.injEq, inl.injEq, reduceCtorEq]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_top : ∞⁻¹ = 0 :=
  bot_unique <| le_of_forall_gt_imp_ge_of_dense fun a (h : 0 < a) => sInf_le <| by
    simp [*, h.ne', top_mul]

Proof state:
a : ℝ≥0∞
h : 0 < a
⊢ a ∈ {b | 1 ≤ ⊤ * b}

Tactic:
simp [*, h.ne', top_mul]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean
theorem sSup_unitClosedBall_eq_norm {𝕜 𝕜₂ E F : Type*} [NormedAddCommGroup E]
    [SeminormedAddCommGroup F] [DenselyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂}
    [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
    sSup ((fun x => ‖f x‖) '' closedBall 0 1) = ‖f‖

Proof state:
𝕜 : Type u_11
𝕜₂ : Type u_12
E : Type u_13
F : Type u_14
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ sSup ((fun x => ‖f x‖) '' closedBall 0 1) = ‖f‖

Tactic:
simpa only [NNReal.coe_sSup, Set.image_image] using
  NNReal.coe_inj.2 f.sSup_unitClosedBall_eq_nnnorm

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Ioo : (some : α → WithTop α) '' Ioo a b = Ioo (a : WithTop α) b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Ioo a b = Ioo ↑a ↑b

Tactic:
rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Iio_self <| Iio_subset_Iio le_top)]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
lemma coe_add_eq_top_iff : a + y = ⊤ ↔ y = ⊤

Proof state:
α : Type u
inst✝ : Add α
y : WithTop α
a : α
⊢ ↑a + y = ⊤ ↔ y = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma isStrictlyLE_of_iso (n : ℤ) [K.IsStrictlyLE n] : L.IsStrictlyLE n

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K L : CochainComplex C ℤ
e : K ≅ L
n : ℤ
inst✝ : K.IsStrictlyLE n
⊢ L.IsStrictlyLE n

Tactic:
apply isStrictlySupported_of_iso e

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem append_left_lt [LT α] {l₁ : Vector α n} {l₂ l₃ : Vector α m} (h : l₂ < l₃) :
    l₁ ++ l₂ < l₁ ++ l₃

Proof state:
α : Type u_1
n m : Nat
inst✝ : LT α
l₁ : Vector α n
l₂ l₃ : Vector α m
h : l₂ < l₃
⊢ l₁ ++ l₂ < l₁ ++ l₃

Tactic:
simpa using Array.append_left_lt h

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem neg_eq_neg_one_mul (a : α) : -a = -1 * a

Proof state:
α : Type u
inst✝¹ : MulOneClass α
inst✝ : HasDistribNeg α
a : α
⊢ -a = -1 * a

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Algebraic/MvPolynomial.lean
theorem transcendental_supported_X {i : σ} {s : Set σ} (h : i ∉ s) :
    Transcendental (supported R s) (X i : MvPolynomial σ R)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
s : Set σ
h : i ∉ s
⊢ Transcendental (↥(supported R s)) (X i)

Tactic:
simpa using transcendental_supported_polynomial_aeval_X R h (Polynomial.transcendental_X R)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/CompareExp.lean
theorem isLittleO_pow_mul_exp {b₁ b₂ : ℝ} (hl : IsExpCmpFilter l) (hb : b₁ < b₂) (m n : ℕ) :
    (fun z => z ^ m * exp (b₁ * z)) =o[l] fun z => z ^ n * exp (b₂ * z)

Proof state:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
m n : ℕ
⊢ (fun z => z ^ m * cexp (↑b₁ * z)) =o[l] fun z => z ^ n * cexp (↑b₂ * z)

Tactic:
simpa only [cpow_natCast] using hl.isLittleO_cpow_mul_exp hb m n

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_union₀ (h : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) :
    μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

Tactic:
simp [← restrict_union_add_inter₀ s ht, restrict_zero_set h]

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem uniformOfFinset_apply_of_not_mem (ha : a ∉ s) : uniformOfFinset s hs a = 0

Proof state:
α : Type u_1
s : Finset α
hs : s.Nonempty
a : α
ha : a ∉ s
⊢ (uniformOfFinset s hs) a = 0

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Membership.lean
theorem coe_iSup_of_directed {S : ι → Subsemigroup M} (hS : Directed (· ≤ ·) S) :
    ((⨆ i, S i : Subsemigroup M) : Set M) = ⋃ i, S i :=
  Set.ext fun x => by simp [mem_iSup_of_directed hS]

Proof state:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
simp [mem_iSup_of_directed hS]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_fun_eq_lift_mul : Module.rank R (η → M) =
    (Fintype.card η : Cardinal.{max u₁' v}) * Cardinal.lift.{u₁'} (Module.rank R M)

Proof state:
R : Type u
M : Type v
η : Type u₁'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Free R M
inst✝ : Fintype η
⊢ Module.rank R (η → M) = ↑(Fintype.card η) * lift.{u₁', v} (Module.rank R M)

Tactic:
rw [rank_pi, Cardinal.sum_const, Cardinal.mk_fintype, Cardinal.lift_natCast]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem setLaverage_const (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) (c : ℝ≥0∞) : ⨍⁻ _x in s, c ∂μ = c

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs₀ : μ s ≠ 0
hs : μ s ≠ ⊤
c : ℝ≥0∞
⊢ ⨍⁻ (_x : α) in s, c ∂μ = c

Tactic:
simp only [setLaverage_eq, lintegral_const, Measure.restrict_apply, MeasurableSet.univ,
  univ_inter, div_eq_mul_inv, mul_assoc, ENNReal.mul_inv_cancel hs₀ hs, mul_one]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem ediam_mul_le (x y : Set E) : EMetric.diam (x * y) ≤ EMetric.diam x + EMetric.diam y :=
  (LipschitzOnWith.ediam_image2_le (· * ·) _ _
        (fun _ _ => (isometry_mul_right _).lipschitz.lipschitzOnWith) fun _ _ =>
        (isometry_mul_left _).lipschitz.lipschitzOnWith).trans_eq <|
    by simp only [ENNReal.coe_one, one_mul]

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
x y : Set E
⊢ ↑1 * EMetric.diam x + ↑1 * EMetric.diam y = EMetric.diam x + EMetric.diam y

Tactic:
simp only [ENNReal.coe_one, one_mul]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Quotient.lean
theorem sum_card_fixedBy_eq_card_orbits_mul_card_group [Fintype α] [∀ a : α, Fintype <| fixedBy β a]
    [Fintype Ω] : (∑ a : α, Fintype.card (fixedBy β a)) = Fintype.card Ω * Fintype.card α

Proof state:
α : Type u
β : Type v
inst✝⁴ : Group α
inst✝³ : MulAction α β
inst✝² : Fintype α
inst✝¹ : (a : α) → Fintype ↑(fixedBy β a)
inst✝ : Fintype (Quotient (orbitRel α β))
⊢ ∑ a : α, Fintype.card ↑(fixedBy β a) = Fintype.card (Quotient (orbitRel α β)) * Fintype.card α

Tactic:
rw [← Fintype.card_prod, ← Fintype.card_sigma,
  Fintype.card_congr (sigmaFixedByEquivOrbitsProdGroup α β)]

Result:
no goals